Documentation

Mathlib.Order.Monotone.Monovary

Monovariance of functions #

Two functions vary together if a strict change in the first implies a change in the second.

This is in some sense a way to say that two functions f : ι → α, g : ι → β are "monotone together", without actually having an order on ι.

This condition comes up in the rearrangement inequality. See Algebra.Order.Rearrangement.

Main declarations #

def Monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (g : ιβ) :

f monovaries with g if g i < g j implies f i ≤ f j.

Equations
def Antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (g : ιβ) :

f antivaries with g if g i < g j implies f j ≤ f i.

Equations
def MonovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (g : ιβ) (s : Set ι) :

f monovaries with g on s if g i < g j implies f i ≤ f j for all i, j ∈ s.

Equations
def AntivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (g : ιβ) (s : Set ι) :

f antivaries with g on s if g i < g j implies f j ≤ f i for all i, j ∈ s.

Equations
theorem Monovary.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} (h : Monovary f g) (s : Set ι) :
theorem Antivary.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} (h : Antivary f g) (s : Set ι) :
@[simp]
theorem MonovaryOn.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem AntivaryOn.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem monovaryOn_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem antivaryOn_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem monovaryOn_iff_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g s Monovary (fun (i : s) => f i) fun (i : s) => g i
theorem antivaryOn_iff_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g s Antivary (fun (i : s) => f i) fun (i : s) => g i
theorem MonovaryOn.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s t : Set ι} (hst : s t) (h : MonovaryOn f g t) :
theorem AntivaryOn.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s t : Set ι} (hst : s t) (h : AntivaryOn f g t) :
theorem monovary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ιβ) (a : α) :
theorem antivary_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ιβ) (a : α) :
theorem monovary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (b : β) :
theorem antivary_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (b : β) :
theorem monovary_self {ι : Type u_1} {α : Type u_3} [Preorder α] (f : ια) :
theorem monovaryOn_self {ι : Type u_1} {α : Type u_3} [Preorder α] (f : ια) (s : Set ι) :
theorem Subsingleton.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ια) (g : ιβ) :
theorem Subsingleton.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ια) (g : ιβ) :
theorem Subsingleton.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ια) (g : ιβ) (s : Set ι) :
theorem Subsingleton.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Subsingleton ι] (f : ια) (g : ιβ) (s : Set ι) :
theorem monovaryOn_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ιβ) (a : α) (s : Set ι) :
theorem antivaryOn_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (g : ιβ) (a : α) (s : Set ι) :
theorem monovaryOn_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (b : β) (s : Set ι) :
theorem antivaryOn_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] (f : ια) (b : β) (s : Set ι) :
theorem Monovary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} (h : Monovary f g) (k : ι'ι) :
theorem Antivary.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} (h : Antivary f g) (k : ι'ι) :
theorem MonovaryOn.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (k : ι'ι) :
theorem AntivaryOn.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (k : ι'ι) :
theorem Monovary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Monovary f g) (hf : Monotone f') :
theorem Monovary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Monovary f g) (hf : Antitone f') :
theorem Antivary.comp_monotone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Antivary f g) (hf : Monotone f') :
theorem Antivary.comp_antitone_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Antivary f g) (hf : Antitone f') :
theorem MonovaryOn.comp_monotone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (hf : Monotone f') :
theorem MonovaryOn.comp_antitone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (hf : Antitone f') :
theorem AntivaryOn.comp_monotone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (hf : Monotone f') :
theorem AntivaryOn.comp_antitone_on_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [Preorder β] [Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (hf : Antitone f') :
theorem Monovary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem Antivary.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem Monovary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem Antivary.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem Monovary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem Antivary.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
theorem MonovaryOn.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem AntivaryOn.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem MonovaryOn.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem AntivaryOn.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem MonovaryOn.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem AntivaryOn.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
@[simp]
theorem monovary_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem monovary_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem antivary_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem antivary_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem monovaryOn_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
@[simp]
theorem monovaryOn_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
@[simp]
theorem antivaryOn_toDual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
@[simp]
theorem antivaryOn_toDual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
@[simp]
theorem monovary_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ια} [PartialOrder ι] :
@[simp]
theorem antivary_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ια} [PartialOrder ι] :
@[simp]
theorem monovaryOn_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ια} {s : Set ι} [PartialOrder ι] :
@[simp]
theorem antivaryOn_id_iff {ι : Type u_1} {α : Type u_3} [Preorder α] {f : ια} {s : Set ι} [PartialOrder ι] :
theorem StrictMono.trans_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [PartialOrder ι] (hf : StrictMono f) (h : Monovary g f) :
theorem StrictMono.trans_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [PartialOrder ι] (hf : StrictMono f) (h : Antivary g f) :
theorem StrictAnti.trans_monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [PartialOrder ι] (hf : StrictAnti f) (h : Monovary g f) :
theorem StrictAnti.trans_antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [PartialOrder ι] (hf : StrictAnti f) (h : Antivary g f) :
theorem StrictMonoOn.trans_monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [PartialOrder ι] (hf : StrictMonoOn f s) (h : MonovaryOn g f s) :
theorem StrictMonoOn.trans_antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [PartialOrder ι] (hf : StrictMonoOn f s) (h : AntivaryOn g f s) :
theorem StrictAntiOn.trans_monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [PartialOrder ι] (hf : StrictAntiOn f s) (h : MonovaryOn g f s) :
theorem StrictAntiOn.trans_antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [PartialOrder ι] (hf : StrictAntiOn f s) (h : AntivaryOn g f s) :
theorem Monotone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [LinearOrder ι] (hf : Monotone f) (hg : Monotone g) :
theorem Monotone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [LinearOrder ι] (hf : Monotone f) (hg : Antitone g) :
theorem Antitone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [LinearOrder ι] (hf : Antitone f) (hg : Antitone g) :
theorem Antitone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} [LinearOrder ι] (hf : Antitone f) (hg : Monotone g) :
theorem MonotoneOn.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [LinearOrder ι] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
theorem MonotoneOn.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [LinearOrder ι] (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
theorem AntitoneOn.monovaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [LinearOrder ι] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
theorem AntitoneOn.antivaryOn {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] {f : ια} {g : ιβ} {s : Set ι} [LinearOrder ι] (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
theorem MonovaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : MonovaryOn f g s) (hg : MonotoneOn g' (g '' s)) :
theorem MonovaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : MonovaryOn f g s) (hg : AntitoneOn g' (g '' s)) :
theorem AntivaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : AntivaryOn f g s) (hg : MonotoneOn g' (g '' s)) :
theorem AntivaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [Preorder α] [LinearOrder β] [Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : AntivaryOn f g s) (hg : AntitoneOn g' (g '' s)) :
theorem Monovary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ια} {g : ιβ} (h : Monovary f g) :
theorem Antivary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ια} {g : ιβ} (h : Antivary f g) :
theorem MonovaryOn.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) :
theorem AntivaryOn.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [Preorder α] [LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) :
theorem monovary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ια} {g : ιβ} :
theorem antivary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ια} {g : ιβ} :
theorem monovaryOn_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem antivaryOn_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [LinearOrder α] [LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} :