Minimum and maximum w.r.t. a filter and on a aet
Main Definitions
This file defines six predicates of the form is_A_B, where A is min, max, or extr,
and B is filter or on.
is_min_filter f l ameans thatf a ≤ f xin somel-neighborhood ofa;is_max_filter f l ameans thatf x ≤ f ain somel-neighborhood ofa;is_extr_filter f l ameansis_min_filter f l aoris_max_filter 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 filterlwithl ⊓ l';is_*_on.on_subset: restrict to a smaller set;is_*_on.inter: replace a setswtihs ∩ t.
Composition
is_*_*.comp_mono: ifxis an extremum forfandgis a monotone function, thenxis an extremum forg ∘ f;is_*_*.comp_antimono: similarly for the case of monotonically decreasingg;is_*_*.bicomp_mono: ifxis an extremum of the same type forfandgand a binary operationopis monotone in both arguments, thenxis an extremum of the same type forλ x, op (f x) (g x).is_*_filter.comp_tendsto: ifg xis an extremum forfw.r.t.l'andtendsto g l l', thenxis an extremum forf ∘ gw.r.t.l.is_*_on.on_preimage: ifg xis an extremum forfons, thenxis an extremum forf ∘ gong ⁻¹' s.
Algebraic operations
is_*_*.add: ifxis an extremum of the same type for two functions, then it is an extremum of the same type for their sum;is_*_*.neg: ifxis an extremum forf, then it is an extremum of the opposite type for-f;is_*_*.sub: ifxis an a minimum forfand a maximum forg, then it is a minimum forf - gand a maximum forg - f;is_*_*.max,is_*_*.min,is_*_*.sup,is_*_*.inf: similarly foris_*_*.addfor pointwisemax,min,sup,inf, respectively.
Miscellaneous definitions
is_*_*_const: any point is both a minimum and maximum for a constant function;is_min/max_*.is_ext: any minimum/maximum point is an extremum;is_*_*.dual,is_*_*.undual: conversion between codomainsαanddual α;
Missing features (TODO)
- Multiplication and division;
is_*_*.bicompl: ifxis a minimum forf,yis a minimum forg, andopis a monotone binary operation, then(x, y)is a minimum foruncurry (bicompl op f g). From this point of view,is_*_*.bicompis a composition- It would be nice to have a tactic that specializes
comp_(anti)monoorbicomp_monobased on a proof of monotonicity of a given (binary) function. The tactic should maintain ametalist 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
is_min_filter f l a means that f a ≤ f x in some l-neighborhood of a
Equations
- is_min_filter f l a = ∀ᶠ (x : α) in l, f a ≤ f x
is_max_filter f l a means that f x ≤ f a in some l-neighborhood of a
Equations
- is_max_filter f l a = ∀ᶠ (x : α) in l, f x ≤ f a
is_extr_filter f l a means is_min_filter f l a or is_max_filter f l a
Equations
- is_extr_filter f l a = (is_min_filter f l a ∨ is_max_filter f l a)
is_min_on f s a means that f a ≤ f x for all x ∈ a. Note that we do not assume a ∈ s.
Equations
- is_min_on f s a = is_min_filter f (filter.principal s) a
is_max_on f s a means that f x ≤ f a for all x ∈ a. Note that we do not assume a ∈ s.
Equations
- is_max_on f s a = is_max_filter f (filter.principal s) a
is_extr_on f s a means is_min_on f s a or is_max_on f s a
Equations
- is_extr_on f s a = is_extr_filter f (filter.principal s) a
theorem
is_extr_on.elim
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α}
{p : Prop} :
is_extr_on f s a → (is_min_on f s a → p) → (is_max_on f s a → p) → p
Conversion to is_extr_*
theorem
is_min_filter.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_min_filter f l a → is_extr_filter f l a
theorem
is_max_filter.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_max_filter f l a → is_extr_filter f l a
theorem
is_min_on.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α} :
is_min_on f s a → is_extr_on f s a
theorem
is_max_on.is_extr
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α} :
is_max_on f s a → is_extr_on f s a
Constant function
theorem
is_min_filter_const
{α : Type u}
{β : Type v}
[preorder β]
{l : filter α}
{a : α}
{b : β} :
is_min_filter (λ (_x : α), b) l a
theorem
is_max_filter_const
{α : Type u}
{β : Type v}
[preorder β]
{l : filter α}
{a : α}
{b : β} :
is_max_filter (λ (_x : α), b) l a
theorem
is_extr_filter_const
{α : Type u}
{β : Type v}
[preorder β]
{l : filter α}
{a : α}
{b : β} :
is_extr_filter (λ (_x : α), b) l a
theorem
is_min_on_const
{α : Type u}
{β : Type v}
[preorder β]
{s : set α}
{a : α}
{b : β} :
is_min_on (λ (_x : α), b) s a
theorem
is_max_on_const
{α : Type u}
{β : Type v}
[preorder β]
{s : set α}
{a : α}
{b : β} :
is_max_on (λ (_x : α), b) s a
theorem
is_extr_on_const
{α : Type u}
{β : Type v}
[preorder β]
{s : set α}
{a : α}
{b : β} :
is_extr_on (λ (_x : α), b) s a
Order dual
theorem
is_min_filter_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_min_filter f l a ↔ is_max_filter f l a
theorem
is_max_filter_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_max_filter f l a ↔ is_min_filter f l a
theorem
is_extr_filter_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α} :
is_extr_filter f l a ↔ is_extr_filter f l a
theorem
is_extr_on_dual_iff
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α} :
is_extr_on f s a ↔ is_extr_on f s a
Operations on the filter/set
theorem
is_min_filter.filter_mono
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
{l' : filter α} :
is_min_filter f l a → l' ≤ l → is_min_filter f l' a
theorem
is_max_filter.filter_mono
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
{l' : filter α} :
is_max_filter f l a → l' ≤ l → is_max_filter f l' a
theorem
is_extr_filter.filter_mono
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
{l' : filter α} :
is_extr_filter f l a → l' ≤ l → is_extr_filter f l' a
theorem
is_min_filter.filter_inf
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
(h : is_min_filter f l a)
(l' : filter α) :
is_min_filter f (l ⊓ l') a
theorem
is_max_filter.filter_inf
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
(h : is_max_filter f l a)
(l' : filter α) :
is_max_filter f (l ⊓ l') a
theorem
is_extr_filter.filter_inf
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{l : filter α}
{a : α}
(h : is_extr_filter f l a)
(l' : filter α) :
is_extr_filter f (l ⊓ l') a
theorem
is_extr_on.on_subset
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α}
{t : set α} :
is_extr_on f t a → s ⊆ t → is_extr_on f s a
theorem
is_extr_on.inter
{α : Type u}
{β : Type v}
[preorder β]
{f : α → β}
{s : set α}
{a : α}
(hf : is_extr_on f s a)
(t : set α) :
is_extr_on f (s ∩ t) a
Composition with (anti)monotone functions
theorem
is_min_filter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_min_filter f l a)
{g : β → γ} :
monotone g → is_min_filter (g ∘ f) l a
theorem
is_max_filter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_max_filter f l a)
{g : β → γ} :
monotone g → is_max_filter (g ∘ f) l a
theorem
is_extr_filter.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_extr_filter f l a)
{g : β → γ} :
monotone g → is_extr_filter (g ∘ f) l a
theorem
is_min_filter.comp_antimono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_min_filter f l a)
{g : β → γ} :
(∀ ⦃x y : β⦄, x ≤ y → g y ≤ g x) → is_max_filter (g ∘ f) l a
theorem
is_max_filter.comp_antimono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_max_filter f l a)
{g : β → γ} :
(∀ ⦃x y : β⦄, x ≤ y → g y ≤ g x) → is_min_filter (g ∘ f) l a
theorem
is_extr_filter.comp_antimono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
(hf : is_extr_filter f l a)
{g : β → γ} :
(∀ ⦃x y : β⦄, x ≤ y → g y ≤ g x) → is_extr_filter (g ∘ f) l a
theorem
is_extr_on.comp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{s : set α}
{a : α}
(hf : is_extr_on f s a)
{g : β → γ} :
monotone g → is_extr_on (g ∘ f) s a
theorem
is_extr_on.comp_antimono
{α : Type u}
{β : Type v}
{γ : Type w}
[preorder β]
[preorder γ]
{f : α → β}
{s : set α}
{a : α}
(hf : is_extr_on f s a)
{g : β → γ} :
(∀ ⦃x y : β⦄, x ≤ y → g y ≤ g x) → is_extr_on (g ∘ f) s a
theorem
is_min_filter.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
[preorder δ]
{op : β → γ → δ}
(hop : (has_le.le ⇒ has_le.le ⇒ has_le.le) op op)
(hf : is_min_filter f l a)
{g : α → γ} :
is_min_filter g l a → is_min_filter (λ (x : α), op (f x) (g x)) l a
theorem
is_max_filter.bicomp_mono
{α : Type u}
{β : Type v}
{γ : Type w}
{δ : Type x}
[preorder β]
[preorder γ]
{f : α → β}
{l : filter α}
{a : α}
[preorder δ]
{op : β → γ → δ}
(hop : (has_le.le ⇒ has_le.le ⇒ has_le.le) op op)
(hf : is_max_filter f l a)
{g : α → γ} :
is_max_filter g l a → is_max_filter (λ (x : α), op (f x) (g x)) l a
Composition with tendsto
theorem
is_min_filter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[preorder β]
{f : α → β}
{l : filter α}
{g : δ → α}
{l' : filter δ}
{b : δ} :
is_min_filter f l (g b) → filter.tendsto g l' l → is_min_filter (f ∘ g) l' b
theorem
is_max_filter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[preorder β]
{f : α → β}
{l : filter α}
{g : δ → α}
{l' : filter δ}
{b : δ} :
is_max_filter f l (g b) → filter.tendsto g l' l → is_max_filter (f ∘ g) l' b
theorem
is_extr_filter.comp_tendsto
{α : Type u}
{β : Type v}
{δ : Type x}
[preorder β]
{f : α → β}
{l : filter α}
{g : δ → α}
{l' : filter δ}
{b : δ} :
is_extr_filter f l (g b) → filter.tendsto g l' l → is_extr_filter (f ∘ g) l' b
theorem
is_extr_on.on_preimage
{α : Type u}
{β : Type v}
{δ : Type x}
[preorder β]
{f : α → β}
{s : set α}
(g : δ → α)
{b : δ} :
is_extr_on f s (g b) → is_extr_on (f ∘ g) (g ⁻¹' s) b
Pointwise addition
theorem
is_min_filter.add
{α : Type u}
{β : Type v}
[ordered_add_comm_monoid β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_min_filter g l a → is_min_filter (λ (x : α), f x + g x) l a
theorem
is_max_filter.add
{α : Type u}
{β : Type v}
[ordered_add_comm_monoid β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_max_filter g l a → is_max_filter (λ (x : α), f x + g x) l a
theorem
is_min_on.add
{α : Type u}
{β : Type v}
[ordered_add_comm_monoid β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.add
{α : Type u}
{β : Type v}
[ordered_add_comm_monoid β]
{f g : α → β}
{a : α}
{s : set α} :
Pointwise negation and subtraction
theorem
is_min_filter.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_max_filter (λ (x : α), -f x) l a
theorem
is_max_filter.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_min_filter (λ (x : α), -f x) l a
theorem
is_extr_filter.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{l : filter α} :
is_extr_filter f l a → is_extr_filter (λ (x : α), -f x) l a
theorem
is_min_on.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{s : set α} :
theorem
is_extr_on.neg
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f : α → β}
{a : α}
{s : set α} :
is_extr_on f s a → is_extr_on (λ (x : α), -f x) s a
theorem
is_min_filter.sub
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_max_filter g l a → is_min_filter (λ (x : α), f x - g x) l a
theorem
is_max_filter.sub
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_min_filter g l a → is_max_filter (λ (x : α), f x - g x) l a
theorem
is_min_on.sub
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.sub
{α : Type u}
{β : Type v}
[ordered_add_comm_group β]
{f g : α → β}
{a : α}
{s : set α} :
Pointwise sup/inf
theorem
is_min_filter.sup
{α : Type u}
{β : Type v}
[semilattice_sup β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_min_filter g l a → is_min_filter (λ (x : α), f x ⊔ g x) l a
theorem
is_max_filter.sup
{α : Type u}
{β : Type v}
[semilattice_sup β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_max_filter g l a → is_max_filter (λ (x : α), f x ⊔ g x) l a
theorem
is_min_on.sup
{α : Type u}
{β : Type v}
[semilattice_sup β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.sup
{α : Type u}
{β : Type v}
[semilattice_sup β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_min_filter.inf
{α : Type u}
{β : Type v}
[semilattice_inf β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_min_filter g l a → is_min_filter (λ (x : α), f x ⊓ g x) l a
theorem
is_max_filter.inf
{α : Type u}
{β : Type v}
[semilattice_inf β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_max_filter g l a → is_max_filter (λ (x : α), f x ⊓ g x) l a
theorem
is_min_on.inf
{α : Type u}
{β : Type v}
[semilattice_inf β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.inf
{α : Type u}
{β : Type v}
[semilattice_inf β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_min_filter.min
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_min_filter g l a → is_min_filter (λ (x : α), min (f x) (g x)) l a
theorem
is_max_filter.min
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_max_filter g l a → is_max_filter (λ (x : α), min (f x) (g x)) l a
theorem
is_min_on.min
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.min
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_min_filter.max
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → is_min_filter g l a → is_min_filter (λ (x : α), max (f x) (g x)) l a
theorem
is_max_filter.max
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → is_max_filter g l a → is_max_filter (λ (x : α), max (f x) (g x)) l a
theorem
is_min_on.max
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
theorem
is_max_on.max
{α : Type u}
{β : Type v}
[decidable_linear_order β]
{f g : α → β}
{a : α}
{s : set α} :
Relation with eventually comparisons of two functions
theorem
filter.eventually_le.is_max_filter
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
g ≤ᶠ[l] f → f a = g a → is_max_filter f l a → is_max_filter g l a
theorem
is_max_filter.congr
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
is_max_filter f l a → f =ᶠ[l] g → f a = g a → is_max_filter g l a
theorem
filter.eventually_eq.is_max_filter_iff
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
f =ᶠ[l] g → f a = g a → (is_max_filter f l a ↔ is_max_filter g l a)
theorem
filter.eventually_le.is_min_filter
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
f ≤ᶠ[l] g → f a = g a → is_min_filter f l a → is_min_filter g l a
theorem
is_min_filter.congr
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
is_min_filter f l a → f =ᶠ[l] g → f a = g a → is_min_filter g l a
theorem
filter.eventually_eq.is_min_filter_iff
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
f =ᶠ[l] g → f a = g a → (is_min_filter f l a ↔ is_min_filter g l a)
theorem
is_extr_filter.congr
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
is_extr_filter f l a → f =ᶠ[l] g → f a = g a → is_extr_filter g l a
theorem
filter.eventually_eq.is_extr_filter_iff
{α : Type u_1}
{β : Type u_2}
[preorder β]
{f g : α → β}
{a : α}
{l : filter α} :
f =ᶠ[l] g → f a = g a → (is_extr_filter f l a ↔ is_extr_filter g l a)