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 a
means thatf a ≤ f x
in somel
-neighborhood ofa
;is_max_filter f l a
means thatf x ≤ f a
in somel
-neighborhood ofa
;is_extr_filter f l a
meansis_min_filter f l a
oris_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 filterl
withl ⊓ l'
;is_*_on.on_subset
: restrict to a smaller set;is_*_on.inter
: replace a sets
wtihs ∩ t
.
Composition #
is_*_*.comp_mono
: ifx
is an extremum forf
andg
is a monotone function, thenx
is an extremum forg ∘ 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 forλ 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
w.r.t.l
.is_*_on.on_preimage
: ifg x
is an extremum forf
ons
, thenx
is an extremum forf ∘ g
ong ⁻¹' 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;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
: 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 #
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
Conversion to is_extr_*
#
Constant function #
Order dual #
Alias of the forward direction of is_min_filter_dual_iff
.
Alias of the reverse direction of is_min_filter_dual_iff
.
Alias of the forward direction of is_max_filter_dual_iff
.
Alias of the reverse direction of is_max_filter_dual_iff
.
Alias of the forward direction of is_extr_filter_dual_iff
.
Alias of the reverse direction of is_extr_filter_dual_iff
.
Alias of the forward direction of is_min_on_dual_iff
.
Alias of the reverse direction of is_min_on_dual_iff
.
Alias of the forward direction of is_max_on_dual_iff
.
Alias of the reverse direction of is_max_on_dual_iff
.
Alias of the reverse direction of is_extr_on_dual_iff
.
Alias of the forward direction of is_extr_on_dual_iff
.