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_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (f : ια) (g : ιβ) :

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

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

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

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

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

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

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

Equations
theorem Monovary.monovaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} (h : Monovary f g) (s : Set ι) :
theorem Antivary.antivaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} (h : Antivary f g) (s : Set ι) :
@[simp]
theorem MonovaryOn.empty {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem AntivaryOn.empty {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
@[simp]
theorem monovaryOn_univ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
MonovaryOn f g Set.univ Monovary f g
@[simp]
theorem antivaryOn_univ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
AntivaryOn f g Set.univ Antivary f g
theorem MonovaryOn.subset {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} {t : Set ι} (hst : s t) (h : MonovaryOn f g t) :
theorem AntivaryOn.subset {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} {t : Set ι} (hst : s t) (h : AntivaryOn f g t) :
theorem monovary_const_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (g : ιβ) (a : α) :
theorem antivary_const_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (g : ιβ) (a : α) :
theorem monovary_const_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (f : ια) (b : β) :
theorem antivary_const_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (f : ια) (b : β) :
theorem monovary_self {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ια) :
theorem monovaryOn_self {ι : Type u_1} {α : Type u_2} [inst : Preorder α] (f : ια) (s : Set ι) :
theorem Subsingleton.monovary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Subsingleton ι] (f : ια) (g : ιβ) :
theorem Subsingleton.antivary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Subsingleton ι] (f : ια) (g : ιβ) :
theorem Subsingleton.monovaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Subsingleton ι] (f : ια) (g : ιβ) (s : Set ι) :
theorem Subsingleton.antivaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] [inst : Subsingleton ι] (f : ια) (g : ιβ) (s : Set ι) :
theorem monovaryOn_const_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (g : ιβ) (a : α) (s : Set ι) :
theorem antivaryOn_const_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (g : ιβ) (a : α) (s : Set ι) :
theorem monovaryOn_const_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (f : ια) (b : β) (s : Set ι) :
theorem antivaryOn_const_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] (f : ια) (b : β) (s : Set ι) :
theorem Monovary.comp_right {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} (h : Monovary f g) (k : ι'ι) :
Monovary (f k) (g k)
theorem Antivary.comp_right {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} (h : Antivary f g) (k : ι'ι) :
Antivary (f k) (g k)
theorem MonovaryOn.comp_right {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (k : ι'ι) :
MonovaryOn (f k) (g k) (k ⁻¹' s)
theorem AntivaryOn.comp_right {ι : Type u_1} {ι' : Type u_4} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (k : ι'ι) :
AntivaryOn (f k) (g k) (k ⁻¹' s)
theorem Monovary.comp_monotone_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Monovary f g) (hf : Monotone f') :
Monovary (f' f) g
theorem Monovary.comp_antitone_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Monovary f g) (hf : Antitone f') :
Antivary (f' f) g
theorem Antivary.comp_monotone_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Antivary f g) (hf : Monotone f') :
Antivary (f' f) g
theorem Antivary.comp_antitone_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} (h : Antivary f g) (hf : Antitone f') :
Monovary (f' f) g
theorem MonovaryOn.comp_monotone_on_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (hf : Monotone f') :
MonovaryOn (f' f) g s
theorem MonovaryOn.comp_antitone_on_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) (hf : Antitone f') :
AntivaryOn (f' f) g s
theorem AntivaryOn.comp_monotone_on_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (hf : Monotone f') :
AntivaryOn (f' f) g s
theorem AntivaryOn.comp_antitone_on_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : Preorder β] [inst : Preorder γ] {f : ια} {f' : αγ} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) (hf : Antitone f') :
MonovaryOn (f' f) g s
theorem Monovary.dual {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Monovary f gMonovary (OrderDual.toDual f) (OrderDual.toDual g)
theorem Antivary.dual {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Antivary f gAntivary (OrderDual.toDual f) (OrderDual.toDual g)
theorem Monovary.dual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Monovary f gAntivary (OrderDual.toDual f) g
theorem Antivary.dual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Antivary f gMonovary (OrderDual.toDual f) g
theorem Monovary.dual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Monovary f gAntivary f (OrderDual.toDual g)
theorem Antivary.dual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Antivary f gMonovary f (OrderDual.toDual g)
theorem MonovaryOn.dual {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g sMonovaryOn (OrderDual.toDual f) (OrderDual.toDual g) s
theorem AntivaryOn.dual {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g sAntivaryOn (OrderDual.toDual f) (OrderDual.toDual g) s
theorem MonovaryOn.dual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g sAntivaryOn (OrderDual.toDual f) g s
theorem AntivaryOn.dual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g sMonovaryOn (OrderDual.toDual f) g s
theorem MonovaryOn.dual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f g sAntivaryOn f (OrderDual.toDual g) s
theorem AntivaryOn.dual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f g sMonovaryOn f (OrderDual.toDual g) s
@[simp]
theorem monovary_toDual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Monovary (OrderDual.toDual f) g Antivary f g
@[simp]
theorem monovary_toDual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Monovary f (OrderDual.toDual g) Antivary f g
@[simp]
theorem antivary_toDual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Antivary (OrderDual.toDual f) g Monovary f g
@[simp]
theorem antivary_toDual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} :
Antivary f (OrderDual.toDual g) Monovary f g
@[simp]
theorem monovaryOn_toDual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn (OrderDual.toDual f) g s AntivaryOn f g s
@[simp]
theorem monovaryOn_toDual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
MonovaryOn f (OrderDual.toDual g) s AntivaryOn f g s
@[simp]
theorem antivaryOn_toDual_left {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn (OrderDual.toDual f) g s MonovaryOn f g s
@[simp]
theorem antivaryOn_toDual_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} :
AntivaryOn f (OrderDual.toDual g) s MonovaryOn f g s
@[simp]
theorem monovary_id_iff {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ια} [inst : PartialOrder ι] :
@[simp]
theorem antivary_id_iff {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ια} [inst : PartialOrder ι] :
@[simp]
theorem monovaryOn_id_iff {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ια} {s : Set ι} [inst : PartialOrder ι] :
@[simp]
theorem antivaryOn_id_iff {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {f : ια} {s : Set ι} [inst : PartialOrder ι] :
theorem Monotone.monovary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} [inst : LinearOrder ι] (hf : Monotone f) (hg : Monotone g) :
theorem Monotone.antivary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} [inst : LinearOrder ι] (hf : Monotone f) (hg : Antitone g) :
theorem Antitone.monovary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} [inst : LinearOrder ι] (hf : Antitone f) (hg : Antitone g) :
theorem Antitone.antivary {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} [inst : LinearOrder ι] (hf : Antitone f) (hg : Monotone g) :
theorem MonotoneOn.monovaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} [inst : LinearOrder ι] (hf : MonotoneOn f s) (hg : MonotoneOn g s) :
theorem MonotoneOn.antivaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} [inst : LinearOrder ι] (hf : MonotoneOn f s) (hg : AntitoneOn g s) :
theorem AntitoneOn.monovaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} [inst : LinearOrder ι] (hf : AntitoneOn f s) (hg : AntitoneOn g s) :
theorem AntitoneOn.antivaryOn {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : Preorder β] {f : ια} {g : ιβ} {s : Set ι} [inst : LinearOrder ι] (hf : AntitoneOn f s) (hg : MonotoneOn g s) :
theorem MonovaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : LinearOrder β] [inst : Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : MonovaryOn f g s) (hg : MonotoneOn g' (g '' s)) :
MonovaryOn f (g' g) s
theorem MonovaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : LinearOrder β] [inst : Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : MonovaryOn f g s) (hg : AntitoneOn g' (g '' s)) :
AntivaryOn f (g' g) s
theorem AntivaryOn.comp_monotoneOn_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : LinearOrder β] [inst : Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : AntivaryOn f g s) (hg : MonotoneOn g' (g '' s)) :
AntivaryOn f (g' g) s
theorem AntivaryOn.comp_antitoneOn_right {ι : Type u_1} {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst : LinearOrder β] [inst : Preorder γ] {f : ια} {g : ιβ} {g' : βγ} {s : Set ι} (h : AntivaryOn f g s) (hg : AntitoneOn g' (g '' s)) :
MonovaryOn f (g' g) s
theorem Monovary.symm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : LinearOrder β] {f : ια} {g : ιβ} (h : Monovary f g) :
theorem Antivary.symm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : LinearOrder β] {f : ια} {g : ιβ} (h : Antivary f g) :
theorem MonovaryOn.symm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} (h : MonovaryOn f g s) :
theorem AntivaryOn.symm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst : LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} (h : AntivaryOn f g s) :
theorem monovary_comm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst : LinearOrder β] {f : ια} {g : ιβ} :
theorem antivary_comm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst : LinearOrder β] {f : ια} {g : ιβ} :
theorem monovaryOn_comm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst : LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} :
theorem antivaryOn_comm {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst : LinearOrder β] {f : ια} {g : ιβ} {s : Set ι} :