mathlib3 documentation

order.monotone.monovary

Monovariance of functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : ι β) :
Prop

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 : ι β) :
Prop

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

Equations
def monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) (s : set ι) :
Prop

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

Equations
def antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (g : ι β) (s : set ι) :
Prop

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

Equations
@[protected]
theorem monovary.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : monovary f g) (s : set ι) :
@[protected]
theorem antivary.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} (h : antivary f g) (s : set ι) :
@[simp]
theorem monovary_on.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem antivary_on.empty {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem monovary_on_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem antivary_on_univ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[protected]
theorem monovary_on.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s t : set ι} (hst : s t) (h : monovary_on f g t) :
@[protected]
theorem antivary_on.subset {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s t : set ι} (hst : s t) (h : antivary_on 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 monovary_on_self {ι : Type u_1} {α : Type u_3} [preorder α] (f : ι α) (s : set ι) :
@[protected]
theorem subsingleton.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) :
@[protected]
theorem subsingleton.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) :
@[protected]
theorem subsingleton.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) (s : set ι) :
@[protected]
theorem subsingleton.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] [subsingleton ι] (f : ι α) (g : ι β) (s : set ι) :
theorem monovary_on_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) (s : set ι) :
theorem antivary_on_const_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (g : ι β) (a : α) (s : set ι) :
theorem monovary_on_const_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] (f : ι α) (b : β) (s : set ι) :
theorem antivary_on_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 : ι' ι) :
monovary (f k) (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 : ι' ι) :
antivary (f k) (g k)
theorem monovary_on.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} (h : monovary_on f g s) (k : ι' ι) :
monovary_on (f k) (g k) (k ⁻¹' s)
theorem antivary_on.comp_right {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} (h : antivary_on f g s) (k : ι' ι) :
antivary_on (f k) (g k) (k ⁻¹' s)
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') :
monovary (f' f) g
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') :
antivary (f' f) g
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') :
antivary (f' f) g
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') :
monovary (f' f) g
theorem monovary_on.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 : monovary_on f g s) (hf : monotone f') :
monovary_on (f' f) g s
theorem monovary_on.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 : monovary_on f g s) (hf : antitone f') :
antivary_on (f' f) g s
theorem antivary_on.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 : antivary_on f g s) (hf : monotone f') :
antivary_on (f' f) g s
theorem antivary_on.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 : antivary_on f g s) (hf : antitone f') :
monovary_on (f' f) g s
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 monovary_on.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
theorem antivary_on.dual {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
theorem monovary_on.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
theorem antivary_on.dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
theorem monovary_on.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
theorem antivary_on.dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
@[simp]
theorem monovary_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem monovary_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem antivary_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem antivary_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} :
@[simp]
theorem monovary_on_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
@[simp]
theorem monovary_on_to_dual_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
@[simp]
theorem antivary_on_to_dual_left {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} :
@[simp]
theorem antivary_on_to_dual_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 : ι α} [partial_order ι] :
@[simp]
theorem antivary_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α} [partial_order ι] :
@[simp]
theorem monovary_on_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α} {s : set ι} [partial_order ι] :
@[simp]
theorem antivary_on_id_iff {ι : Type u_1} {α : Type u_3} [preorder α] {f : ι α} {s : set ι} [partial_order ι] :
@[protected]
theorem monotone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : monotone f) (hg : monotone g) :
@[protected]
theorem monotone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : monotone f) (hg : antitone g) :
@[protected]
theorem antitone.monovary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : antitone f) (hg : antitone g) :
@[protected]
theorem antitone.antivary {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} [linear_order ι] (hf : antitone f) (hg : monotone g) :
@[protected]
theorem monotone_on.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : monotone_on f s) (hg : monotone_on g s) :
@[protected]
theorem monotone_on.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : monotone_on f s) (hg : antitone_on g s) :
@[protected]
theorem antitone_on.monovary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : antitone_on f s) (hg : antitone_on g s) :
@[protected]
theorem antitone_on.antivary_on {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [preorder β] {f : ι α} {g : ι β} {s : set ι} [linear_order ι] (hf : antitone_on f s) (hg : monotone_on g s) :
theorem monovary_on.comp_monotone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : monovary_on f g s) (hg : monotone_on g' (g '' s)) :
monovary_on f (g' g) s
theorem monovary_on.comp_antitone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : monovary_on f g s) (hg : antitone_on g' (g '' s)) :
antivary_on f (g' g) s
theorem antivary_on.comp_monotone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : antivary_on f g s) (hg : monotone_on g' (g '' s)) :
antivary_on f (g' g) s
theorem antivary_on.comp_antitone_on_right {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [preorder α] [linear_order β] [preorder γ] {f : ι α} {g : ι β} {g' : β γ} {s : set ι} (h : antivary_on f g s) (hg : antitone_on g' (g '' s)) :
monovary_on f (g' g) s
@[protected]
theorem monovary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} (h : monovary f g) :
@[protected]
theorem antivary.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} (h : antivary f g) :
@[protected]
theorem monovary_on.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} (h : monovary_on f g s) :
@[protected]
theorem antivary_on.symm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [preorder α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} (h : antivary_on f g s) :
@[protected]
theorem monovary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} :
@[protected]
theorem antivary_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} :
@[protected]
theorem monovary_on_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} :
@[protected]
theorem antivary_on_comm {ι : Type u_1} {α : Type u_3} {β : Type u_4} [linear_order α] [linear_order β] {f : ι α} {g : ι β} {s : set ι} :