Minimum and maximum w.r.t. a filter and on a aet #
Main Definitions #
This file defines six predicates of the form isAB
, where A
is Min
, Max
, or Extr
,
and B
is Filter
or On
.
isMinFilter f l a
means thatf a ≤ f x≤ f x
in somel
-neighborhood ofa
;isMaxFilter f l a
means thatf x ≤ f a≤ f a
in somel
-neighborhood ofa
;isExtrFilter f l a
meansisMinFilter f l a
orisMaxFilter f l a
.
Similar predicates with on
suffix are particular cases for l = 𝓟 s
.
Main statements #
Change of the filter (set) argument #
is*Filter.filter_mono
: replace the filter with a smaller one;is*Filter.filter_inf
: replace a filterl
withl ⊓ l'⊓ l'
;is*On.on_subset
: restrict to a smaller set;is*Pn.inter
: replace a sets
wtihs ∩ t∩ t
.
Composition #
is**.comp_mono
: ifx
is an extremum forf
andg
is a monotone function, thenx
is an extremum forg ∘ f∘ f
;is**.comp_antitone
: similarly for the case of antitoneg
;is**.bicomp_mono
: ifx
is an extremum of the same type forf
andg
and a binary operationop
is monotone in both arguments, thenx
is an extremum of the same type forfun x => op (f x) (g x)
.is*Filter.comp_tendsto
: ifg x
is an extremum forf
w.r.t.l'
andTendsto g l l'
, thenx
is an extremum forf ∘ g∘ g
w.r.t.l
.is*On.on_preimage
: ifg x
is an extremum forf
ons
, thenx
is an extremum forf ∘ g∘ g
ong ⁻¹' s⁻¹' s
.
Algebraic operations #
is**.add
: ifx
is an extremum of the same type for two functions, then it is an extremum of the same type for their sum;is**.neg
: ifx
is an extremum forf
, then it is an extremum of the opposite type for-f
;is**.sub
: ifx
is an a minimum forf
and a maximum forg
, then it is a minimum forf - g
and a maximum forg - f
;is**.max
,is**.min
,is**.sup
,is**.inf
: similarly foris**.add
for pointwisemax
,min
,sup
,inf
, respectively.
Miscellaneous definitions #
is**_const
: any point is both a minimum and maximum for a constant function;isMin/Max*.isExt
: any minimum/maximum point is an extremum;is**.dual
,is**.undual
: conversion between codomainsα
anddual α
;
Missing features (TODO) #
- Multiplication and division;
is**.bicompl
: ifx
is a minimum forf
,y
is a minimum forg
, andop
is a monotone binary operation, then(x, y)
is a minimum foruncurry (bicompl op f g)
. From this point of view,is**.bicomp
is a composition- It would be nice to have a tactic that specializes
comp_(anti)mono
orbicomp_mono
based on a proof of monotonicity of a given (binary) function. The tactic should maintain ameta
list of known (anti)monotone (binary) functions with their names, as well as a list of special types of filters, and define the missing lemmas once one of these two lists grows.
Definitions #
IsMinFilter f l a
means that f a ≤ f x≤ f x
in some l
-neighborhood of a
Equations
- IsMinFilter f l a = Filter.Eventually (fun x => f a ≤ f x) l
is_maxFilter f l a
means that f x ≤ f a≤ f a
in some l
-neighborhood of a
Equations
- IsMaxFilter f l a = Filter.Eventually (fun x => f x ≤ f a) l
IsExtrFilter f l a
means IsMinFilter f l a
or IsMaxFilter f l a
Equations
- IsExtrFilter f l a = (IsMinFilter f l a ∨ IsMaxFilter f l a)
theorem
IsMinFilter.tendsto_principal_Ici
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
(h : IsMinFilter f l a)
:
Filter.Tendsto f l (Filter.principal (Set.Ici (f a)))
theorem
IsMaxFilter.tendsto_principal_Iic
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
(h : IsMaxFilter f l a)
:
Filter.Tendsto f l (Filter.principal (Set.Iic (f a)))
Conversion to IsExtr*
#
theorem
IsMinFilter.isExtr
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMinFilter f l a → IsExtrFilter f l a
theorem
IsMaxFilter.isExtr
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMaxFilter f l a → IsExtrFilter f l a
Constant function #
theorem
isMinFilter_const
{α : Type u}
{β : Type v}
[inst : Preorder β]
{l : Filter α}
{a : α}
{b : β}
:
IsMinFilter (fun x => b) l a
theorem
isMaxFilter_const
{α : Type u}
{β : Type v}
[inst : Preorder β]
{l : Filter α}
{a : α}
{b : β}
:
IsMaxFilter (fun x => b) l a
theorem
isExtrFilter_const
{α : Type u}
{β : Type v}
[inst : Preorder β]
{l : Filter α}
{a : α}
{b : β}
:
IsExtrFilter (fun x => b) l a
Order dual #
theorem
isMinFilter_dual_iff
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMinFilter (↑OrderDual.toDual ∘ f) l a ↔ IsMaxFilter f l a
theorem
isMaxFilter_dual_iff
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMaxFilter (↑OrderDual.toDual ∘ f) l a ↔ IsMinFilter f l a
theorem
isExtrFilter_dual_iff
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsExtrFilter (↑OrderDual.toDual ∘ f) l a ↔ IsExtrFilter f l a
theorem
IsMaxFilter.dual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMaxFilter f l a → IsMinFilter (↑OrderDual.toDual ∘ f) l a
Alias of the reverse direction of isMinFilter_dual_iff
.
theorem
IsMinFilter.undual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMinFilter (↑OrderDual.toDual ∘ f) l a → IsMaxFilter f l a
Alias of the forward direction of isMinFilter_dual_iff
.
theorem
IsMaxFilter.undual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMaxFilter (↑OrderDual.toDual ∘ f) l a → IsMinFilter f l a
Alias of the forward direction of isMaxFilter_dual_iff
.
theorem
IsMinFilter.dual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsMinFilter f l a → IsMaxFilter (↑OrderDual.toDual ∘ f) l a
Alias of the reverse direction of isMaxFilter_dual_iff
.
theorem
IsExtrFilter.undual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsExtrFilter (↑OrderDual.toDual ∘ f) l a → IsExtrFilter f l a
Alias of the forward direction of isExtrFilter_dual_iff
.
theorem
IsExtrFilter.dual
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
:
IsExtrFilter f l a → IsExtrFilter (↑OrderDual.toDual ∘ f) l a
Alias of the reverse direction of isExtrFilter_dual_iff
.
Operations on the filter/set #
theorem
IsMinFilter.filter_mono
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
{l' : Filter α}
(h : IsMinFilter f l a)
(hl : l' ≤ l)
:
IsMinFilter f l' a
theorem
IsMaxFilter.filter_mono
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
{l' : Filter α}
(h : IsMaxFilter f l a)
(hl : l' ≤ l)
:
IsMaxFilter f l' a
theorem
IsExtrFilter.filter_mono
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
{l' : Filter α}
(h : IsExtrFilter f l a)
(hl : l' ≤ l)
:
IsExtrFilter f l' a
theorem
IsMinFilter.filter_inf
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
(h : IsMinFilter f l a)
(l' : Filter α)
:
IsMinFilter f (l ⊓ l') a
theorem
IsMaxFilter.filter_inf
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
(h : IsMaxFilter f l a)
(l' : Filter α)
:
IsMaxFilter f (l ⊓ l') a
theorem
IsExtrFilter.filter_inf
{α : Type u}
{β : Type v}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{a : α}
(h : IsExtrFilter f l a)
(l' : Filter α)
:
IsExtrFilter f (l ⊓ l') a
Composition with (anti)monotone functions #
theorem
IsMinFilter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsMinFilter f l a)
{g : β → γ}
(hg : Monotone g)
:
IsMinFilter (g ∘ f) l a
theorem
IsMaxFilter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsMaxFilter f l a)
{g : β → γ}
(hg : Monotone g)
:
IsMaxFilter (g ∘ f) l a
theorem
IsExtrFilter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsExtrFilter f l a)
{g : β → γ}
(hg : Monotone g)
:
IsExtrFilter (g ∘ f) l a
theorem
IsMinFilter.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsMinFilter f l a)
{g : β → γ}
(hg : Antitone g)
:
IsMaxFilter (g ∘ f) l a
theorem
IsMaxFilter.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsMaxFilter f l a)
{g : β → γ}
(hg : Antitone g)
:
IsMinFilter (g ∘ f) l a
theorem
IsExtrFilter.comp_antitone
{α : Type u}
{β : Type v}
{γ : Type w}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
(hf : IsExtrFilter f l a)
{g : β → γ}
(hg : Antitone g)
:
IsExtrFilter (g ∘ f) l a
theorem
IsMinFilter.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
[inst : Preorder δ]
{op : β → γ → δ}
(hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op)
(hf : IsMinFilter f l a)
{g : α → γ}
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => op (f x) (g x)) l a
theorem
IsMaxFilter.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{l : Filter α}
{a : α}
[inst : Preorder δ]
{op : β → γ → δ}
(hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op)
(hf : IsMaxFilter f l a)
{g : α → γ}
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => op (f x) (g x)) l a
theorem
IsMinOn.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
[inst : Preorder δ]
{op : β → γ → δ}
(hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op)
(hf : IsMinOn f s a)
{g : α → γ}
(hg : IsMinOn g s a)
:
IsMinOn (fun x => op (f x) (g x)) s a
theorem
IsMaxOn.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[inst : Preorder β]
[inst : Preorder γ]
{f : α → β}
{s : Set α}
{a : α}
[inst : Preorder δ]
{op : β → γ → δ}
(hop : ((fun x x_1 => x ≤ x_1) ⇒ (fun x x_1 => x ≤ x_1) ⇒ fun x x_1 => x ≤ x_1) op op)
(hf : IsMaxOn f s a)
{g : α → γ}
(hg : IsMaxOn g s a)
:
IsMaxOn (fun x => op (f x) (g x)) s a
Composition with Tendsto
#
theorem
IsMinFilter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{g : δ → α}
{l' : Filter δ}
{b : δ}
(hf : IsMinFilter f l (g b))
(hg : Filter.Tendsto g l' l)
:
IsMinFilter (f ∘ g) l' b
theorem
IsMaxFilter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{g : δ → α}
{l' : Filter δ}
{b : δ}
(hf : IsMaxFilter f l (g b))
(hg : Filter.Tendsto g l' l)
:
IsMaxFilter (f ∘ g) l' b
theorem
IsExtrFilter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[inst : Preorder β]
{f : α → β}
{l : Filter α}
{g : δ → α}
{l' : Filter δ}
{b : δ}
(hf : IsExtrFilter f l (g b))
(hg : Filter.Tendsto g l' l)
:
IsExtrFilter (f ∘ g) l' b
Pointwise addition #
theorem
IsMinFilter.add
{α : Type u}
{β : Type v}
[inst : OrderedAddCommMonoid β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => f x + g x) l a
theorem
IsMaxFilter.add
{α : Type u}
{β : Type v}
[inst : OrderedAddCommMonoid β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => f x + g x) l a
Pointwise negation and subtraction #
theorem
IsMinFilter.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
:
IsMaxFilter (fun x => -f x) l a
theorem
IsMaxFilter.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
:
IsMinFilter (fun x => -f x) l a
theorem
IsExtrFilter.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{l : Filter α}
(hf : IsExtrFilter f l a)
:
IsExtrFilter (fun x => -f x) l a
theorem
IsMinOn.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsMinOn f s a)
:
theorem
IsMaxOn.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsMaxOn f s a)
:
theorem
IsExtrOn.neg
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{a : α}
{s : Set α}
(hf : IsExtrOn f s a)
:
theorem
IsMinFilter.sub
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMinFilter (fun x => f x - g x) l a
theorem
IsMaxFilter.sub
{α : Type u}
{β : Type v}
[inst : OrderedAddCommGroup β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMinFilter g l a)
:
IsMaxFilter (fun x => f x - g x) l a
theorem
IsMinFilter.sup
{α : Type u}
{β : Type v}
[inst : SemilatticeSup β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => f x ⊔ g x) l a
theorem
IsMaxFilter.sup
{α : Type u}
{β : Type v}
[inst : SemilatticeSup β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => f x ⊔ g x) l a
theorem
IsMinFilter.inf
{α : Type u}
{β : Type v}
[inst : SemilatticeInf β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => f x ⊓ g x) l a
theorem
IsMaxFilter.inf
{α : Type u}
{β : Type v}
[inst : SemilatticeInf β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => f x ⊓ g x) l a
theorem
IsMinFilter.min
{α : Type u}
{β : Type v}
[inst : LinearOrder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => min (f x) (g x)) l a
theorem
IsMaxFilter.min
{α : Type u}
{β : Type v}
[inst : LinearOrder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => min (f x) (g x)) l a
theorem
IsMinFilter.max
{α : Type u}
{β : Type v}
[inst : LinearOrder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMinFilter f l a)
(hg : IsMinFilter g l a)
:
IsMinFilter (fun x => max (f x) (g x)) l a
theorem
IsMaxFilter.max
{α : Type u}
{β : Type v}
[inst : LinearOrder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hf : IsMaxFilter f l a)
(hg : IsMaxFilter g l a)
:
IsMaxFilter (fun x => max (f x) (g x)) l a
Relation with eventually
comparisons of two functions #
theorem
Filter.EventuallyLE.isMaxFilter
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hle : g ≤ᶠ[l] f)
(hfga : f a = g a)
(h : IsMaxFilter f l a)
:
IsMaxFilter g l a
theorem
IsMaxFilter.congr
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(h : IsMaxFilter f l a)
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsMaxFilter g l a
theorem
Filter.EventuallyEq.isMaxFilter_iff
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsMaxFilter f l a ↔ IsMaxFilter g l a
theorem
Filter.EventuallyLE.isMinFilter
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(hle : f ≤ᶠ[l] g)
(hfga : f a = g a)
(h : IsMinFilter f l a)
:
IsMinFilter g l a
theorem
IsMinFilter.congr
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(h : IsMinFilter f l a)
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsMinFilter g l a
theorem
Filter.EventuallyEq.isMinFilter_iff
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsMinFilter f l a ↔ IsMinFilter g l a
theorem
IsExtrFilter.congr
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(h : IsExtrFilter f l a)
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsExtrFilter g l a
theorem
Filter.EventuallyEq.isExtrFilter_iff
{α : Type u_1}
{β : Type u_2}
[inst : Preorder β]
{f : α → β}
{g : α → β}
{a : α}
{l : Filter α}
(heq : f =ᶠ[l] g)
(hfga : f a = g a)
:
IsExtrFilter f l a ↔ IsExtrFilter g l a
isMaxOn
/isMinOn
imply csupᵢ
/cinfᵢ
#
theorem
IsMaxOn.supᵢ_eq
{α : Type u}
{β : Type v}
[inst : ConditionallyCompleteLinearOrder α]
{f : β → α}
{s : Set β}
{x₀ : β}
(hx₀ : x₀ ∈ s)
(h : IsMaxOn f s x₀)
:
(⨆ x, f ↑x) = f x₀
theorem
IsMinOn.infᵢ_eq
{α : Type u}
{β : Type v}
[inst : ConditionallyCompleteLinearOrder α]
{f : β → α}
{s : Set β}
{x₀ : β}
(hx₀ : x₀ ∈ s)
(h : IsMinOn f s x₀)
:
(⨅ x, f ↑x) = f x₀