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 #
monovary f g:fmonovaries withg. Ifg i < g j, thenf i ≤ f j.antivary f g:fantivaries withg. Ifg i < g j, thenf j ≤ f i.monovary_on f g s:fmonovaries withgons.monovary_on f g s:fantivaries withgons.
@[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) :
monovary_on f g s
@[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) :
antivary_on f g s
theorem
monovary_const_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(g : ι → β)
(a : α) :
monovary (function.const ι a) g
theorem
antivary_const_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(g : ι → β)
(a : α) :
antivary (function.const ι a) g
theorem
monovary_const_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(f : ι → α)
(b : β) :
monovary f (function.const ι b)
theorem
antivary_const_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(f : ι → α)
(b : β) :
antivary f (function.const ι b)
theorem
monovary_on_self
{ι : Type u_1}
{α : Type u_3}
[preorder α]
(f : ι → α)
(s : set ι) :
monovary_on f f s
@[protected]
theorem
subsingleton.monovary_on
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
[subsingleton ι]
(f : ι → α)
(g : ι → β)
(s : set ι) :
monovary_on f g s
@[protected]
theorem
subsingleton.antivary_on
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
[subsingleton ι]
(f : ι → α)
(g : ι → β)
(s : set ι) :
antivary_on f g s
theorem
monovary_on_const_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(g : ι → β)
(a : α)
(s : set ι) :
monovary_on (function.const ι a) g s
theorem
antivary_on_const_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(g : ι → β)
(a : α)
(s : set ι) :
antivary_on (function.const ι a) g s
theorem
monovary_on_const_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(f : ι → α)
(b : β)
(s : set ι) :
monovary_on f (function.const ι b) s
theorem
antivary_on_const_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
(f : ι → α)
(b : β)
(s : set ι) :
antivary_on f (function.const ι b) s
theorem
monovary_on.dual
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
monovary_on f g s → monovary_on (⇑order_dual.to_dual ∘ f) (⇑order_dual.to_dual ∘ g) s
theorem
antivary_on.dual
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on f g s → antivary_on (⇑order_dual.to_dual ∘ f) (⇑order_dual.to_dual ∘ g) s
theorem
monovary_on.dual_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
monovary_on f g s → antivary_on (⇑order_dual.to_dual ∘ f) g s
theorem
antivary_on.dual_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on f g s → monovary_on (⇑order_dual.to_dual ∘ f) g s
theorem
monovary_on.dual_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
monovary_on f g s → antivary_on f (⇑order_dual.to_dual ∘ g) s
theorem
antivary_on.dual_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on f g s → monovary_on f (⇑order_dual.to_dual ∘ g) s
@[simp]
theorem
monovary_on_to_dual_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
monovary_on (⇑order_dual.to_dual ∘ f) g s ↔ antivary_on f g s
@[simp]
theorem
monovary_on_to_dual_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
monovary_on f (⇑order_dual.to_dual ∘ g) s ↔ antivary_on f g s
@[simp]
theorem
antivary_on_to_dual_left
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on (⇑order_dual.to_dual ∘ f) g s ↔ monovary_on f g s
@[simp]
theorem
antivary_on_to_dual_right
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[preorder β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on f (⇑order_dual.to_dual ∘ g) s ↔ monovary_on f g s
@[simp]
theorem
monovary_on_id_iff
{ι : Type u_1}
{α : Type u_3}
[preorder α]
{f : ι → α}
{s : set ι}
[partial_order ι] :
monovary_on f id s ↔ monotone_on f s
@[simp]
theorem
antivary_on_id_iff
{ι : Type u_1}
{α : Type u_3}
[preorder α]
{f : ι → α}
{s : set ι}
[partial_order ι] :
antivary_on f id s ↔ antitone_on f s
@[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) :
monovary_on f 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) :
antivary_on f 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) :
monovary_on f 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) :
antivary_on f 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_on.symm
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[preorder α]
[linear_order β]
{f : ι → α}
{g : ι → β}
{s : set ι}
(h : monovary_on f g s) :
monovary_on g f 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) :
antivary_on g f 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 ι} :
monovary_on f g s ↔ monovary_on g f s
@[protected]
theorem
antivary_on_comm
{ι : Type u_1}
{α : Type u_3}
{β : Type u_4}
[linear_order α]
[linear_order β]
{f : ι → α}
{g : ι → β}
{s : set ι} :
antivary_on f g s ↔ antivary_on g f s