Mathlib.Order.Filter.Extr

IsMinFilter definition

: Prop

Full source

/-- `IsMinFilter f l a` means that `f a ≤ f x` for all `x` in some `l`-neighborhood of `a` -/
def IsMinFilter : Prop :=
  ∀ᶠ x in l, f a ≤ f x

Local minimum of a function with respect to a filter

Informal description

A point $ a $ is called a *local minimum of $ f $ with respect to the filter $ l $* if there exists a neighborhood of $ a $ in the filter $ l $ such that for all $ x $ in this neighborhood, $ f(a) \leq f(x) $.

IsMaxFilter definition

: Prop

Full source

/-- `is_maxFilter f l a` means that `f x ≤ f a` for all `x` in some `l`-neighborhood of `a` -/
def IsMaxFilter : Prop :=
  ∀ᶠ x in l, f x ≤ f a

Local maximum of a function with respect to a filter

Informal description

A point $ a $ is called a *local maximum of $ f $ with respect to the filter $ l $* if there exists a neighborhood of $ a $ in the filter $ l $ such that for all $ x $ in this neighborhood, $ f(x) \leq f(a) $.

IsExtrFilter definition

: Prop

Full source

/-- `IsExtrFilter f l a` means `IsMinFilter f l a` or `IsMaxFilter f l a` -/
def IsExtrFilter : Prop :=
  IsMinFilterIsMinFilter f l a ∨ IsMaxFilter f l a

Local extremum of a function with respect to a filter

Informal description

A point $ a $ is called an *extremum of $ f $ with respect to the filter $ l $* if it is either a local minimum or a local maximum of $ f $ with respect to $ l $. That is, there exists a neighborhood of $ a $ in the filter $ l $ such that either $ f(a) \leq f(x) $ for all $ x $ in this neighborhood (minimum) or $ f(x) \leq f(a) $ for all $ x $ in this neighborhood (maximum).

IsMinOn definition

Full source

/-- `IsMinOn f s a` means that `f a ≤ f x` for all `x ∈ s`. Note that we do not assume `a ∈ s`. -/
def IsMinOn :=
  IsMinFilter f (𝓟 s) a

Minimum of a function on a set

Informal description

A point $ a $ is called a *minimum of $ f $ on the set $ s $* if for all $ x \in s $, $ f(a) \leq f(x) $. Note that $ a $ is not required to be an element of $ s $.

IsMaxOn definition

Full source

/-- `IsMaxOn f s a` means that `f x ≤ f a` for all `x ∈ s`. Note that we do not assume `a ∈ s`. -/
def IsMaxOn :=
  IsMaxFilter f (𝓟 s) a

Maximum of a function on a set

Informal description

A point $ a $ is called a *maximum of $ f $ on the set $ s $* if for all $ x \in s $, $ f(x) \leq f(a) $. Note that $ a $ is not required to be an element of $ s $.

IsExtrOn definition

: Prop

Full source

/-- `IsExtrOn f s a` means `IsMinOn f s a` or `IsMaxOn f s a` -/
def IsExtrOn : Prop :=
  IsExtrFilter f (𝓟 s) a

Extremum of a function on a set

Informal description

A point $ a $ is called an *extremum of $ f $ on the set $ s $* if it is either a minimum or a maximum of $ f $ on $ s $. That is, either $ f(a) \leq f(x) $ for all $ x \in s $ (minimum) or $ f(x) \leq f(a) $ for all $ x \in s $ (maximum).

IsExtrOn.elim theorem

{p : Prop} : IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p

Full source

theorem IsExtrOn.elim {p : Prop} : IsExtrOn f s a → (IsMinOn f s a → p) → (IsMaxOn f s a → p) → p :=
  Or.elim

Case Analysis for Extremum Points on a Set

Informal description

Given a function $f$ defined on a set $s$, a point $a$, and a proposition $p$, if $a$ is an extremum of $f$ on $s$ (i.e., either a minimum or a maximum), then to prove $p$ it suffices to show that $p$ holds under both the assumption that $a$ is a minimum of $f$ on $s$ and the assumption that $a$ is a maximum of $f$ on $s$.

isMinOn_iff theorem

: IsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x

Full source

theorem isMinOn_iff : IsMinOnIsMinOn f s a ↔ ∀ x ∈ s, f a ≤ f x :=
  Iff.rfl

Characterization of Minimum on a Set

Informal description

For a function $f$ defined on a set $s$ and a point $a$, the following are equivalent: 1. $a$ is a minimum of $f$ on $s$ (i.e., $f(a) \leq f(x)$ for all $x \in s$) 2. For every $x \in s$, we have $f(a) \leq f(x)$.

isMaxOn_iff theorem

: IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a

Full source

theorem isMaxOn_iff : IsMaxOnIsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a :=
  Iff.rfl

Characterization of Maximum on a Set

Informal description

For a function $f$ defined on a set $s$ and a point $a$, the following are equivalent: 1. $a$ is a maximum of $f$ on $s$ (i.e., $f(x) \leq f(a)$ for all $x \in s$) 2. For every $x \in s$, we have $f(x) \leq f(a)$.

isMinOn_univ_iff theorem

: IsMinOn f univ a ↔ ∀ x, f a ≤ f x

Full source

theorem isMinOn_univ_iff : IsMinOnIsMinOn f univ a ↔ ∀ x, f a ≤ f x :=
  univ_subset_iff.trans eq_univ_iff_forall

Characterization of Global Minimum: $a$ is a global minimum of $f$ if and only if $f(a) \leq f(x)$ for all $x$

Informal description

For a function $f$ and a point $a$, the following are equivalent: 1. $a$ is a minimum of $f$ on the universal set (i.e., $f(a) \leq f(x)$ for all $x$) 2. For every $x$, we have $f(a) \leq f(x)$.

isMaxOn_univ_iff theorem

: IsMaxOn f univ a ↔ ∀ x, f x ≤ f a

Full source

theorem isMaxOn_univ_iff : IsMaxOnIsMaxOn f univ a ↔ ∀ x, f x ≤ f a :=
  univ_subset_iff.trans eq_univ_iff_forall

Characterization of Global Maximum: $\text{IsMaxOn}\, f\, \text{univ}\, a \leftrightarrow \forall x, f(x) \leq f(a)$

Informal description

For a function $f : \alpha \to \beta$ (where $\beta$ has a preorder) and a point $a \in \alpha$, the following are equivalent: 1. $a$ is a maximum of $f$ on the universal set $\text{univ}$ (i.e., $f(x) \leq f(a)$ for all $x \in \alpha$) 2. For every $x \in \alpha$, we have $f(x) \leq f(a)$.

IsMinFilter.tendsto_principal_Ici theorem

(h : IsMinFilter f l a) : Tendsto f l (𝓟 <| Ici (f a))

Full source

theorem IsMinFilter.tendsto_principal_Ici (h : IsMinFilter f l a) : Tendsto f l (𝓟 <| Ici (f a)) :=
  tendsto_principal.2 h

Tendency to Right-Closed Interval at Local Minimum

Informal description

If $a$ is a local minimum of the function $f$ with respect to the filter $l$, then $f$ tends to values in the interval $[f(a), \infty)$ along the filter $l$. In other words, for any neighborhood $U$ of $f(a)$ in the interval $[f(a), \infty)$, there exists a set $S$ in the filter $l$ such that $f(x) \in U$ for all $x \in S$.

IsMaxFilter.tendsto_principal_Iic theorem

(h : IsMaxFilter f l a) : Tendsto f l (𝓟 <| Iic (f a))

Full source

theorem IsMaxFilter.tendsto_principal_Iic (h : IsMaxFilter f l a) : Tendsto f l (𝓟 <| Iic (f a)) :=
  tendsto_principal.2 h

Tendency to Left-Infinite Right-Closed Interval at Local Maximum

Informal description

If $a$ is a local maximum of the function $f$ with respect to the filter $l$, then $f$ tends to values in the interval $(-\infty, f(a)]$ along the filter $l$. In other words, for any neighborhood $U$ of $f(a)$ in the interval $(-\infty, f(a)]$, there exists a set $S$ in the filter $l$ such that $f(x) \in U$ for all $x \in S$.

IsMinFilter.isExtr theorem

: IsMinFilter f l a → IsExtrFilter f l a

Full source

theorem IsMinFilter.isExtr : IsMinFilter f l a → IsExtrFilter f l a :=
  Or.inl

Local Minimum Implies Local Extremum with Respect to a Filter

Informal description

If a point $a$ is a local minimum of a function $f$ with respect to a filter $l$, then $a$ is also a local extremum of $f$ with respect to $l$.

IsMaxFilter.isExtr theorem

: IsMaxFilter f l a → IsExtrFilter f l a

Full source

theorem IsMaxFilter.isExtr : IsMaxFilter f l a → IsExtrFilter f l a :=
  Or.inr

Local Maximum Implies Local Extremum with Respect to a Filter

Informal description

If a point $a$ is a local maximum of a function $f$ with respect to a filter $l$, then $a$ is also a local extremum of $f$ with respect to $l$.

IsMinOn.isExtr theorem

(h : IsMinOn f s a) : IsExtrOn f s a

Full source

theorem IsMinOn.isExtr (h : IsMinOn f s a) : IsExtrOn f s a :=
  IsMinFilter.isExtr h

Minimum on a Set Implies Extremum on the Same Set

Informal description

If a point $a$ is a minimum of a function $f$ on a set $s$ (i.e., $f(a) \leq f(x)$ for all $x \in s$), then $a$ is also an extremum of $f$ on $s$.

IsMaxOn.isExtr theorem

(h : IsMaxOn f s a) : IsExtrOn f s a

Full source

theorem IsMaxOn.isExtr (h : IsMaxOn f s a) : IsExtrOn f s a :=
  IsMaxFilter.isExtr h

Maximum on a Set Implies Extremum on the Same Set

Informal description

If a point $a$ is a maximum of a function $f$ on a set $s$ (i.e., $f(x) \leq f(a)$ for all $x \in s$), then $a$ is also an extremum of $f$ on $s$.

isMinFilter_const theorem

{b : β} : IsMinFilter (fun _ => b) l a

Full source

theorem isMinFilter_const {b : β} : IsMinFilter (fun _ => b) l a :=
  univ_mem' fun _ => le_rfl

Every Point is a Local Minimum for a Constant Function

Informal description

For any constant function $ f(x) = b $ and any filter $ l $, every point $ a $ is a local minimum of $ f $ with respect to $ l $. That is, there exists a neighborhood of $ a $ in $ l $ such that $ b \leq b $ for all $ x $ in this neighborhood.

isMaxFilter_const theorem

{b : β} : IsMaxFilter (fun _ => b) l a

Full source

theorem isMaxFilter_const {b : β} : IsMaxFilter (fun _ => b) l a :=
  univ_mem' fun _ => le_rfl

Every Point is a Local Maximum for a Constant Function

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of a preorder) and any filter $ l $, every point $ a $ is a local maximum of $ f $ with respect to $ l $. That is, there exists a neighborhood of $ a $ in the filter $ l $ such that for all $ x $ in this neighborhood, $ f(x) \leq f(a) $.

isExtrFilter_const theorem

{b : β} : IsExtrFilter (fun _ => b) l a

Full source

theorem isExtrFilter_const {b : β} : IsExtrFilter (fun _ => b) l a :=
  isMinFilter_const.isExtr

Every Point is a Local Extremum for a Constant Function

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of a preordered type $ \beta $) and any filter $ l $ on the domain of $ f $, every point $ a $ is a local extremum of $ f $ with respect to $ l $. That is, there exists a neighborhood of $ a $ in the filter $ l $ such that $ f(a) \leq f(x) $ for all $ x $ in this neighborhood (local minimum) or $ f(x) \leq f(a) $ for all $ x $ in this neighborhood (local maximum).

isMinOn_const theorem

{b : β} : IsMinOn (fun _ => b) s a

Full source

theorem isMinOn_const {b : β} : IsMinOn (fun _ => b) s a :=
  isMinFilter_const

Every Point is a Minimum for a Constant Function on Any Set

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of a preordered type $ \beta $) and any set $ s $, every point $ a $ is a minimum of $ f $ on $ s $. That is, for all $ x \in s $, we have $ b \leq b $.

isMaxOn_const theorem

{b : β} : IsMaxOn (fun _ => b) s a

Full source

theorem isMaxOn_const {b : β} : IsMaxOn (fun _ => b) s a :=
  isMaxFilter_const

Every Point is a Maximum for a Constant Function on Any Set

Informal description

For any constant function $f(x) = b$ (where $b$ is an element of a preorder) and any set $s$, every point $a$ is a maximum of $f$ on $s$. That is, for all $x \in s$, $f(x) \leq f(a)$.

isExtrOn_const theorem

{b : β} : IsExtrOn (fun _ => b) s a

Full source

theorem isExtrOn_const {b : β} : IsExtrOn (fun _ => b) s a :=
  isExtrFilter_const

Every Point is an Extremum for a Constant Function on Any Set

Informal description

For any constant function $f(x) = b$ (where $b$ is an element of a preordered type $\beta$) and any set $s$, every point $a$ is an extremum of $f$ on $s$. That is, either $f(a) \leq f(x)$ for all $x \in s$ (minimum) or $f(x) \leq f(a)$ for all $x \in s$ (maximum).

isMinFilter_dual_iff theorem

: IsMinFilter (toDual ∘ f) l a ↔ IsMaxFilter f l a

Full source

theorem isMinFilter_dual_iff : IsMinFilterIsMinFilter (toDual ∘ f) l a ↔ IsMaxFilter f l a :=
  Iff.rfl

Dual Order Characterization of Local Minima and Maxima: $f$ has a local minimum in the dual order at $a$ if and only if $f$ has a local maximum in the original order at $a$

Informal description

For a function $f$ and a filter $l$ at a point $a$, the composition of $f$ with the order dual map is a local minimum with respect to $l$ at $a$ if and only if $f$ is a local maximum with respect to $l$ at $a$. In other words, $a$ is a local minimum point for $f$ in the dual order if and only if it is a local maximum point for $f$ in the original order.

isMaxFilter_dual_iff theorem

: IsMaxFilter (toDual ∘ f) l a ↔ IsMinFilter f l a

Full source

theorem isMaxFilter_dual_iff : IsMaxFilterIsMaxFilter (toDual ∘ f) l a ↔ IsMinFilter f l a :=
  Iff.rfl

Dual Order Transformation of Local Maxima and Minima

Informal description

For a function $f$ and a filter $l$ at a point $a$, the composition of $f$ with the order dual map is a local maximum with respect to $l$ at $a$ if and only if $f$ is a local minimum with respect to $l$ at $a$.

isExtrFilter_dual_iff theorem

: IsExtrFilter (toDual ∘ f) l a ↔ IsExtrFilter f l a

Full source

theorem isExtrFilter_dual_iff : IsExtrFilterIsExtrFilter (toDual ∘ f) l a ↔ IsExtrFilter f l a :=
  or_comm

Extremum Duality: $\text{toDual} \circ f$ vs. $f$ with respect to a filter

Informal description

For a function $f$ and a filter $l$ at a point $a$, the composition of $f$ with the order dual map is an extremum with respect to $l$ at $a$ if and only if $f$ itself is an extremum with respect to $l$ at $a$. In other words, $a$ is an extremum of $\text{toDual} \circ f$ with respect to $l$ if and only if $a$ is an extremum of $f$ with respect to $l$.

isMinOn_dual_iff theorem

: IsMinOn (toDual ∘ f) s a ↔ IsMaxOn f s a

Full source

theorem isMinOn_dual_iff : IsMinOnIsMinOn (toDual ∘ f) s a ↔ IsMaxOn f s a :=
  Iff.rfl

Minimum in Order Dual Equivalence to Maximum in Original Order

Informal description

For a function $f : \alpha \to \beta$ and a set $s \subseteq \alpha$, the composition of $f$ with the order dual map $\text{toDual} : \beta \to \beta^{\text{op}}$ has a minimum at $a$ on $s$ if and only if $f$ has a maximum at $a$ on $s$. In other words, $a$ is a minimum point of $\text{toDual} \circ f$ on $s$ if and only if $a$ is a maximum point of $f$ on $s$.

isMaxOn_dual_iff theorem

: IsMaxOn (toDual ∘ f) s a ↔ IsMinOn f s a

Full source

theorem isMaxOn_dual_iff : IsMaxOnIsMaxOn (toDual ∘ f) s a ↔ IsMinOn f s a :=
  Iff.rfl

Duality Between Maximum and Minimum on a Set: $\text{IsMaxOn}(\text{toDual} \circ f, s, a) \leftrightarrow \text{IsMinOn}(f, s, a)$

Informal description

For a function $f : \alpha \to \beta$ and a set $s \subseteq \alpha$, a point $a$ is a maximum of the composition $\text{toDual} \circ f$ on $s$ (with respect to the dual order on $\beta$) if and only if $a$ is a minimum of $f$ on $s$ (with respect to the original order on $\beta$). Here, $\text{toDual} : \beta \to \beta^{\text{op}}$ is the identity map that interprets an element of $\beta$ in the dual order, where $x \leq y$ in $\beta^{\text{op}}$ means $y \leq x$ in $\beta$.

isExtrOn_dual_iff theorem

: IsExtrOn (toDual ∘ f) s a ↔ IsExtrOn f s a

Full source

theorem isExtrOn_dual_iff : IsExtrOnIsExtrOn (toDual ∘ f) s a ↔ IsExtrOn f s a :=
  or_comm

Extremum Characterization via Order Dual

Informal description

Let $f$ be a function defined on a set $s$ with values in a preordered type $\alpha$, and let $a \in s$. Then $a$ is an extremum of the composition $\text{toDual} \circ f$ on $s$ if and only if $a$ is an extremum of $f$ on $s$, where $\text{toDual} : \alpha \to \alpha^{\text{op}}$ is the canonical map to the order dual of $\alpha$.

IsMinFilter.filter_mono theorem

(h : IsMinFilter f l a) (hl : l' ≤ l) : IsMinFilter f l' a

Full source

theorem IsMinFilter.filter_mono (h : IsMinFilter f l a) (hl : l' ≤ l) : IsMinFilter f l' a :=
  hl h

Local Minimum is Preserved Under Filter Refinement

Informal description

Let $f$ be a function and $l, l'$ be filters. If $a$ is a local minimum of $f$ with respect to $l$ (i.e., there exists a neighborhood of $a$ in $l$ where $f(a) \leq f(x)$ for all $x$ in this neighborhood), and $l'$ is a finer filter than $l$ (i.e., $l' \leq l$), then $a$ is also a local minimum of $f$ with respect to $l'$.

IsMaxFilter.filter_mono theorem

(h : IsMaxFilter f l a) (hl : l' ≤ l) : IsMaxFilter f l' a

Full source

theorem IsMaxFilter.filter_mono (h : IsMaxFilter f l a) (hl : l' ≤ l) : IsMaxFilter f l' a :=
  hl h

Local Maximum is Preserved Under Filter Refinement

Informal description

Let $f$ be a function and $l, l'$ be filters on a type $\alpha$ with a preorder. If $a$ is a local maximum of $f$ with respect to $l$ (i.e., there exists a neighborhood of $a$ in $l$ where $f(x) \leq f(a)$ for all $x$ in this neighborhood), and $l'$ is a finer filter than $l$ (i.e., $l' \leq l$), then $a$ is also a local maximum of $f$ with respect to $l'$.

IsExtrFilter.filter_mono theorem

(h : IsExtrFilter f l a) (hl : l' ≤ l) : IsExtrFilter f l' a

Full source

theorem IsExtrFilter.filter_mono (h : IsExtrFilter f l a) (hl : l' ≤ l) : IsExtrFilter f l' a :=
  h.elim (fun h => (h.filter_mono hl).isExtr) fun h => (h.filter_mono hl).isExtr

Local Extremum is Preserved Under Filter Refinement

Informal description

Let $f$ be a function defined on a type $\alpha$ with a preorder, and let $l$ and $l'$ be filters on $\alpha$. If $a$ is a local extremum of $f$ with respect to $l$ (i.e., $a$ is either a local minimum or a local maximum of $f$ with respect to $l$), and $l'$ is a finer filter than $l$ (i.e., $l' \leq l$), then $a$ is also a local extremum of $f$ with respect to $l'$.

IsMinFilter.filter_inf theorem

(h : IsMinFilter f l a) (l') : IsMinFilter f (l ⊓ l') a

Full source

theorem IsMinFilter.filter_inf (h : IsMinFilter f l a) (l') : IsMinFilter f (l ⊓ l') a :=
  h.filter_mono inf_le_left

Local Minimum is Preserved Under Filter Infimum

Informal description

Let $f$ be a function and $l, l'$ be filters on a type $\alpha$ with a preorder. If $a$ is a local minimum of $f$ with respect to $l$ (i.e., there exists a neighborhood of $a$ in $l$ where $f(a) \leq f(x)$ for all $x$ in this neighborhood), then $a$ is also a local minimum of $f$ with respect to the infimum filter $l \sqcap l'$.

IsMaxFilter.filter_inf theorem

(h : IsMaxFilter f l a) (l') : IsMaxFilter f (l ⊓ l') a

Full source

theorem IsMaxFilter.filter_inf (h : IsMaxFilter f l a) (l') : IsMaxFilter f (l ⊓ l') a :=
  h.filter_mono inf_le_left

Local Maximum is Preserved Under Filter Infimum

Informal description

Let $f$ be a function defined on a type $\alpha$ with a preorder, and let $l$ and $l'$ be filters on $\alpha$. If $a$ is a local maximum of $f$ with respect to $l$ (i.e., there exists a neighborhood of $a$ in $l$ where $f(x) \leq f(a)$ for all $x$ in this neighborhood), then $a$ is also a local maximum of $f$ with respect to the infimum filter $l \sqcap l'$.

IsExtrFilter.filter_inf theorem

(h : IsExtrFilter f l a) (l') : IsExtrFilter f (l ⊓ l') a

Full source

theorem IsExtrFilter.filter_inf (h : IsExtrFilter f l a) (l') : IsExtrFilter f (l ⊓ l') a :=
  h.filter_mono inf_le_left

Local Extremum is Preserved Under Filter Infimum

Informal description

Let $f : \alpha \to \beta$ be a function between types with a preorder on $\beta$, and let $l$ and $l'$ be filters on $\alpha$. If $a$ is a local extremum of $f$ with respect to $l$ (i.e., $a$ is either a local minimum or a local maximum of $f$ with respect to $l$), then $a$ is also a local extremum of $f$ with respect to the infimum filter $l \sqcap l'$.

IsMinOn.on_subset theorem

(hf : IsMinOn f t a) (h : s ⊆ t) : IsMinOn f s a

Full source

theorem IsMinOn.on_subset (hf : IsMinOn f t a) (h : s ⊆ t) : IsMinOn f s a :=
  hf.filter_mono <| principal_mono.2 h

Minimum on Subset Property

Informal description

Let $f : \alpha \to \beta$ be a function between types with a preorder on $\beta$, and let $s, t$ be subsets of $\alpha$ such that $s \subseteq t$. If $a$ is a minimum of $f$ on $t$ (i.e., $f(a) \leq f(x)$ for all $x \in t$), then $a$ is also a minimum of $f$ on $s$.

IsMaxOn.on_subset theorem

(hf : IsMaxOn f t a) (h : s ⊆ t) : IsMaxOn f s a

Full source

theorem IsMaxOn.on_subset (hf : IsMaxOn f t a) (h : s ⊆ t) : IsMaxOn f s a :=
  hf.filter_mono <| principal_mono.2 h

Restriction of Maximum to Subset

Informal description

Let $f$ be a function defined on a type with a preorder, and let $s \subseteq t$ be subsets of the domain. If $a$ is a maximum of $f$ on $t$ (i.e., $f(x) \leq f(a)$ for all $x \in t$), then $a$ is also a maximum of $f$ on $s$.

IsExtrOn.on_subset theorem

(hf : IsExtrOn f t a) (h : s ⊆ t) : IsExtrOn f s a

Full source

theorem IsExtrOn.on_subset (hf : IsExtrOn f t a) (h : s ⊆ t) : IsExtrOn f s a :=
  hf.filter_mono <| principal_mono.2 h

Extremum Preservation Under Subset Restriction

Informal description

Let $f$ be a function defined on a type $\alpha$ with a preorder, and let $s$ and $t$ be subsets of $\alpha$ such that $s \subseteq t$. If $a$ is an extremum of $f$ on $t$ (i.e., $a$ is either a minimum or a maximum of $f$ on $t$), then $a$ is also an extremum of $f$ on $s$.

IsMinOn.inter theorem

(hf : IsMinOn f s a) (t) : IsMinOn f (s ∩ t) a

Full source

theorem IsMinOn.inter (hf : IsMinOn f s a) (t) : IsMinOn f (s ∩ t) a :=
  hf.on_subset inter_subset_left

Minimum Preservation Under Intersection: $a$ is minimum on $s \cap t$ if minimum on $s$

Informal description

Let $f : \alpha \to \beta$ be a function between types with a preorder on $\beta$, and let $s, t$ be subsets of $\alpha$. If $a$ is a minimum of $f$ on $s$ (i.e., $f(a) \leq f(x)$ for all $x \in s$), then $a$ is also a minimum of $f$ on the intersection $s \cap t$.

IsMaxOn.inter theorem

(hf : IsMaxOn f s a) (t) : IsMaxOn f (s ∩ t) a

Full source

theorem IsMaxOn.inter (hf : IsMaxOn f s a) (t) : IsMaxOn f (s ∩ t) a :=
  hf.on_subset inter_subset_left

Maximum Preservation Under Intersection

Informal description

Let $f$ be a function defined on a type with a preorder, and let $s$ and $t$ be subsets of the domain. If $a$ is a maximum of $f$ on $s$ (i.e., $f(x) \leq f(a)$ for all $x \in s$), then $a$ is also a maximum of $f$ on the intersection $s \cap t$.

IsExtrOn.inter theorem

(hf : IsExtrOn f s a) (t) : IsExtrOn f (s ∩ t) a

Full source

theorem IsExtrOn.inter (hf : IsExtrOn f s a) (t) : IsExtrOn f (s ∩ t) a :=
  hf.on_subset inter_subset_left

Extremum Preservation Under Intersection

Informal description

Let $f : \alpha \to \beta$ be a function defined on a type $\alpha$ with a preorder, and let $s$ and $t$ be subsets of $\alpha$. If $a$ is an extremum of $f$ on $s$ (i.e., $a$ is either a minimum or a maximum of $f$ on $s$), then $a$ is also an extremum of $f$ on the intersection $s \cap t$.

IsMinFilter.comp_mono theorem

(hf : IsMinFilter f l a) {g : β → γ} (hg : Monotone g) : IsMinFilter (g ∘ f) l a

Full source

theorem IsMinFilter.comp_mono (hf : IsMinFilter f l a) {g : β → γ} (hg : Monotone g) :
    IsMinFilter (g ∘ f) l a :=
  mem_of_superset hf fun _x hx => hg hx

Monotone Composition Preserves Local Minima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local minimum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also a local minimum of the composition $g \circ f$ with respect to $l$.

IsMaxFilter.comp_mono theorem

(hf : IsMaxFilter f l a) {g : β → γ} (hg : Monotone g) : IsMaxFilter (g ∘ f) l a

Full source

theorem IsMaxFilter.comp_mono (hf : IsMaxFilter f l a) {g : β → γ} (hg : Monotone g) :
    IsMaxFilter (g ∘ f) l a :=
  mem_of_superset hf fun _x hx => hg hx

Monotone Composition Preserves Local Maxima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local maximum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also a local maximum of the composition $g \circ f$ with respect to $l$.

IsExtrFilter.comp_mono theorem

(hf : IsExtrFilter f l a) {g : β → γ} (hg : Monotone g) : IsExtrFilter (g ∘ f) l a

Full source

theorem IsExtrFilter.comp_mono (hf : IsExtrFilter f l a) {g : β → γ} (hg : Monotone g) :
    IsExtrFilter (g ∘ f) l a :=
  hf.elim (fun hf => (hf.comp_mono hg).isExtr) fun hf => (hf.comp_mono hg).isExtr

Monotone Composition Preserves Local Extrema with Respect to a Filter

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local extremum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also a local extremum of the composition $g \circ f$ with respect to $l$.

IsMinFilter.comp_antitone theorem

(hf : IsMinFilter f l a) {g : β → γ} (hg : Antitone g) : IsMaxFilter (g ∘ f) l a

Full source

theorem IsMinFilter.comp_antitone (hf : IsMinFilter f l a) {g : β → γ} (hg : Antitone g) :
    IsMaxFilter (g ∘ f) l a :=
  hf.dual.comp_mono fun _ _ h => hg h

Antitone Composition Transforms Local Minima to Local Maxima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local minimum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is a local maximum of the composition $g \circ f$ with respect to $l$.

IsMaxFilter.comp_antitone theorem

(hf : IsMaxFilter f l a) {g : β → γ} (hg : Antitone g) : IsMinFilter (g ∘ f) l a

Full source

theorem IsMaxFilter.comp_antitone (hf : IsMaxFilter f l a) {g : β → γ} (hg : Antitone g) :
    IsMinFilter (g ∘ f) l a :=
  hf.dual.comp_mono fun _ _ h => hg h

Antitone Composition Converts Local Maxima to Local Minima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local maximum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is a local minimum of the composition $g \circ f$ with respect to $l$.

IsExtrFilter.comp_antitone theorem

(hf : IsExtrFilter f l a) {g : β → γ} (hg : Antitone g) : IsExtrFilter (g ∘ f) l a

Full source

theorem IsExtrFilter.comp_antitone (hf : IsExtrFilter f l a) {g : β → γ} (hg : Antitone g) :
    IsExtrFilter (g ∘ f) l a :=
  hf.dual.comp_mono fun _ _ h => hg h

Antitone Composition Preserves Local Extrema with Respect to a Filter

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local extremum of $f$ with respect to $l$. If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is also a local extremum of the composition $g \circ f$ with respect to $l$.

IsMinOn.comp_mono theorem

(hf : IsMinOn f s a) {g : β → γ} (hg : Monotone g) : IsMinOn (g ∘ f) s a

Full source

theorem IsMinOn.comp_mono (hf : IsMinOn f s a) {g : β → γ} (hg : Monotone g) :
    IsMinOn (g ∘ f) s a :=
  IsMinFilter.comp_mono hf hg

Monotone Composition Preserves Setwise Minima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a point where $f$ attains its minimum on $s$, i.e., $f(a) \leq f(x)$ for all $x \in s$. If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also a minimum point of the composition $g \circ f$ on $s$, i.e., $(g \circ f)(a) \leq (g \circ f)(x)$ for all $x \in s$.

IsMaxOn.comp_mono theorem

(hf : IsMaxOn f s a) {g : β → γ} (hg : Monotone g) : IsMaxOn (g ∘ f) s a

Full source

theorem IsMaxOn.comp_mono (hf : IsMaxOn f s a) {g : β → γ} (hg : Monotone g) :
    IsMaxOn (g ∘ f) s a :=
  IsMaxFilter.comp_mono hf hg

Monotone Composition Preserves Setwise Maxima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a point where $f$ attains its maximum on $s$, i.e., $f(x) \leq f(a)$ for all $x \in s$. If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also a maximum point of the composition $g \circ f$ on $s$, i.e., $(g \circ f)(x) \leq (g \circ f)(a)$ for all $x \in s$.

IsExtrOn.comp_mono theorem

(hf : IsExtrOn f s a) {g : β → γ} (hg : Monotone g) : IsExtrOn (g ∘ f) s a

Full source

theorem IsExtrOn.comp_mono (hf : IsExtrOn f s a) {g : β → γ} (hg : Monotone g) :
    IsExtrOn (g ∘ f) s a :=
  IsExtrFilter.comp_mono hf hg

Monotone Composition Preserves Setwise Extrema

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in s$ be an extremum of $f$ on $s$ (i.e., either a minimum or a maximum). If $g : \beta \to \gamma$ is a monotone function between preorders, then $a$ is also an extremum of the composition $g \circ f$ on $s$.

IsMinOn.comp_antitone theorem

(hf : IsMinOn f s a) {g : β → γ} (hg : Antitone g) : IsMaxOn (g ∘ f) s a

Full source

theorem IsMinOn.comp_antitone (hf : IsMinOn f s a) {g : β → γ} (hg : Antitone g) :
    IsMaxOn (g ∘ f) s a :=
  IsMinFilter.comp_antitone hf hg

Antitone Composition Transforms Setwise Minima to Maxima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a point where $f$ attains its minimum on $s$, i.e., $f(a) \leq f(x)$ for all $x \in s$. If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is a maximum point of the composition $g \circ f$ on $s$, i.e., $(g \circ f)(x) \leq (g \circ f)(a)$ for all $x \in s$.

IsMaxOn.comp_antitone theorem

(hf : IsMaxOn f s a) {g : β → γ} (hg : Antitone g) : IsMinOn (g ∘ f) s a

Full source

theorem IsMaxOn.comp_antitone (hf : IsMaxOn f s a) {g : β → γ} (hg : Antitone g) :
    IsMinOn (g ∘ f) s a :=
  IsMaxFilter.comp_antitone hf hg

Antitone Composition Converts Setwise Maxima to Minima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a maximum of $f$ on $s$ (i.e., $f(x) \leq f(a)$ for all $x \in s$). If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is a minimum of the composition $g \circ f$ on $s$.

IsExtrOn.comp_antitone theorem

(hf : IsExtrOn f s a) {g : β → γ} (hg : Antitone g) : IsExtrOn (g ∘ f) s a

Full source

theorem IsExtrOn.comp_antitone (hf : IsExtrOn f s a) {g : β → γ} (hg : Antitone g) :
    IsExtrOn (g ∘ f) s a :=
  IsExtrFilter.comp_antitone hf hg

Antitone Composition Preserves Extrema on a Set

Informal description

Let $f : \alpha \to \beta$ be a function, $s$ a subset of $\alpha$, and $a \in s$ such that $a$ is an extremum of $f$ on $s$. If $g : \beta \to \gamma$ is an antitone function between preorders, then $a$ is also an extremum of the composition $g \circ f$ on $s$.

IsMinFilter.bicomp_mono theorem

 [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinFilter f l a) {g : α → γ}
  (hg : IsMinFilter g l a) : IsMinFilter (fun x => op (f x) (g x)) l a

Full source

theorem IsMinFilter.bicomp_mono [Preorder δ] {op : β → γ → δ}
    (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinFilter f l a) {g : α → γ}
    (hg : IsMinFilter g l a) : IsMinFilter (fun x => op (f x) (g x)) l a :=
  mem_of_superset (inter_mem hf hg) fun _x ⟨hfx, hgx⟩ => hop hfx hgx

Monotone Binary Operation Preserves Local Minima

Informal description

Let $\delta$ be a preorder, and let $op : \beta \to \gamma \to \delta$ be a binary operation that is monotone in both arguments (i.e., $op$ preserves the order in each argument). Suppose $a$ is a local minimum of $f$ with respect to the filter $l$, and $a$ is also a local minimum of $g$ with respect to $l$. Then $a$ is a local minimum of the function $x \mapsto op (f x) (g x)$ with respect to $l$.

IsMaxFilter.bicomp_mono theorem

 [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMaxFilter f l a) {g : α → γ}
  (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => op (f x) (g x)) l a

Full source

theorem IsMaxFilter.bicomp_mono [Preorder δ] {op : β → γ → δ}
    (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMaxFilter f l a) {g : α → γ}
    (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => op (f x) (g x)) l a :=
  mem_of_superset (inter_mem hf hg) fun _x ⟨hfx, hgx⟩ => hop hfx hgx

Local Maximum Preservation under Monotone Binary Operation

Informal description

Let $\delta$ be a preorder, $op : \beta \to \gamma \to \delta$ be a binary operation that is monotone in both arguments (i.e., $op$ preserves the order in each argument), and $f : \alpha \to \beta$, $g : \alpha \to \gamma$ be functions. If $a$ is a local maximum of $f$ with respect to the filter $l$ and $a$ is also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto op (f x) (g x)$ with respect to $l$.

IsMinOn.bicomp_mono theorem

 [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinOn f s a) {g : α → γ}
  (hg : IsMinOn g s a) : IsMinOn (fun x => op (f x) (g x)) s a

Full source

theorem IsMinOn.bicomp_mono [Preorder δ] {op : β → γ → δ}
    (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMinOn f s a) {g : α → γ}
    (hg : IsMinOn g s a) : IsMinOn (fun x => op (f x) (g x)) s a :=
  IsMinFilter.bicomp_mono hop hf hg

Monotone Binary Operation Preserves Minimum on a Set

Informal description

Let $\delta$ be a preorder, $s$ a set in $\alpha$, and $a \in \alpha$. Suppose $op : \beta \to \gamma \to \delta$ is a binary operation that is monotone in both arguments (i.e., $op$ preserves the order in each argument). If $a$ is a minimum of $f$ on $s$ and $a$ is also a minimum of $g$ on $s$, then $a$ is a minimum of the function $x \mapsto op (f x) (g x)$ on $s$.

IsMaxOn.bicomp_mono theorem

 [Preorder δ] {op : β → γ → δ} (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMaxOn f s a) {g : α → γ}
  (hg : IsMaxOn g s a) : IsMaxOn (fun x => op (f x) (g x)) s a

Full source

theorem IsMaxOn.bicomp_mono [Preorder δ] {op : β → γ → δ}
    (hop : ((· ≤ ·) ⇒ (· ≤ ·) ⇒ (· ≤ ·)) op op) (hf : IsMaxOn f s a) {g : α → γ}
    (hg : IsMaxOn g s a) : IsMaxOn (fun x => op (f x) (g x)) s a :=
  IsMaxFilter.bicomp_mono hop hf hg

Maximum Preservation under Monotone Binary Operation on a Set

Informal description

Let $\delta$ be a preorder, $s$ a set in $\alpha$, and $a \in \alpha$. Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, and $op : \beta \to \gamma \to \delta$ a binary operation that is monotone in both arguments (i.e., $op$ preserves the order in each argument). If $a$ is a maximum of $f$ on $s$ and $a$ is also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto op (f x) (g x)$ on $s$.

IsMinFilter.comp_tendsto theorem

 {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsMinFilter f l (g b)) (hg : Tendsto g l' l) : IsMinFilter (f ∘ g) l' b

Full source

theorem IsMinFilter.comp_tendsto {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsMinFilter f l (g b))
    (hg : Tendsto g l' l) : IsMinFilter (f ∘ g) l' b :=
  hg hf

Preservation of Local Minimum under Composition and Filter Convergence

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $f$ has a local minimum at $a$ with respect to $l$. If $g : \delta \to \alpha$ is a function and $l'$ is a filter on $\delta$ such that $g$ tends to $l$ along $l'$, then the composition $f \circ g$ has a local minimum at $b \in \delta$ with respect to $l'$.

IsMaxFilter.comp_tendsto theorem

 {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsMaxFilter f l (g b)) (hg : Tendsto g l' l) : IsMaxFilter (f ∘ g) l' b

Full source

theorem IsMaxFilter.comp_tendsto {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsMaxFilter f l (g b))
    (hg : Tendsto g l' l) : IsMaxFilter (f ∘ g) l' b :=
  hg hf

Preservation of Local Maximum under Composition and Filter Convergence

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $f$ has a local maximum at $a$ with respect to $l$. If $g : \delta \to \alpha$ is a function and $l'$ is a filter on $\delta$ such that $g$ tends to $l$ along $l'$, then the composition $f \circ g$ has a local maximum at $b \in \delta$ with respect to $l'$.

IsExtrFilter.comp_tendsto theorem

 {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsExtrFilter f l (g b)) (hg : Tendsto g l' l) : IsExtrFilter (f ∘ g) l' b

Full source

theorem IsExtrFilter.comp_tendsto {g : δ → α} {l' : Filter δ} {b : δ} (hf : IsExtrFilter f l (g b))
    (hg : Tendsto g l' l) : IsExtrFilter (f ∘ g) l' b :=
  hf.elim (fun hf => (hf.comp_tendsto hg).isExtr) fun hf => (hf.comp_tendsto hg).isExtr

Preservation of Local Extremum under Composition and Filter Convergence

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $f$ has a local extremum at $a$ with respect to $l$. If $g : \delta \to \alpha$ is a function and $l'$ is a filter on $\delta$ such that $g$ tends to $l$ along $l'$, then the composition $f \circ g$ has a local extremum at $b \in \delta$ with respect to $l'$.

IsMinOn.on_preimage theorem

(g : δ → α) {b : δ} (hf : IsMinOn f s (g b)) : IsMinOn (f ∘ g) (g ⁻¹' s) b

Full source

theorem IsMinOn.on_preimage (g : δ → α) {b : δ} (hf : IsMinOn f s (g b)) :
    IsMinOn (f ∘ g) (g ⁻¹' s) b :=
  hf.comp_tendsto (tendsto_principal_principal.mpr <| Subset.refl _)

Minimum Preservation under Preimage Composition

Informal description

Let $f : \alpha \to \beta$ be a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ such that $f$ attains a minimum on $s$ at $a$. For any function $g : \delta \to \alpha$ and any point $b \in \delta$ with $g(b) = a$, the composition $f \circ g$ attains a minimum on the preimage $g^{-1}(s)$ at $b$. In other words, if $f(g(b)) \leq f(x)$ for all $x \in s$, then $(f \circ g)(b) \leq (f \circ g)(y)$ for all $y \in g^{-1}(s)$.

IsMaxOn.on_preimage theorem

(g : δ → α) {b : δ} (hf : IsMaxOn f s (g b)) : IsMaxOn (f ∘ g) (g ⁻¹' s) b

Full source

theorem IsMaxOn.on_preimage (g : δ → α) {b : δ} (hf : IsMaxOn f s (g b)) :
    IsMaxOn (f ∘ g) (g ⁻¹' s) b :=
  hf.comp_tendsto (tendsto_principal_principal.mpr <| Subset.refl _)

Preservation of Maximum on Set under Preimage Composition

Informal description

Let $f : \alpha \to \beta$ be a function with a preorder on $\beta$, $s \subseteq \alpha$, and $a \in \alpha$ such that $f(x) \leq f(a)$ for all $x \in s$ (i.e., $a$ is a maximum of $f$ on $s$). Let $g : \delta \to \alpha$ be a function and $b \in \delta$ such that $g(b) = a$. Then $b$ is a maximum of $f \circ g$ on the preimage $g^{-1}(s)$, i.e., $(f \circ g)(x) \leq (f \circ g)(b)$ for all $x \in g^{-1}(s)$.

IsExtrOn.on_preimage theorem

(g : δ → α) {b : δ} (hf : IsExtrOn f s (g b)) : IsExtrOn (f ∘ g) (g ⁻¹' s) b

Full source

theorem IsExtrOn.on_preimage (g : δ → α) {b : δ} (hf : IsExtrOn f s (g b)) :
    IsExtrOn (f ∘ g) (g ⁻¹' s) b :=
  hf.elim (fun hf => (hf.on_preimage g).isExtr) fun hf => (hf.on_preimage g).isExtr

Extremum Preservation under Preimage Composition

Informal description

Let $f : \alpha \to \beta$ be a function with a preorder on $\beta$, $s \subseteq \alpha$, and $a \in \alpha$ such that $a$ is an extremum of $f$ on $s$ (i.e., either $f(a) \leq f(x)$ for all $x \in s$ or $f(x) \leq f(a)$ for all $x \in s$). Let $g : \delta \to \alpha$ be a function and $b \in \delta$ such that $g(b) = a$. Then $b$ is an extremum of $f \circ g$ on the preimage $g^{-1}(s)$.

IsMinOn.comp_mapsTo theorem

{t : Set δ} {g : δ → α} {b : δ} (hf : IsMinOn f s a) (hg : MapsTo g t s) (ha : g b = a) : IsMinOn (f ∘ g) t b

Full source

theorem IsMinOn.comp_mapsTo {t : Set δ} {g : δ → α} {b : δ} (hf : IsMinOn f s a) (hg : MapsTo g t s)
    (ha : g b = a) : IsMinOn (f ∘ g) t b := fun y hy => by
  simpa only [ha, (· ∘ ·)] using hf (hg hy)

Composition of Minimum on Set with Function Mapping into Domain

Informal description

Let $f : \alpha \to \beta$ be a function with a preorder on $\beta$, $s \subseteq \alpha$, and $a \in \alpha$ such that $f(a) \leq f(x)$ for all $x \in s$ (i.e., $a$ is a minimum of $f$ on $s$). Let $g : \delta \to \alpha$ be a function, $t \subseteq \delta$, and $b \in \delta$ such that $g$ maps $t$ into $s$ (i.e., $g(t) \subseteq s$) and $g(b) = a$. Then $b$ is a minimum of $f \circ g$ on $t$, i.e., $(f \circ g)(b) \leq (f \circ g)(x)$ for all $x \in t$.

IsMaxOn.comp_mapsTo theorem

{t : Set δ} {g : δ → α} {b : δ} (hf : IsMaxOn f s a) (hg : MapsTo g t s) (ha : g b = a) : IsMaxOn (f ∘ g) t b

Full source

theorem IsMaxOn.comp_mapsTo {t : Set δ} {g : δ → α} {b : δ} (hf : IsMaxOn f s a) (hg : MapsTo g t s)
    (ha : g b = a) : IsMaxOn (f ∘ g) t b :=
  hf.dual.comp_mapsTo hg ha

Composition of Maximum on Set with Function Mapping into Domain

Informal description

Let $f : \alpha \to \beta$ be a function with a preorder on $\beta$, $s \subseteq \alpha$, and $a \in \alpha$ such that $f(x) \leq f(a)$ for all $x \in s$ (i.e., $a$ is a maximum of $f$ on $s$). Let $g : \delta \to \alpha$ be a function, $t \subseteq \delta$, and $b \in \delta$ such that $g$ maps $t$ into $s$ (i.e., $g(t) \subseteq s$) and $g(b) = a$. Then $b$ is a maximum of $f \circ g$ on $t$, i.e., $(f \circ g)(x) \leq (f \circ g)(b)$ for all $x \in t$.

IsExtrOn.comp_mapsTo theorem

{t : Set δ} {g : δ → α} {b : δ} (hf : IsExtrOn f s a) (hg : MapsTo g t s) (ha : g b = a) : IsExtrOn (f ∘ g) t b

Full source

theorem IsExtrOn.comp_mapsTo {t : Set δ} {g : δ → α} {b : δ} (hf : IsExtrOn f s a)
    (hg : MapsTo g t s) (ha : g b = a) : IsExtrOn (f ∘ g) t b :=
  hf.elim (fun h => Or.inl <| h.comp_mapsTo hg ha) fun h => Or.inr <| h.comp_mapsTo hg ha

Composition of Extremum on Set with Function Mapping into Domain

Informal description

Let $f : \alpha \to \beta$ be a function with a preorder on $\beta$, $s \subseteq \alpha$, and $a \in \alpha$ such that $a$ is an extremum of $f$ on $s$ (i.e., either $f(a) \leq f(x)$ for all $x \in s$ or $f(x) \leq f(a)$ for all $x \in s$). Let $g : \delta \to \alpha$ be a function, $t \subseteq \delta$, and $b \in \delta$ such that $g$ maps $t$ into $s$ (i.e., $g(t) \subseteq s$) and $g(b) = a$. Then $b$ is an extremum of $f \circ g$ on $t$.

IsMinFilter.add theorem

(hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => f x + g x) l a

Full source

theorem IsMinFilter.add (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
    IsMinFilter (fun x => f x + g x) l a :=
  show IsMinFilter (fun x => f x + g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => add_le_add hx hy) hg

Sum of Local Minima is a Local Minimum

Informal description

Let $f$ and $g$ be functions defined on a type with a partial order and an additive commutative monoid structure. If $a$ is a local minimum of $f$ with respect to a filter $l$, and $a$ is also a local minimum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto f(x) + g(x)$ with respect to $l$.

IsMaxFilter.add theorem

(hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x + g x) l a

Full source

theorem IsMaxFilter.add (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
    IsMaxFilter (fun x => f x + g x) l a :=
  show IsMaxFilter (fun x => f x + g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => add_le_add hx hy) hg

Sum of Locally Maximizing Functions is Locally Maximizing

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to an ordered additive monoid $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local maximum of $f$ with respect to $l$ and $a$ is also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto f(x) + g(x)$ with respect to $l$.

IsMinOn.add theorem

(hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x + g x) s a

Full source

theorem IsMinOn.add (hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x + g x) s a :=
  IsMinFilter.add hf hg

Sum of Minimum Points is Minimum Point of Sum on Set

Informal description

Let $f$ and $g$ be functions from a set $s$ to an ordered additive commutative monoid. If $a$ is a minimum point of $f$ on $s$ and $a$ is also a minimum point of $g$ on $s$, then $a$ is a minimum point of the sum function $x \mapsto f(x) + g(x)$ on $s$.

IsMaxOn.add theorem

(hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x + g x) s a

Full source

theorem IsMaxOn.add (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x + g x) s a :=
  IsMaxFilter.add hf hg

Sum of Maximizing Functions on a Set is Maximizing

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to an ordered additive monoid $\beta$, and let $s$ be a subset of $\alpha$. If $a$ is a maximum of $f$ on $s$ and $a$ is also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto f(x) + g(x)$ on $s$.

IsMinFilter.neg theorem

(hf : IsMinFilter f l a) : IsMaxFilter (fun x => -f x) l a

Full source

theorem IsMinFilter.neg (hf : IsMinFilter f l a) : IsMaxFilter (fun x => -f x) l a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

Negation Transforms Local Minima to Local Maxima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local minimum of $f$ with respect to $l$. Then $a$ is a local maximum of the function $-f$ with respect to $l$.

IsMaxFilter.neg theorem

(hf : IsMaxFilter f l a) : IsMinFilter (fun x => -f x) l a

Full source

theorem IsMaxFilter.neg (hf : IsMaxFilter f l a) : IsMinFilter (fun x => -f x) l a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

Negation Converts Local Maxima to Local Minima

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local maximum of $f$ with respect to $l$. Then $a$ is a local minimum of the function $-f$ with respect to $l$.

IsExtrFilter.neg theorem

(hf : IsExtrFilter f l a) : IsExtrFilter (fun x => -f x) l a

Full source

theorem IsExtrFilter.neg (hf : IsExtrFilter f l a) : IsExtrFilter (fun x => -f x) l a :=
  hf.elim (fun hf => hf.neg.isExtr) fun hf => hf.neg.isExtr

Negation Preserves Local Extrema with Respect to a Filter

Informal description

Let $f : \alpha \to \beta$ be a function, $l$ a filter on $\alpha$, and $a \in \alpha$ such that $a$ is a local extremum of $f$ with respect to $l$. Then $a$ is also a local extremum of the function $-f$ with respect to $l$.

IsMinOn.neg theorem

(hf : IsMinOn f s a) : IsMaxOn (fun x => -f x) s a

Full source

theorem IsMinOn.neg (hf : IsMinOn f s a) : IsMaxOn (fun x => -f x) s a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

Negation Converts Setwise Minima to Maxima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a point where $f$ attains its minimum on $s$, i.e., $f(a) \leq f(x)$ for all $x \in s$. Then $a$ is a maximum point of the function $-f$ on $s$, i.e., $-f(x) \leq -f(a)$ for all $x \in s$.

IsMaxOn.neg theorem

(hf : IsMaxOn f s a) : IsMinOn (fun x => -f x) s a

Full source

theorem IsMaxOn.neg (hf : IsMaxOn f s a) : IsMinOn (fun x => -f x) s a :=
  hf.comp_antitone fun _x _y hx => neg_le_neg hx

Negation Converts Setwise Maxima to Minima

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be a maximum of $f$ on $s$ (i.e., $f(x) \leq f(a)$ for all $x \in s$). Then $a$ is a minimum of the function $-f$ on $s$.

IsExtrOn.neg theorem

(hf : IsExtrOn f s a) : IsExtrOn (fun x => -f x) s a

Full source

theorem IsExtrOn.neg (hf : IsExtrOn f s a) : IsExtrOn (fun x => -f x) s a :=
  hf.elim (fun hf => hf.neg.isExtr) fun hf => hf.neg.isExtr

Negation Preserves Extremum Points on a Set

Informal description

Let $f : \alpha \to \beta$ be a function defined on a set $s \subseteq \alpha$, and let $a \in \alpha$ be an extremum of $f$ on $s$ (i.e., either a minimum or a maximum). Then $a$ is also an extremum of the function $-f$ on $s$.

IsMinFilter.sub theorem

(hf : IsMinFilter f l a) (hg : IsMaxFilter g l a) : IsMinFilter (fun x => f x - g x) l a

Full source

theorem IsMinFilter.sub (hf : IsMinFilter f l a) (hg : IsMaxFilter g l a) :
    IsMinFilter (fun x => f x - g x) l a := by simpa only [sub_eq_add_neg] using hf.add hg.neg

Difference of Local Minimum and Local Maximum is a Local Minimum

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to an ordered additive commutative group $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local minimum of $f$ with respect to $l$, and $a$ is a local maximum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto f(x) - g(x)$ with respect to $l$.

IsMaxFilter.sub theorem

(hf : IsMaxFilter f l a) (hg : IsMinFilter g l a) : IsMaxFilter (fun x => f x - g x) l a

Full source

theorem IsMaxFilter.sub (hf : IsMaxFilter f l a) (hg : IsMinFilter g l a) :
    IsMaxFilter (fun x => f x - g x) l a := by simpa only [sub_eq_add_neg] using hf.add hg.neg

Local Maximum of Difference of Functions with Opposite Extremal Conditions

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to an ordered additive monoid $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local maximum of $f$ with respect to $l$ and $a$ is a local minimum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto f(x) - g(x)$ with respect to $l$.

IsMinOn.sub theorem

(hf : IsMinOn f s a) (hg : IsMaxOn g s a) : IsMinOn (fun x => f x - g x) s a

Full source

theorem IsMinOn.sub (hf : IsMinOn f s a) (hg : IsMaxOn g s a) :
    IsMinOn (fun x => f x - g x) s a := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Minimum of Difference of Functions with Opposite Extremal Conditions on a Set

Informal description

Let $f$ and $g$ be functions from a set $s$ to an ordered additive commutative group, and let $a$ be a point. If $a$ is a minimum of $f$ on $s$ and $a$ is a maximum of $g$ on $s$, then $a$ is a minimum of the function $x \mapsto f(x) - g(x)$ on $s$.

IsMaxOn.sub theorem

(hf : IsMaxOn f s a) (hg : IsMinOn g s a) : IsMaxOn (fun x => f x - g x) s a

Full source

theorem IsMaxOn.sub (hf : IsMaxOn f s a) (hg : IsMinOn g s a) :
    IsMaxOn (fun x => f x - g x) s a := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

Maximum of Difference of Functions with Opposite Extremal Conditions on a Set

Informal description

Let $f, g : \alpha \to \beta$ be functions from a set $\alpha$ to an ordered additive monoid $\beta$, and let $s \subseteq \alpha$. If $a$ is a maximum of $f$ on $s$ and $a$ is a minimum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto f(x) - g(x)$ on $s$.

IsMinFilter.sup theorem

(hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => f x ⊔ g x) l a

Full source

theorem IsMinFilter.sup (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
    IsMinFilter (fun x => f x ⊔ g x) l a :=
  show IsMinFilter (fun x => f x ⊔ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg

Supremum of Local Minima is a Local Minimum

Informal description

Let $f$ and $g$ be functions defined on a type $\alpha$ with values in a join-semilattice $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local minimum of $f$ with respect to $l$, and $a$ is also a local minimum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto f(x) \sqcup g(x)$ with respect to $l$.

IsMaxFilter.sup theorem

(hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x ⊔ g x) l a

Full source

theorem IsMaxFilter.sup (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
    IsMaxFilter (fun x => f x ⊔ g x) l a :=
  show IsMaxFilter (fun x => f x ⊔ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => sup_le_sup hx hy) hg

Local Maximum Preservation under Supremum Operation

Informal description

Let $f$ and $g$ be functions defined on a type $\alpha$ with values in a join-semilattice. If $a$ is a local maximum of $f$ with respect to a filter $l$ and also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto f(x) \sqcup g(x)$ with respect to $l$.

IsMinOn.sup theorem

(hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x ⊔ g x) s a

Full source

theorem IsMinOn.sup (hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x ⊔ g x) s a :=
  IsMinFilter.sup hf hg

Supremum of Minimum Points is a Minimum Point on a Set

Informal description

Let $f$ and $g$ be functions from a set $s$ to a join-semilattice. If $a$ is a minimum point for $f$ on $s$ and also a minimum point for $g$ on $s$, then $a$ is a minimum point for the function $x \mapsto f(x) \sqcup g(x)$ on $s$.

IsMaxOn.sup theorem

(hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x ⊔ g x) s a

Full source

theorem IsMaxOn.sup (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x ⊔ g x) s a :=
  IsMaxFilter.sup hf hg

Supremum Preserves Maximum on Set

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to a join-semilattice. If $a$ is a maximum of $f$ on a set $s$ and also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto f(x) \sqcup g(x)$ on $s$.

IsMinFilter.inf theorem

(hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => f x ⊓ g x) l a

Full source

theorem IsMinFilter.inf (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
    IsMinFilter (fun x => f x ⊓ g x) l a :=
  show IsMinFilter (fun x => f x ⊓ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => inf_le_inf hx hy) hg

Local Minima are Preserved under Infimum Operation

Informal description

Let $f$ and $g$ be functions defined on a type with a meet-semilattice structure, and let $l$ be a filter. If $a$ is a local minimum of $f$ with respect to $l$, and $a$ is also a local minimum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto f(x) \sqcap g(x)$ with respect to $l$.

IsMaxFilter.inf theorem

(hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => f x ⊓ g x) l a

Full source

theorem IsMaxFilter.inf (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
    IsMaxFilter (fun x => f x ⊓ g x) l a :=
  show IsMaxFilter (fun x => f x ⊓ g x) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => inf_le_inf hx hy) hg

Local Maximum Preservation under Infimum Operation

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, where $\beta$ and $\gamma$ are meet-semilattices. If $a$ is a local maximum of $f$ with respect to the filter $l$ and $a$ is also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto f(x) \sqcap g(x)$ with respect to $l$.

IsMinOn.inf theorem

(hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x ⊓ g x) s a

Full source

theorem IsMinOn.inf (hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => f x ⊓ g x) s a :=
  IsMinFilter.inf hf hg

Minimum Points are Preserved under Infimum Operation on a Set

Informal description

Let $f$ and $g$ be functions from a set $s$ to a meet-semilattice. If $a$ is a minimum point of $f$ on $s$ and $a$ is also a minimum point of $g$ on $s$, then $a$ is a minimum point of the function $x \mapsto f(x) \sqcap g(x)$ on $s$.

IsMaxOn.inf theorem

(hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x ⊓ g x) s a

Full source

theorem IsMaxOn.inf (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => f x ⊓ g x) s a :=
  IsMaxFilter.inf hf hg

Maximum Preservation under Infimum Operation on a Set

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, where $\beta$ and $\gamma$ are meet-semilattices. If $a$ is a maximum of $f$ on the set $s$ and $a$ is also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto f(x) \sqcap g(x)$ on $s$.

IsMinFilter.min theorem

(hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => min (f x) (g x)) l a

Full source

theorem IsMinFilter.min (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
    IsMinFilter (fun x => min (f x) (g x)) l a :=
  show IsMinFilter (fun x => Min.min (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => min_le_min hx hy) hg

Local Minimum Preservation under Pointwise Minimum Operation

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to a linearly ordered type, and let $l$ be a filter on $\alpha$. If $a$ is a local minimum of $f$ with respect to $l$, and $a$ is also a local minimum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto \min(f(x), g(x))$ with respect to $l$.

IsMaxFilter.min theorem

(hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => min (f x) (g x)) l a

Full source

theorem IsMaxFilter.min (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
    IsMaxFilter (fun x => min (f x) (g x)) l a :=
  show IsMaxFilter (fun x => Min.min (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => min_le_min hx hy) hg

Local Maximum Preservation under Pointwise Minimum

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to a linearly ordered type $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local maximum of $f$ with respect to $l$ and $a$ is also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto \min(f(x), g(x))$ with respect to $l$.

IsMinOn.min theorem

(hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => min (f x) (g x)) s a

Full source

theorem IsMinOn.min (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
    IsMinOn (fun x => min (f x) (g x)) s a :=
  IsMinFilter.min hf hg

Minimum of Pointwise Minimum of Two Functions on a Set

Informal description

Let $f$ and $g$ be functions from a set $s$ to a linearly ordered type, and let $a$ be a point. If $a$ is a minimum of $f$ on $s$ and $a$ is also a minimum of $g$ on $s$, then $a$ is a minimum of the function $x \mapsto \min(f(x), g(x))$ on $s$.

IsMaxOn.min theorem

(hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => min (f x) (g x)) s a

Full source

theorem IsMaxOn.min (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
    IsMaxOn (fun x => min (f x) (g x)) s a :=
  IsMaxFilter.min hf hg

Preservation of Maximum on Set under Pointwise Minimum

Informal description

Let $f, g : \alpha \to \beta$ be functions from a type $\alpha$ to a linearly ordered type $\beta$, and let $s \subseteq \alpha$. If $a$ is a maximum of $f$ on $s$ and $a$ is also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto \min(f(x), g(x))$ on $s$.

IsMinFilter.max theorem

(hf : IsMinFilter f l a) (hg : IsMinFilter g l a) : IsMinFilter (fun x => max (f x) (g x)) l a

Full source

theorem IsMinFilter.max (hf : IsMinFilter f l a) (hg : IsMinFilter g l a) :
    IsMinFilter (fun x => max (f x) (g x)) l a :=
  show IsMinFilter (fun x => Max.max (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => max_le_max hx hy) hg

Local Minima are Preserved Under Pointwise Maximum

Informal description

Let $f$ and $g$ be functions from a type $\alpha$ to a linearly ordered type $\beta$, and let $l$ be a filter on $\alpha$. If $a$ is a local minimum of $f$ with respect to $l$, and $a$ is also a local minimum of $g$ with respect to $l$, then $a$ is a local minimum of the function $x \mapsto \max(f(x), g(x))$ with respect to $l$.

IsMaxFilter.max theorem

(hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) : IsMaxFilter (fun x => max (f x) (g x)) l a

Full source

theorem IsMaxFilter.max (hf : IsMaxFilter f l a) (hg : IsMaxFilter g l a) :
    IsMaxFilter (fun x => max (f x) (g x)) l a :=
  show IsMaxFilter (fun x => Max.max (f x) (g x)) l a from
    hf.bicomp_mono (fun _x _x' hx _y _y' hy => max_le_max hx hy) hg

Local Maximum Preservation under Pointwise Maximum Operation

Informal description

Let $f, g : \alpha \to \beta$ be functions, $l$ a filter on $\alpha$, and $a \in \alpha$. If $a$ is a local maximum of $f$ with respect to $l$ and $a$ is also a local maximum of $g$ with respect to $l$, then $a$ is a local maximum of the function $x \mapsto \max(f(x), g(x))$ with respect to $l$.

IsMinOn.max theorem

(hf : IsMinOn f s a) (hg : IsMinOn g s a) : IsMinOn (fun x => max (f x) (g x)) s a

Full source

theorem IsMinOn.max (hf : IsMinOn f s a) (hg : IsMinOn g s a) :
    IsMinOn (fun x => max (f x) (g x)) s a :=
  IsMinFilter.max hf hg

Minima are Preserved Under Pointwise Maximum on a Set

Informal description

Let $f, g : \alpha \to \beta$ be functions from a type $\alpha$ to a linearly ordered type $\beta$, and let $s$ be a subset of $\alpha$. If $a$ is a minimum of $f$ on $s$ and $a$ is also a minimum of $g$ on $s$, then $a$ is a minimum of the function $x \mapsto \max(f(x), g(x))$ on $s$.

IsMaxOn.max theorem

(hf : IsMaxOn f s a) (hg : IsMaxOn g s a) : IsMaxOn (fun x => max (f x) (g x)) s a

Full source

theorem IsMaxOn.max (hf : IsMaxOn f s a) (hg : IsMaxOn g s a) :
    IsMaxOn (fun x => max (f x) (g x)) s a :=
  IsMaxFilter.max hf hg

Preservation of Maximum on a Set under Pointwise Maximum Operation

Informal description

Let $f, g : \alpha \to \beta$ be functions from a set $\alpha$ to a linearly ordered set $\beta$, and let $s \subseteq \alpha$ be a subset. If $a \in \alpha$ is a maximum of $f$ on $s$ and also a maximum of $g$ on $s$, then $a$ is a maximum of the function $x \mapsto \max(f(x), g(x))$ on $s$.

Filter.EventuallyLE.isMaxFilter theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a)
  (h : IsMaxFilter f l a) : IsMaxFilter g l a

Full source

theorem Filter.EventuallyLE.isMaxFilter {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : IsMaxFilter f l a) :
    IsMaxFilter g l a := by
  refine hle.mp (h.mono fun x hf hgf => ?_)
  rw [← hfga]
  exact le_trans hgf hf

Preservation of Local Maximum under Eventual Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $g \leq f$ eventually in $l$, $f(a) = g(a)$, and $a$ is a local maximum of $f$ with respect to $l$, then $a$ is also a local maximum of $g$ with respect to $l$.

IsMaxFilter.congr theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (h : IsMaxFilter f l a) (heq : f =ᶠ[l] g)
  (hfga : f a = g a) : IsMaxFilter g l a

Full source

theorem IsMaxFilter.congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
    (h : IsMaxFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMaxFilter g l a :=
  heq.symm.le.isMaxFilter hfga h

Preservation of Local Maximum under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $a$ is a local maximum of $f$ with respect to $l$, $f$ and $g$ are eventually equal in $l$, and $f(a) = g(a)$, then $a$ is also a local maximum of $g$ with respect to $l$.

Filter.EventuallyEq.isMaxFilter_iff theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
  IsMaxFilter f l a ↔ IsMaxFilter g l a

Full source

theorem Filter.EventuallyEq.isMaxFilter_iff {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMaxFilterIsMaxFilter f l a ↔ IsMaxFilter g l a :=
  ⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Equivalence of Local Maxima under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $f$ and $g$ are eventually equal in $l$ and $f(a) = g(a)$, then $a$ is a local maximum of $f$ with respect to $l$ if and only if $a$ is a local maximum of $g$ with respect to $l$.

Filter.EventuallyLE.isMinFilter theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a)
  (h : IsMinFilter f l a) : IsMinFilter g l a

Full source

theorem Filter.EventuallyLE.isMinFilter {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : IsMinFilter f l a) :
    IsMinFilter g l a :=
  @Filter.EventuallyLE.isMaxFilter _ βᵒᵈ _ _ _ _ _ hle hfga h

Preservation of Local Minimum under Eventual Inequality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $f \leq g$ eventually in $l$, $f(a) = g(a)$, and $a$ is a local minimum of $f$ with respect to $l$, then $a$ is also a local minimum of $g$ with respect to $l$.

IsMinFilter.congr theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (h : IsMinFilter f l a) (heq : f =ᶠ[l] g)
  (hfga : f a = g a) : IsMinFilter g l a

Full source

theorem IsMinFilter.congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
    (h : IsMinFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMinFilter g l a :=
  heq.le.isMinFilter hfga h

Preservation of Local Minimum under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $a$ is a local minimum of $f$ with respect to $l$, $f$ and $g$ are eventually equal in $l$, and $f(a) = g(a)$, then $a$ is also a local minimum of $g$ with respect to $l$.

Filter.EventuallyEq.isMinFilter_iff theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
  IsMinFilter f l a ↔ IsMinFilter g l a

Full source

theorem Filter.EventuallyEq.isMinFilter_iff {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsMinFilterIsMinFilter f l a ↔ IsMinFilter g l a :=
  ⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Equivalence of Local Minima under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $f$ and $g$ are eventually equal in $l$ and $f(a) = g(a)$, then $a$ is a local minimum of $f$ with respect to $l$ if and only if $a$ is a local minimum of $g$ with respect to $l$.

IsExtrFilter.congr theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (h : IsExtrFilter f l a) (heq : f =ᶠ[l] g)
  (hfga : f a = g a) : IsExtrFilter g l a

Full source

theorem IsExtrFilter.congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
    (h : IsExtrFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsExtrFilter g l a := by
  rw [IsExtrFilter] at *
  rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]

Preservation of Local Extremum under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $a$ is a local extremum of $f$ with respect to $l$, $f$ and $g$ are eventually equal in $l$, and $f(a) = g(a)$, then $a$ is also a local extremum of $g$ with respect to $l$.

Filter.EventuallyEq.isExtrFilter_iff theorem

 {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
  IsExtrFilter f l a ↔ IsExtrFilter g l a

Full source

theorem Filter.EventuallyEq.isExtrFilter_iff {α β : Type*} [Preorder β] {f g : α → β} {a : α}
    {l : Filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsExtrFilterIsExtrFilter f l a ↔ IsExtrFilter g l a :=
  ⟨fun h => h.congr heq hfga, fun h => h.congr heq.symm hfga.symm⟩

Equivalence of Local Extrema under Eventual Equality

Informal description

Let $\alpha$ and $\beta$ be types with $\beta$ equipped with a preorder, and let $f, g : \alpha \to \beta$ be functions. Given a point $a \in \alpha$ and a filter $l$ on $\alpha$, if $f$ and $g$ are eventually equal in $l$ (i.e., $f(x) = g(x)$ for all $x$ in some neighborhood of $a$ with respect to $l$) and $f(a) = g(a)$, then $a$ is a local extremum of $f$ with respect to $l$ if and only if $a$ is a local extremum of $g$ with respect to $l$.

IsMaxOn.iSup_eq theorem

(hx₀ : x₀ ∈ s) (h : IsMaxOn f s x₀) : ⨆ x : s, f x = f x₀

Full source

theorem IsMaxOn.iSup_eq (hx₀ : x₀ ∈ s) (h : IsMaxOn f s x₀) : ⨆ x : s, f x = f x₀ :=
  haveI : Nonempty s := ⟨⟨x₀, hx₀⟩⟩
  ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun x => h x.2) fun _w hw => ⟨⟨x₀, hx₀⟩, hw⟩

Supremum Equals Function Value at Maximum Point

Informal description

Let $s$ be a set in a conditionally complete linear order $\alpha$, and let $f : s \to \alpha$ be a function. If $x_0 \in s$ is a maximum point of $f$ on $s$ (i.e., $f(x) \leq f(x_0)$ for all $x \in s$), then the supremum of $f$ over $s$ equals $f(x_0)$, i.e., $\sup_{x \in s} f(x) = f(x_0)$.

IsMinOn.iInf_eq theorem

(hx₀ : x₀ ∈ s) (h : IsMinOn f s x₀) : ⨅ x : s, f x = f x₀

Full source

theorem IsMinOn.iInf_eq (hx₀ : x₀ ∈ s) (h : IsMinOn f s x₀) : ⨅ x : s, f x = f x₀ :=
  @IsMaxOn.iSup_eq αᵒᵈ β _ _ _ _ hx₀ h

Infimum Equals Function Value at Minimum Point

Informal description

Let $s$ be a set in a conditionally complete linear order $\alpha$, and let $f : s \to \alpha$ be a function. If $x_0 \in s$ is a minimum point of $f$ on $s$ (i.e., $f(x_0) \leq f(x)$ for all $x \in s$), then the infimum of $f$ over $s$ equals $f(x_0)$, i.e., $\inf_{x \in s} f(x) = f(x_0)$.

sup_eq_of_isMaxOn theorem

{a : α} (hmem : a ∈ s) (hmax : IsMaxOn D s a) : s.sup D = D a

Full source

theorem sup_eq_of_isMaxOn {a : α} (hmem : a ∈ s) (hmax : IsMaxOn D s a) : s.sup D = D a :=
  (Finset.sup_le hmax).antisymm (Finset.le_sup hmem)

Supremum Equals Function Value at Maximum Point on Finite Set

Informal description

Let $s$ be a finite subset of a type $\alpha$, and let $D : \alpha \to \beta$ be a function where $\beta$ is a join-semilattice with a bottom element. If $a \in s$ is a maximum point of $D$ on $s$ (i.e., $D(x) \leq D(a)$ for all $x \in s$), then the supremum of $D$ over $s$ equals $D(a)$, i.e., $\sup_{x \in s} D(x) = D(a)$.

sup_eq_of_max theorem

[Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s) (hmax : ∀ a ∈ s, D a ≤ b) : s.sup D = b

Full source

theorem sup_eq_of_max [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s)
    (hmax : ∀ a ∈ s, D a ≤ b) : s.sup D = b := by
  obtain ⟨a, rfl⟩ := hb
  rw [← Function.apply_invFun_apply (f := D)]
  apply sup_eq_of_isMaxOn hmem; intro
  rw [Function.apply_invFun_apply (f := D)]; apply hmax

Supremum Equals Given Upper Bound in Finite Set

Informal description

Let $\alpha$ be a nonempty type, $\beta$ a join-semilattice with a bottom element, $s$ a finite subset of $\alpha$, and $D : \alpha \to \beta$ a function. Suppose $b$ is in the range of $D$, the preimage of $b$ under $D$ is in $s$, and $D(a) \leq b$ for all $a \in s$. Then the supremum of $D$ over $s$ equals $b$, i.e., $\sup_{x \in s} D(x) = b$.

inf_eq_of_isMinOn theorem

{a : α} (hmem : a ∈ s) (hmax : IsMinOn D s a) : s.inf D = D a

Full source

theorem inf_eq_of_isMinOn {a : α} (hmem : a ∈ s) (hmax : IsMinOn D s a) : s.inf D = D a :=
  sup_eq_of_isMaxOn (α := αᵒᵈ) (β := βᵒᵈ) hmem hmax.dual

Infimum Equals Function Value at Minimum Point on Finite Set

Informal description

Let $s$ be a finite subset of a type $\alpha$, and let $D : \alpha \to \beta$ be a function where $\beta$ is a meet-semilattice with a top element. If $a \in s$ is a minimum point of $D$ on $s$ (i.e., $D(a) \leq D(x)$ for all $x \in s$), then the infimum of $D$ over $s$ equals $D(a)$, i.e., $\inf_{x \in s} D(x) = D(a)$.

inf_eq_of_min theorem

[Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s) (hmin : ∀ a ∈ s, b ≤ D a) : s.inf D = b

Full source

theorem inf_eq_of_min [Nonempty α] {b : β} (hb : b ∈ Set.range D) (hmem : D.invFun b ∈ s)
    (hmin : ∀ a ∈ s, b ≤ D a) : s.inf D = b :=
  sup_eq_of_max (α := αᵒᵈ) (β := βᵒᵈ) hb hmem hmin

Infimum Equals Given Lower Bound in Finite Set

Informal description

Let $\alpha$ be a nonempty type, $\beta$ a meet-semilattice with a top element, $s$ a finite subset of $\alpha$, and $D : \alpha \to \beta$ a function. Suppose $b$ is in the range of $D$, the preimage of $b$ under $D$ is in $s$, and $b \leq D(a)$ for all $a \in s$. Then the infimum of $D$ over $s$ equals $b$, i.e., $\inf_{x \in s} D(x) = b$.

Mathlib.Order.Filter.Extr

Main Definitions

Main statements

Change of the filter (set) argument

Composition

Algebraic operations

Miscellaneous definitions

Missing features (TODO)