Mathlib.Topology.Order.LocalExtr

IsLocalMinOn definition

Full source

/-- `IsLocalMinOn f s a` means that `f a ≤ f x` for all `x ∈ s` in some neighborhood of `a`. -/
def IsLocalMinOn :=
  IsMinFilter f (𝓝[s] a) a

Local minimum of a function on a set

Informal description

A function $ f $ has a local minimum on a set $ s $ at a point $ a $ if there exists a neighborhood of $ a $ within $ s $ such that $ f(a) \leq f(x) $ for all $ x $ in this neighborhood.

IsLocalMaxOn definition

Full source

/-- `IsLocalMaxOn f s a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`. -/
def IsLocalMaxOn :=
  IsMaxFilter f (𝓝[s] a) a

Local maximum of a function on a set

Informal description

A function $ f $ has a local maximum on a set $ s $ at a point $ a $ if there exists a neighborhood of $ a $ within $ s $ such that $ f(x) \leq f(a) $ for all $ x $ in this neighborhood.

IsLocalExtrOn definition

Full source

/-- `IsLocalExtrOn f s a` means `IsLocalMinOn f s a ∨ IsLocalMaxOn f s a`. -/
def IsLocalExtrOn :=
  IsExtrFilter f (𝓝[s] a) a

Local extremum of a function on a set

Informal description

A function $ f $ has a local extremum at a point $ a $ on a set $ s $ if $ f $ has either a local minimum or a local maximum at $ a $ within $ s $. More precisely, this means there exists a neighborhood of $ a $ within $ s $ where $ f $ attains its extremal value at $ a $.

IsLocalMin definition

Full source

/-- `IsLocalMin f a` means that `f a ≤ f x` for all `x` in some neighborhood of `a`. -/
def IsLocalMin :=
  IsMinFilter f (𝓝 a) a

Local minimum of a function

Informal description

A function $ f $ has a local minimum at a point $ a $ if there exists a neighborhood of $ a $ such that $ f(a) \leq f(x) $ for all $ x $ in this neighborhood.

IsLocalMax definition

Full source

/-- `IsLocalMax f a` means that `f x ≤ f a` for all `x ∈ s` in some neighborhood of `a`. -/
def IsLocalMax :=
  IsMaxFilter f (𝓝 a) a

Local maximum of a function at a point

Informal description

A function $ f $ has a local maximum at a point $ a $ if there exists a neighborhood of $ a $ such that for all $ x $ in this neighborhood, $ f(x) \leq f(a) $.

IsLocalExtr definition

Full source

/-- `IsLocalExtr f s a` means `IsLocalMin f s a ∨ IsLocalMax f s a`. -/
def IsLocalExtr :=
  IsExtrFilter f (𝓝 a) a

Local extremum of a function at a point

Informal description

A function $ f $ has a local extremum at a point $ a $ if it has either a local minimum or a local maximum at $ a $. Formally, this means there exists a neighborhood of $ a $ where $ f $ attains its extremal value at $ a $.

IsLocalExtrOn.elim theorem

{p : Prop} : IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p

Full source

theorem IsLocalExtrOn.elim {p : Prop} :
    IsLocalExtrOn f s a → (IsLocalMinOn f s a → p) → (IsLocalMaxOn f s a → p) → p :=
  Or.elim

Elimination Principle for Local Extrema on a Set

Informal description

Given a function $f$ with a local extremum at a point $a$ on a set $s$, and two implications showing that a proposition $p$ holds if $f$ has either a local minimum or a local maximum at $a$ on $s$, then $p$ holds.

IsLocalExtr.elim theorem

{p : Prop} : IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p

Full source

theorem IsLocalExtr.elim {p : Prop} :
    IsLocalExtr f a → (IsLocalMin f a → p) → (IsLocalMax f a → p) → p :=
  Or.elim

Elimination Principle for Local Extrema

Informal description

Given a function $f$ with a local extremum at a point $a$, and two implications showing that both a local minimum at $a$ implies $p$ and a local maximum at $a$ implies $p$, then $p$ holds.

IsLocalMin.on theorem

(h : IsLocalMin f a) (s) : IsLocalMinOn f s a

Full source

theorem IsLocalMin.on (h : IsLocalMin f a) (s) : IsLocalMinOn f s a :=
  h.filter_inf _

Local Minimum on Any Set Given Local Minimum at a Point

Informal description

If a function $f$ has a local minimum at a point $a$, then for any set $s$, $f$ has a local minimum on $s$ at $a$. In other words, if there exists a neighborhood of $a$ such that $f(a) \leq f(x)$ for all $x$ in this neighborhood, then for any set $s$, there exists a neighborhood of $a$ within $s$ such that $f(a) \leq f(x)$ for all $x$ in this neighborhood.

IsLocalMax.on theorem

(h : IsLocalMax f a) (s) : IsLocalMaxOn f s a

Full source

theorem IsLocalMax.on (h : IsLocalMax f a) (s) : IsLocalMaxOn f s a :=
  h.filter_inf _

Local Maximum on a Subset

Informal description

If a function $f$ has a local maximum at a point $a$, then for any set $s$, $f$ has a local maximum on $s$ at $a$. In other words, $f(x) \leq f(a)$ for all $x$ in some neighborhood of $a$ within $s$.

IsLocalExtr.on theorem

(h : IsLocalExtr f a) (s) : IsLocalExtrOn f s a

Full source

theorem IsLocalExtr.on (h : IsLocalExtr f a) (s) : IsLocalExtrOn f s a :=
  h.filter_inf _

Local extremum implies local extremum on any set

Informal description

If a function $f$ has a local extremum at a point $a$, then for any set $s$, $f$ has a local extremum at $a$ on $s$.

IsLocalMinOn.on_subset theorem

{t : Set α} (hf : IsLocalMinOn f t a) (h : s ⊆ t) : IsLocalMinOn f s a

Full source

theorem IsLocalMinOn.on_subset {t : Set α} (hf : IsLocalMinOn f t a) (h : s ⊆ t) :
    IsLocalMinOn f s a :=
  hf.filter_mono <| nhdsWithin_mono a h

Local Minimum Preserved Under Subset Restriction

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$ with $s \subseteq t$. If $f$ has a local minimum on $t$ at a point $a \in \alpha$, then $f$ also has a local minimum on $s$ at $a$.

IsLocalMaxOn.on_subset theorem

{t : Set α} (hf : IsLocalMaxOn f t a) (h : s ⊆ t) : IsLocalMaxOn f s a

Full source

theorem IsLocalMaxOn.on_subset {t : Set α} (hf : IsLocalMaxOn f t a) (h : s ⊆ t) :
    IsLocalMaxOn f s a :=
  hf.filter_mono <| nhdsWithin_mono a h

Local Maximum is Preserved Under Subset Restriction

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$ with $s \subseteq t$. If $f$ has a local maximum on $t$ at a point $a \in s$, then $f$ also has a local maximum on $s$ at $a$.

IsLocalExtrOn.on_subset theorem

{t : Set α} (hf : IsLocalExtrOn f t a) (h : s ⊆ t) : IsLocalExtrOn f s a

Full source

theorem IsLocalExtrOn.on_subset {t : Set α} (hf : IsLocalExtrOn f t a) (h : s ⊆ t) :
    IsLocalExtrOn f s a :=
  hf.filter_mono <| nhdsWithin_mono a h

Local Extremum is Preserved Under Subset Restriction

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$ with $s \subseteq t$. If $f$ has a local extremum at a point $a$ on the set $t$, then $f$ also has a local extremum at $a$ on the subset $s$.

IsLocalMinOn.inter theorem

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

Full source

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

Local Minimum Preserved Under Intersection

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$. If $f$ has a local minimum on $s$ at a point $a \in \alpha$, then $f$ also has a local minimum on $s \cap t$ at $a$.

IsLocalMaxOn.inter theorem

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

Full source

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

Local Maximum Preserved Under Intersection

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$. If $f$ has a local maximum on $s$ at a point $a \in \alpha$, then $f$ also has a local maximum on $s \cap t$ at $a$.

IsLocalExtrOn.inter theorem

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

Full source

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

Local Extremum Preserved Under Intersection

Informal description

Let $f$ be a function defined on a topological space $\alpha$, and let $s, t$ be subsets of $\alpha$. If $f$ has a local extremum on $s$ at a point $a \in \alpha$, then $f$ also has a local extremum on $s \cap t$ at $a$.

IsMinOn.localize theorem

(hf : IsMinOn f s a) : IsLocalMinOn f s a

Full source

theorem IsMinOn.localize (hf : IsMinOn f s a) : IsLocalMinOn f s a :=
  hf.filter_mono <| inf_le_right

Global Minimum on Set Implies Local Minimum on Set

Informal description

If a function $f$ attains its minimum on a set $s$ at a point $a$, then $f$ has a local minimum on $s$ at $a$.

IsMaxOn.localize theorem

(hf : IsMaxOn f s a) : IsLocalMaxOn f s a

Full source

theorem IsMaxOn.localize (hf : IsMaxOn f s a) : IsLocalMaxOn f s a :=
  hf.filter_mono <| inf_le_right

Global Maximum on Set Implies Local Maximum on Set

Informal description

If a function $f$ attains its maximum on a set $s$ at a point $a$, then $f$ has a local maximum on $s$ at $a$.

IsExtrOn.localize theorem

(hf : IsExtrOn f s a) : IsLocalExtrOn f s a

Full source

theorem IsExtrOn.localize (hf : IsExtrOn f s a) : IsLocalExtrOn f s a :=
  hf.filter_mono <| inf_le_right

Global Extremum on Set Implies Local Extremum on Set

Informal description

If a function $f$ has an extremum (either minimum or maximum) on a set $s$ at a point $a$, then $f$ has a local extremum on $s$ at $a$.

IsLocalMinOn.isLocalMin theorem

(hf : IsLocalMinOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMin f a

Full source

theorem IsLocalMinOn.isLocalMin (hf : IsLocalMinOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMin f a :=
  have : 𝓝 a ≤ 𝓟 s := le_principal_iff.2 hs
  hf.filter_mono <| le_inf le_rfl this

Local Minimum on Neighborhood Implies Local Minimum at Point

Informal description

If a function $f$ has a local minimum on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local minimum at $a$.

IsLocalMaxOn.isLocalMax theorem

(hf : IsLocalMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a

Full source

theorem IsLocalMaxOn.isLocalMax (hf : IsLocalMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a :=
  have : 𝓝 a ≤ 𝓟 s := le_principal_iff.2 hs
  hf.filter_mono <| le_inf le_rfl this

Local Maximum on Set Implies Local Maximum at Point

Informal description

If a function $f$ has a local maximum on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local maximum at $a$.

IsLocalExtrOn.isLocalExtr theorem

(hf : IsLocalExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a

Full source

theorem IsLocalExtrOn.isLocalExtr (hf : IsLocalExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a :=
  hf.elim (fun hf => (hf.isLocalMin hs).isExtr) fun hf => (hf.isLocalMax hs).isExtr

Local Extremum on Neighborhood Implies Local Extremum at Point

Informal description

If a function $f$ has a local extremum on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local extremum at $a$.

isLocalMinOn_univ_iff theorem

: IsLocalMinOn f univ a ↔ IsLocalMin f a

Full source

lemma isLocalMinOn_univ_iff : IsLocalMinOnIsLocalMinOn f univ a ↔ IsLocalMin f a := by
  simp only [IsLocalMinOn, IsLocalMin, nhdsWithin_univ]

Local Minimum on Entire Space Equivalence

Informal description

A function $f$ has a local minimum on the entire space at a point $a$ if and only if $f$ has a local minimum at $a$.

isLocalMaxOn_univ_iff theorem

: IsLocalMaxOn f univ a ↔ IsLocalMax f a

Full source

lemma isLocalMaxOn_univ_iff : IsLocalMaxOnIsLocalMaxOn f univ a ↔ IsLocalMax f a := by
  simp only [IsLocalMaxOn, IsLocalMax, nhdsWithin_univ]

Local Maximum on Entire Space Equivalence

Informal description

A function $f$ has a local maximum on the entire space at a point $a$ if and only if $f$ has a local maximum at $a$.

isLocalExtrOn_univ_iff theorem

: IsLocalExtrOn f univ a ↔ IsLocalExtr f a

Full source

lemma isLocalExtrOn_univ_iff : IsLocalExtrOnIsLocalExtrOn f univ a ↔ IsLocalExtr f a :=
  isLocalMinOn_univ_iff.or isLocalMaxOn_univ_iff

Local Extremum on Entire Space Equivalence

Informal description

A function $f$ has a local extremum on the entire space at a point $a$ if and only if $f$ has a local extremum at $a$.

IsMinOn.isLocalMin theorem

(hf : IsMinOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMin f a

Full source

theorem IsMinOn.isLocalMin (hf : IsMinOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMin f a :=
  hf.localize.isLocalMin hs

Global Minimum on Neighborhood Implies Local Minimum at Point

Informal description

If a function $f$ attains its minimum on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local minimum at $a$.

IsMaxOn.isLocalMax theorem

(hf : IsMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a

Full source

theorem IsMaxOn.isLocalMax (hf : IsMaxOn f s a) (hs : s ∈ 𝓝 a) : IsLocalMax f a :=
  hf.localize.isLocalMax hs

Global Maximum on Neighborhood Implies Local Maximum at Point

Informal description

If a function $f$ attains its maximum on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local maximum at $a$.

IsExtrOn.isLocalExtr theorem

(hf : IsExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a

Full source

theorem IsExtrOn.isLocalExtr (hf : IsExtrOn f s a) (hs : s ∈ 𝓝 a) : IsLocalExtr f a :=
  hf.localize.isLocalExtr hs

Global Extremum on Neighborhood Implies Local Extremum at Point

Informal description

If a function $f$ has an extremum (either minimum or maximum) on a set $s$ at a point $a$, and $s$ is a neighborhood of $a$, then $f$ has a local extremum at $a$.

IsLocalMinOn.not_nhds_le_map theorem

[TopologicalSpace β] (hf : IsLocalMinOn f s a) [NeBot (𝓝[<] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Full source

theorem IsLocalMinOn.not_nhds_le_map [TopologicalSpace β] (hf : IsLocalMinOn f s a)
    [NeBot (𝓝[<] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a) := fun hle =>
  have : ∀ᶠ y in 𝓝[<] f a, f a ≤ y := (eventually_map.2 hf).filter_mono (inf_le_left.trans hle)
  let ⟨_y, hy⟩ := (this.and self_mem_nhdsWithin).exists
  hy.1.not_lt hy.2

Non-dominance of neighborhood filters at a local minimum

Informal description

Let $f$ be a function defined on a topological space $\beta$, and let $s$ be a subset of the domain of $f$. If $f$ has a local minimum on $s$ at a point $a$, and the left neighborhood filter $\mathcal{N}[<](f(a))$ is non-trivial, then the neighborhood filter of $f(a)$ is not dominated by the image under $f$ of the neighborhood filter of $a$ restricted to $s$. In other words, $\mathcal{N}(f(a)) \not\leq f_*(\mathcal{N}[s](a))$.

IsLocalMaxOn.not_nhds_le_map theorem

[TopologicalSpace β] (hf : IsLocalMaxOn f s a) [NeBot (𝓝[>] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Full source

theorem IsLocalMaxOn.not_nhds_le_map [TopologicalSpace β] (hf : IsLocalMaxOn f s a)
    [NeBot (𝓝[>] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
  @IsLocalMinOn.not_nhds_le_map α βᵒᵈ _ _ _ _ _ ‹_› hf ‹_›

Non-dominance of neighborhood filters at a local maximum

Informal description

Let $f$ be a function defined on a topological space $\beta$, and let $s$ be a subset of the domain of $f$. If $f$ has a local maximum on $s$ at a point $a$, and the right neighborhood filter $\mathcal{N}[>](f(a))$ is non-trivial, then the neighborhood filter of $f(a)$ is not dominated by the image under $f$ of the neighborhood filter of $a$ restricted to $s$. In other words, $\mathcal{N}(f(a)) \not\leq f_*(\mathcal{N}[s](a))$.

IsLocalExtrOn.not_nhds_le_map theorem

 [TopologicalSpace β] (hf : IsLocalExtrOn f s a) [NeBot (𝓝[<] f a)] [NeBot (𝓝[>] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a)

Full source

theorem IsLocalExtrOn.not_nhds_le_map [TopologicalSpace β] (hf : IsLocalExtrOn f s a)
    [NeBot (𝓝[<] f a)] [NeBot (𝓝[>] f a)] : ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
  hf.elim (fun h => h.not_nhds_le_map) fun h => h.not_nhds_le_map

Non-dominance of neighborhood filters at a local extremum

Informal description

Let $f$ be a function defined on a topological space $\beta$, and let $s$ be a subset of the domain of $f$. If $f$ has a local extremum on $s$ at a point $a$, and both the left and right neighborhood filters $\mathcal{N}[<](f(a))$ and $\mathcal{N}[>](f(a))$ are non-trivial, then the neighborhood filter of $f(a)$ is not dominated by the image under $f$ of the neighborhood filter of $a$ restricted to $s$. In other words, $\mathcal{N}(f(a)) \not\leq f_*(\mathcal{N}[s](a))$.

isLocalMinOn_const theorem

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

Full source

theorem isLocalMinOn_const {b : β} : IsLocalMinOn (fun _ => b) s a :=
  isMinFilter_const

Constant Function Has Local Minimum Everywhere

Informal description

For any constant function $ f(x) = b $ defined on a set $ s $ and any point $ a \in s $, the function $ f $ has a local minimum on $ s $ at $ a $.

isLocalMaxOn_const theorem

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

Full source

theorem isLocalMaxOn_const {b : β} : IsLocalMaxOn (fun _ => b) s a :=
  isMaxFilter_const

Constant Function Has Local Maximum Everywhere

Informal description

For any constant function $ f(x) = b $ defined on a set $ s $ and any point $ a \in s $, the function $ f $ has a local maximum on $ s $ at $ a $.

isLocalExtrOn_const theorem

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

Full source

theorem isLocalExtrOn_const {b : β} : IsLocalExtrOn (fun _ => b) s a :=
  isExtrFilter_const

Constant Function Has Local Extremum Everywhere

Informal description

For any constant function $ f(x) = b $ defined on a set $ s $ and any point $ a \in s $, the function $ f $ has a local extremum (either minimum or maximum) on $ s $ at $ a $.

isLocalMin_const theorem

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

Full source

theorem isLocalMin_const {b : β} : IsLocalMin (fun _ => b) a :=
  isMinFilter_const

Constant Function Has Local Minimum Everywhere

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of type $ \beta $) and any point $ a $, the function $ f $ has a local minimum at $ a $. That is, there exists a neighborhood of $ a $ such that $ b \leq f(x) $ for all $ x $ in this neighborhood.

isLocalMax_const theorem

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

Full source

theorem isLocalMax_const {b : β} : IsLocalMax (fun _ => b) a :=
  isMaxFilter_const

Constant Function Has Local Maximum Everywhere

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of type $ \beta $) and any point $ a $, the function $ f $ has a local maximum at $ a $.

isLocalExtr_const theorem

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

Full source

theorem isLocalExtr_const {b : β} : IsLocalExtr (fun _ => b) a :=
  isExtrFilter_const

Constant Function Has Local Extremum Everywhere

Informal description

For any constant function $ f(x) = b $ (where $ b $ is an element of type $ \beta $), the point $ a $ is a local extremum of $ f $. That is, $ a $ is either a local minimum or a local maximum of $ f $.

IsLocalMin.comp_mono theorem

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

Full source

nonrec theorem IsLocalMin.comp_mono (hf : IsLocalMin f a) {g : β → γ} (hg : Monotone g) :
    IsLocalMin (g ∘ f) a :=
  hf.comp_mono hg

Local Minimum Preserved Under Monotone Composition

Informal description

Let $f$ have a local minimum at a point $a$, and let $g$ be a monotone function. Then the composition $g \circ f$ also has a local minimum at $a$.

IsLocalMax.comp_mono theorem

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

Full source

nonrec theorem IsLocalMax.comp_mono (hf : IsLocalMax f a) {g : β → γ} (hg : Monotone g) :
    IsLocalMax (g ∘ f) a :=
  hf.comp_mono hg

Composition of Local Maximum with Monotone Function Preserves Local Maximum

Informal description

Let $ f $ have a local maximum at a point $ a $, and let $ g $ be a monotone function. Then the composition $ g \circ f $ also has a local maximum at $ a $.

IsLocalExtr.comp_mono theorem

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

Full source

nonrec theorem IsLocalExtr.comp_mono (hf : IsLocalExtr f a) {g : β → γ} (hg : Monotone g) :
    IsLocalExtr (g ∘ f) a :=
  hf.comp_mono hg

Local Extremum Preserved Under Monotone Composition

Informal description

Let $ f $ have a local extremum at a point $ a $, and let $ g $ be a monotone function. Then the composition $ g \circ f $ also has a local extremum at $ a $.

IsLocalMin.comp_antitone theorem

(hf : IsLocalMin f a) {g : β → γ} (hg : Antitone g) : IsLocalMax (g ∘ f) a

Full source

nonrec theorem IsLocalMin.comp_antitone (hf : IsLocalMin f a) {g : β → γ} (hg : Antitone g) :
    IsLocalMax (g ∘ f) a :=
  hf.comp_antitone hg

Composition of Local Minimum with Antitone Function Yields Local Maximum

Informal description

Let $ f $ be a function that has a local minimum at a point $ a $, and let $ g $ be an antitone function. Then the composition $ g \circ f $ has a local maximum at $ a $.

IsLocalMax.comp_antitone theorem

(hf : IsLocalMax f a) {g : β → γ} (hg : Antitone g) : IsLocalMin (g ∘ f) a

Full source

nonrec theorem IsLocalMax.comp_antitone (hf : IsLocalMax f a) {g : β → γ} (hg : Antitone g) :
    IsLocalMin (g ∘ f) a :=
  hf.comp_antitone hg

Local maximum composed with antitone function yields local minimum

Informal description

Let $f$ have a local maximum at a point $a$, and let $g$ be an antitone function. Then the composition $g \circ f$ has a local minimum at $a$.

IsLocalExtr.comp_antitone theorem

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

Full source

nonrec theorem IsLocalExtr.comp_antitone (hf : IsLocalExtr f a) {g : β → γ} (hg : Antitone g) :
    IsLocalExtr (g ∘ f) a :=
  hf.comp_antitone hg

Local extremum under antitone composition

Informal description

If a function $f$ has a local extremum at a point $a$ and $g$ is an antitone function, then the composition $g \circ f$ has a local extremum at $a$.

IsLocalMinOn.comp_mono theorem

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

Full source

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

Local Minimum Preservation under Monotone Composition

Informal description

Let $f$ have a local minimum on a set $s$ at a point $a$, and let $g$ be a monotone function. Then the composition $g \circ f$ also has a local minimum on $s$ at $a$.

IsLocalMaxOn.comp_mono theorem

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

Full source

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

Composition of Local Maximum with Monotone Function Preserves Local Maximum

Informal description

Let $f$ be a function defined on a set $s$ with a local maximum at a point $a \in s$, and let $g$ be a monotone function. Then the composition $g \circ f$ also has a local maximum on $s$ at $a$.

IsLocalExtrOn.comp_mono theorem

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

Full source

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

Local Extremum Preservation under Monotone Composition

Informal description

Let $f$ have a local extremum on a set $s$ at a point $a$, and let $g$ be a monotone function. Then the composition $g \circ f$ also has a local extremum on $s$ at $a$.

IsLocalMinOn.comp_antitone theorem

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

Full source

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

Composition of Local Minimum with Antitone Function Yields Local Maximum

Informal description

Let $f$ be a function defined on a set $s$ with a local minimum at a point $a \in s$, and let $g$ be an antitone function. Then the composition $g \circ f$ has a local maximum on $s$ at $a$.

IsLocalMaxOn.comp_antitone theorem

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

Full source

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

Local Maximum Composed with Antitone Function Yields Local Minimum

Informal description

Let $f$ be a function defined on a set $s$ with a local maximum at a point $a \in s$. If $g$ is an antitone function, then the composition $g \circ f$ has a local minimum on $s$ at $a$.

IsLocalExtrOn.comp_antitone theorem

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

Full source

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

Local extremum of antitone composition

Informal description

Let $f$ have a local extremum at a point $a$ on a set $s$, and let $g$ be an antitone function. Then the composition $g \circ f$ has a local extremum at $a$ on $s$.

IsLocalMin.bicomp_mono theorem

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

Full source

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

Local Minimum Preservation under Monotone Binary Operation

Informal description

Let $\delta$ be a preorder and $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). If $f$ has a local minimum at $a$ and $g$ has a local minimum at $a$, then the function $x \mapsto op(f(x), g(x))$ has a local minimum at $a$.

IsLocalMax.bicomp_mono theorem

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

Full source

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

Local Maximum Preservation Under Monotone Binary Operation

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). If $f$ has a local maximum at $a$ and $g$ has a local maximum at $a$, then the function $x \mapsto op(f(x), g(x))$ also has a local maximum at $a$.

IsLocalMinOn.bicomp_mono theorem

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

Full source

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

Local Minimum Preservation under Monotone Binary Operation

Informal description

Let $s$ be a subset of a topological space, $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions, and $a \in s$. Suppose $f$ has a local minimum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$. Given a binary operation $\mathrm{op} : \beta \to \gamma \to \delta$ that is monotone in both arguments (i.e., $\mathrm{op}$ preserves the order in each argument), then the function $x \mapsto \mathrm{op}(f(x), g(x))$ has a local minimum on $s$ at $a$.

IsLocalMaxOn.bicomp_mono theorem

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

Full source

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

Local Maximum Preservation under Monotone Binary Operation

Informal description

Let $\beta$, $\gamma$, and $\delta$ be types equipped with preorders, and let $s$ be a subset of a topological space $\alpha$ containing a point $a$. Suppose $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ have local maxima on $s$ at $a$, and $op : \beta \to \gamma \to \delta$ is a monotone operation in both arguments (i.e., $op$ preserves the order in each argument). Then the function $x \mapsto op(f(x), g(x))$ has a local maximum on $s$ at $a$.

IsLocalMin.comp_continuous theorem

 [TopologicalSpace δ] {g : δ → α} {b : δ} (hf : IsLocalMin f (g b)) (hg : ContinuousAt g b) : IsLocalMin (f ∘ g) b

Full source

theorem IsLocalMin.comp_continuous [TopologicalSpace δ] {g : δ → α} {b : δ}
    (hf : IsLocalMin f (g b)) (hg : ContinuousAt g b) : IsLocalMin (f ∘ g) b :=
  hg hf

Preservation of Local Minimum under Continuous Composition

Informal description

Let $f : \alpha \to \beta$ be a function and $g : \delta \to \alpha$ be a continuous function at a point $b \in \delta$. If $f$ has a local minimum at $g(b)$, then the composition $f \circ g$ has a local minimum at $b$.

IsLocalMax.comp_continuous theorem

 [TopologicalSpace δ] {g : δ → α} {b : δ} (hf : IsLocalMax f (g b)) (hg : ContinuousAt g b) : IsLocalMax (f ∘ g) b

Full source

theorem IsLocalMax.comp_continuous [TopologicalSpace δ] {g : δ → α} {b : δ}
    (hf : IsLocalMax f (g b)) (hg : ContinuousAt g b) : IsLocalMax (f ∘ g) b :=
  hg hf

Local maximum is preserved under composition with a continuous function

Informal description

Let $f : \alpha \to \beta$ and $g : \delta \to \alpha$ be functions, where $\alpha$ and $\delta$ are topological spaces. If $f$ has a local maximum at $g(b)$ and $g$ is continuous at $b \in \delta$, then the composition $f \circ g$ has a local maximum at $b$.

IsLocalExtr.comp_continuous theorem

 [TopologicalSpace δ] {g : δ → α} {b : δ} (hf : IsLocalExtr f (g b)) (hg : ContinuousAt g b) : IsLocalExtr (f ∘ g) b

Full source

theorem IsLocalExtr.comp_continuous [TopologicalSpace δ] {g : δ → α} {b : δ}
    (hf : IsLocalExtr f (g b)) (hg : ContinuousAt g b) : IsLocalExtr (f ∘ g) b :=
  hf.comp_tendsto hg

Preservation of Local Extrema under Continuous Composition

Informal description

Let $f : \alpha \to \beta$ and $g : \delta \to \alpha$ be functions, where $\alpha$ and $\delta$ are topological spaces. If $f$ has a local extremum at $g(b)$ and $g$ is continuous at $b$, then the composition $f \circ g$ has a local extremum at $b$.

IsLocalMin.comp_continuousOn theorem

 [TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMin f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) :
  IsLocalMinOn (f ∘ g) s b

Full source

theorem IsLocalMin.comp_continuousOn [TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ}
    (hf : IsLocalMin f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMinOn (f ∘ g) s b :=
  hf.comp_tendsto (hg b hb)

Local Minimum Preservation under Continuous Composition on a Subset

Informal description

Let $ \delta $ be a topological space, $ s \subseteq \delta $ a subset, $ g : \delta \to \alpha $ a function, and $ b \in \delta $ a point. If $ f $ has a local minimum at $ g(b) $ and $ g $ is continuous on $ s $ at $ b $, then the composition $ f \circ g $ has a local minimum on $ s $ at $ b $.

IsLocalMax.comp_continuousOn theorem

 [TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMax f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) :
  IsLocalMaxOn (f ∘ g) s b

Full source

theorem IsLocalMax.comp_continuousOn [TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ}
    (hf : IsLocalMax f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMaxOn (f ∘ g) s b :=
  hf.comp_tendsto (hg b hb)

Preservation of Local Maximum under Continuous Composition on a Set

Informal description

Let $f : \alpha \to \mathbb{R}$ have a local maximum at $g(b)$, and let $g : \delta \to \alpha$ be continuous on a set $s \subseteq \delta$ with $b \in s$. Then the composition $f \circ g$ has a local maximum on $s$ at $b$.

IsLocalExtr.comp_continuousOn theorem

 [TopologicalSpace δ] {s : Set δ} (g : δ → α) {b : δ} (hf : IsLocalExtr f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) :
  IsLocalExtrOn (f ∘ g) s b

Full source

theorem IsLocalExtr.comp_continuousOn [TopologicalSpace δ] {s : Set δ} (g : δ → α) {b : δ}
    (hf : IsLocalExtr f (g b)) (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalExtrOn (f ∘ g) s b :=
  hf.elim (fun hf => (hf.comp_continuousOn hg hb).isExtr) fun hf =>
    (IsLocalMax.comp_continuousOn hf hg hb).isExtr

Local Extremum Preservation under Continuous Composition on a Subset

Informal description

Let $\alpha$ and $\delta$ be topological spaces, $s \subseteq \delta$, $g : \delta \to \alpha$, and $b \in \delta$. If $f$ has a local extremum at $g(b)$ and $g$ is continuous on $s$ at $b$, then the composition $f \circ g$ has a local extremum on $s$ at $b$.

IsLocalMinOn.comp_continuousOn theorem

 [TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMinOn f t (g b)) (hst : s ⊆ g ⁻¹' t)
  (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMinOn (f ∘ g) s b

Full source

theorem IsLocalMinOn.comp_continuousOn [TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α}
    {b : δ} (hf : IsLocalMinOn f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : ContinuousOn g s) (hb : b ∈ s) :
    IsLocalMinOn (f ∘ g) s b :=
  hf.comp_tendsto
    (tendsto_nhdsWithin_mono_right (image_subset_iff.mpr hst)
      (ContinuousWithinAt.tendsto_nhdsWithin_image (hg b hb)))

Local Minimum Preservation under Continuous Composition

Informal description

Let $\alpha$ and $\delta$ be topological spaces, $t \subseteq \alpha$, $s \subseteq \delta$, and $g : \delta \to \alpha$. Suppose $f$ has a local minimum on $t$ at $g(b)$ for some $b \in s$, $s \subseteq g^{-1}(t)$, $g$ is continuous on $s$, and $b \in s$. Then the composition $f \circ g$ has a local minimum on $s$ at $b$.

IsLocalMaxOn.comp_continuousOn theorem

 [TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMaxOn f t (g b)) (hst : s ⊆ g ⁻¹' t)
  (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMaxOn (f ∘ g) s b

Full source

theorem IsLocalMaxOn.comp_continuousOn [TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α}
    {b : δ} (hf : IsLocalMaxOn f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : ContinuousOn g s) (hb : b ∈ s) :
    IsLocalMaxOn (f ∘ g) s b :=
  hf.comp_tendsto
    (tendsto_nhdsWithin_mono_right (image_subset_iff.mpr hst)
      (ContinuousWithinAt.tendsto_nhdsWithin_image (hg b hb)))

Local Maximum Preservation Under Continuous Composition on Subset

Informal description

Let $\alpha$ and $\delta$ be topological spaces, $t \subseteq \alpha$, $s \subseteq \delta$, $g : \delta \to \alpha$, and $b \in \delta$. If $f$ has a local maximum on $t$ at $g(b)$, $s \subseteq g^{-1}(t)$, $g$ is continuous on $s$, and $b \in s$, then the composition $f \circ g$ has a local maximum on $s$ at $b$.

IsLocalExtrOn.comp_continuousOn theorem

 [TopologicalSpace δ] {t : Set α} {s : Set δ} (g : δ → α) {b : δ} (hf : IsLocalExtrOn f t (g b)) (hst : s ⊆ g ⁻¹' t)
  (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalExtrOn (f ∘ g) s b

Full source

theorem IsLocalExtrOn.comp_continuousOn [TopologicalSpace δ] {t : Set α} {s : Set δ} (g : δ → α)
    {b : δ} (hf : IsLocalExtrOn f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : ContinuousOn g s)
    (hb : b ∈ s) : IsLocalExtrOn (f ∘ g) s b :=
  hf.elim (fun hf => (hf.comp_continuousOn hst hg hb).isExtr) fun hf =>
    (IsLocalMaxOn.comp_continuousOn hf hst hg hb).isExtr

Local Extremum Preservation under Continuous Composition

Informal description

Let $\alpha$ and $\delta$ be topological spaces, $t \subseteq \alpha$, $s \subseteq \delta$, and $g : \delta \to \alpha$. Suppose $f$ has a local extremum on $t$ at $g(b)$ for some $b \in s$, $s \subseteq g^{-1}(t)$, $g$ is continuous on $s$, and $b \in s$. Then the composition $f \circ g$ has a local extremum on $s$ at $b$.

IsLocalMin.add theorem

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

Full source

nonrec theorem IsLocalMin.add (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
    IsLocalMin (fun x => f x + g x) a :=
  hf.add hg

Sum of Local Minima is a Local Minimum

Informal description

If a function $f$ has a local minimum at a point $a$ and a function $g$ has a local minimum at the same point $a$, then the function $x \mapsto f(x) + g(x)$ also has a local minimum at $a$.

IsLocalMax.add theorem

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

Full source

nonrec theorem IsLocalMax.add (hf : IsLocalMax f a) (hg : IsLocalMax g a) :
    IsLocalMax (fun x => f x + g x) a :=
  hf.add hg

Sum of Local Maxima is a Local Maximum

Informal description

If $f$ has a local maximum at $a$ and $g$ has a local maximum at $a$, then the function $x \mapsto f(x) + g(x)$ also has a local maximum at $a$.

IsLocalMinOn.add theorem

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

Full source

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

Sum of Local Minimum Functions is Local Minimum

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local minimum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$, then the function $x \mapsto f(x) + g(x)$ has a local minimum on $s$ at $a$.

IsLocalMaxOn.add theorem

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

Full source

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

Sum of Local Maxima on a Set is a Local Maximum

Informal description

If a function $f$ has a local maximum on a set $s$ at a point $a$, and a function $g$ also has a local maximum on $s$ at $a$, then the function $x \mapsto f(x) + g(x)$ has a local maximum on $s$ at $a$.

IsLocalMin.neg theorem

(hf : IsLocalMin f a) : IsLocalMax (fun x => -f x) a

Full source

nonrec theorem IsLocalMin.neg (hf : IsLocalMin f a) : IsLocalMax (fun x => -f x) a :=
  hf.neg

Negation Reverses Local Minima to Local Maxima

Informal description

If a function $f$ has a local minimum at a point $a$, then the function $-f$ has a local maximum at $a$.

IsLocalMax.neg theorem

(hf : IsLocalMax f a) : IsLocalMin (fun x => -f x) a

Full source

nonrec theorem IsLocalMax.neg (hf : IsLocalMax f a) : IsLocalMin (fun x => -f x) a :=
  hf.neg

Negation reverses local maxima to local minima

Informal description

If a function $f$ has a local maximum at a point $a$, then the function $-f$ has a local minimum at $a$.

IsLocalExtr.neg theorem

(hf : IsLocalExtr f a) : IsLocalExtr (fun x => -f x) a

Full source

nonrec theorem IsLocalExtr.neg (hf : IsLocalExtr f a) : IsLocalExtr (fun x => -f x) a :=
  hf.neg

Local extremum under negation

Informal description

If a function $f$ has a local extremum at a point $a$, then the function $-f$ also has a local extremum at $a$.

IsLocalMinOn.neg theorem

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

Full source

nonrec theorem IsLocalMinOn.neg (hf : IsLocalMinOn f s a) : IsLocalMaxOn (fun x => -f x) s a :=
  hf.neg

Negation Reverses Local Minima to Local Maxima on a Set

Informal description

If a function $f$ has a local minimum on a set $s$ at a point $a$, then the function $-f$ has a local maximum on $s$ at $a$.

IsLocalMaxOn.neg theorem

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

Full source

nonrec theorem IsLocalMaxOn.neg (hf : IsLocalMaxOn f s a) : IsLocalMinOn (fun x => -f x) s a :=
  hf.neg

Negation Reverses Local Maxima to Local Minima on a Set

Informal description

If a function $f$ has a local maximum on a set $s$ at a point $a$, then the function $-f$ has a local minimum on $s$ at $a$.

IsLocalExtrOn.neg theorem

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

Full source

nonrec theorem IsLocalExtrOn.neg (hf : IsLocalExtrOn f s a) : IsLocalExtrOn (fun x => -f x) s a :=
  hf.neg

Negation Preserves Local Extrema on a Set

Informal description

If a function $f$ has a local extremum on a set $s$ at a point $a$, then the function $-f$ also has a local extremum on $s$ at $a$.

IsLocalMin.sub theorem

(hf : IsLocalMin f a) (hg : IsLocalMax g a) : IsLocalMin (fun x => f x - g x) a

Full source

nonrec theorem IsLocalMin.sub (hf : IsLocalMin f a) (hg : IsLocalMax g a) :
    IsLocalMin (fun x => f x - g x) a :=
  hf.sub hg

Local Minimum of Difference at Critical Points

Informal description

Let $f$ and $g$ be functions such that $f$ has a local minimum at $a$ and $g$ has a local maximum at $a$. Then the function $x \mapsto f(x) - g(x)$ has a local minimum at $a$.

IsLocalMax.sub theorem

(hf : IsLocalMax f a) (hg : IsLocalMin g a) : IsLocalMax (fun x => f x - g x) a

Full source

nonrec theorem IsLocalMax.sub (hf : IsLocalMax f a) (hg : IsLocalMin g a) :
    IsLocalMax (fun x => f x - g x) a :=
  hf.sub hg

Local Maximum of Difference of Functions with Local Maximum and Minimum

Informal description

Let $f$ and $g$ be functions defined on a topological space. If $f$ has a local maximum at a point $a$ and $g$ has a local minimum at $a$, then the function $x \mapsto f(x) - g(x)$ has a local maximum at $a$.

IsLocalMinOn.sub theorem

(hf : IsLocalMinOn f s a) (hg : IsLocalMaxOn g s a) : IsLocalMinOn (fun x => f x - g x) s a

Full source

nonrec theorem IsLocalMinOn.sub (hf : IsLocalMinOn f s a) (hg : IsLocalMaxOn g s a) :
    IsLocalMinOn (fun x => f x - g x) s a :=
  hf.sub hg

Local Minimum of Difference at Point where First Function has Local Minimum and Second has Local Maximum

Informal description

Let $f$ and $g$ be functions defined on a set $s$ containing a point $a$. If $f$ has a local minimum on $s$ at $a$ and $g$ has a local maximum on $s$ at $a$, then the function $x \mapsto f(x) - g(x)$ has a local minimum on $s$ at $a$.

IsLocalMaxOn.sub theorem

(hf : IsLocalMaxOn f s a) (hg : IsLocalMinOn g s a) : IsLocalMaxOn (fun x => f x - g x) s a

Full source

nonrec theorem IsLocalMaxOn.sub (hf : IsLocalMaxOn f s a) (hg : IsLocalMinOn g s a) :
    IsLocalMaxOn (fun x => f x - g x) s a :=
  hf.sub hg

Local Maximum of Difference When First Function Has Local Maximum and Second Has Local Minimum

Informal description

Let $f$ and $g$ be functions defined on a set $s$ containing a point $a$. If $f$ has a local maximum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$, then the function $x \mapsto f(x) - g(x)$ has a local maximum on $s$ at $a$.

IsLocalMin.sup theorem

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

Full source

nonrec theorem IsLocalMin.sup (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
    IsLocalMin (fun x => f x ⊔ g x) a :=
  hf.sup hg

Local Minimum is Preserved under Pointwise Supremum

Informal description

If $f$ has a local minimum at $a$ and $g$ has a local minimum at $a$, then the function $x \mapsto f(x) \sqcup g(x)$ (pointwise supremum) has a local minimum at $a$.

IsLocalMax.sup theorem

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

Full source

nonrec theorem IsLocalMax.sup (hf : IsLocalMax f a) (hg : IsLocalMax g a) :
    IsLocalMax (fun x => f x ⊔ g x) a :=
  hf.sup hg

Pointwise Supremum Preserves Local Maxima

Informal description

If a function $f$ has a local maximum at a point $a$ and a function $g$ has a local maximum at the same point $a$, then the pointwise supremum function $x \mapsto f(x) \sqcup g(x)$ also has a local maximum at $a$.

IsLocalMinOn.sup theorem

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

Full source

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

Local Minimum of Pointwise Supremum of Two Functions on a Set

Informal description

Let $ f $ and $ g $ be functions defined on a set $ s $ in a topological space, and let $ a \in s $. If $ f $ has a local minimum on $ s $ at $ a $ and $ g $ has a local minimum on $ s $ at $ a $, then the pointwise supremum function $ x \mapsto f(x) \sqcup g(x) $ also has a local minimum on $ s $ at $ a $.

IsLocalMaxOn.sup theorem

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

Full source

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

Pointwise Supremum Preserves Local Maxima on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local maximum on $s$ at $a$ and $g$ has a local maximum on $s$ at $a$, then the function $x \mapsto f(x) \sqcup g(x)$ (pointwise supremum of $f$ and $g$) also has a local maximum on $s$ at $a$.

IsLocalMin.inf theorem

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

Full source

nonrec theorem IsLocalMin.inf (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
    IsLocalMin (fun x => f x ⊓ g x) a :=
  hf.inf hg

Local Minimum is Preserved under Pointwise Infimum

Informal description

Let $ f $ and $ g $ be functions that each have a local minimum at a point $ a $. Then the function $ x \mapsto \min(f(x), g(x)) $ also has a local minimum at $ a $.

IsLocalMax.inf theorem

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

Full source

nonrec theorem IsLocalMax.inf (hf : IsLocalMax f a) (hg : IsLocalMax g a) :
    IsLocalMax (fun x => f x ⊓ g x) a :=
  hf.inf hg

Local Maximum of Infimum of Two Functions

Informal description

If a function $f$ has a local maximum at a point $a$ and a function $g$ has a local maximum at $a$, then the function $x \mapsto f(x) \sqcap g(x)$ also has a local maximum at $a$.

IsLocalMinOn.inf theorem

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

Full source

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

Infimum of Local Minima is a Local Minimum

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local minimum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$, then the function $x \mapsto f(x) \sqcap g(x)$ also has a local minimum on $s$ at $a$.

IsLocalMaxOn.inf theorem

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

Full source

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

Local Maximum of Infimum of Two Functions on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local maximum on $s$ at $a$ and $g$ has a local maximum on $s$ at $a$, then the function $x \mapsto f(x) \sqcap g(x)$ also has a local maximum on $s$ at $a$.

IsLocalMin.min theorem

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

Full source

nonrec theorem IsLocalMin.min (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
    IsLocalMin (fun x => min (f x) (g x)) a :=
  hf.min hg

Pointwise Minimum Preserves Local Minima

Informal description

If functions $f$ and $g$ have local minima at a point $a$, then the pointwise minimum function $x \mapsto \min(f(x), g(x))$ also has a local minimum at $a$.

IsLocalMax.min theorem

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

Full source

nonrec theorem IsLocalMax.min (hf : IsLocalMax f a) (hg : IsLocalMax g a) :
    IsLocalMax (fun x => min (f x) (g x)) a :=
  hf.min hg

Local maximum of the minimum of two functions

Informal description

If functions $f$ and $g$ have local maxima at a point $a$, then the function $x \mapsto \min(f(x), g(x))$ also has a local maximum at $a$.

IsLocalMinOn.min theorem

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

Full source

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

Local Minimum of Pointwise Minimum of Two Functions

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local minimum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$, then the function $x \mapsto \min(f(x), g(x))$ has a local minimum on $s$ at $a$.

IsLocalMaxOn.min theorem

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

Full source

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

Local Maximum of Minimum of Two Functions on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local maximum on $s$ at $a$ and $g$ has a local maximum on $s$ at $a$, then the function $x \mapsto \min(f(x), g(x))$ has a local maximum on $s$ at $a$.

IsLocalMin.max theorem

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

Full source

nonrec theorem IsLocalMin.max (hf : IsLocalMin f a) (hg : IsLocalMin g a) :
    IsLocalMin (fun x => max (f x) (g x)) a :=
  hf.max hg

Local Minimum of Pointwise Maximum of Two Functions

Informal description

If functions $f$ and $g$ have local minima at a point $a$, then the function $x \mapsto \max(f(x), g(x))$ also has a local minimum at $a$.

IsLocalMax.max theorem

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

Full source

nonrec theorem IsLocalMax.max (hf : IsLocalMax f a) (hg : IsLocalMax g a) :
    IsLocalMax (fun x => max (f x) (g x)) a :=
  hf.max hg

Local Maximum of Pointwise Maximum of Two Functions

Informal description

If functions $f$ and $g$ have local maxima at a point $a$, then the function $x \mapsto \max(f(x), g(x))$ also has a local maximum at $a$.

IsLocalMinOn.max theorem

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

Full source

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

Local Minimum of Pointwise Maximum of Two Functions on a Set

Informal description

Let $f$ and $g$ be functions defined on a set $s$ in a topological space, and let $a \in s$. If $f$ has a local minimum on $s$ at $a$ and $g$ has a local minimum on $s$ at $a$, then the function $x \mapsto \max(f(x), g(x))$ also has a local minimum on $s$ at $a$.

IsLocalMaxOn.max theorem

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

Full source

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

Local Maximum of Pointwise Maximum of Two Functions on a Set

Informal description

Let $f$ and $g$ be functions from a topological space $\alpha$ to a partially ordered set $\beta$, and let $s$ be a subset of $\alpha$. If $f$ has a local maximum on $s$ at a point $a \in s$, and $g$ has a local maximum on $s$ at $a$, then the function $x \mapsto \max(f(x), g(x))$ also has a local maximum on $s$ at $a$.

Filter.EventuallyLE.isLocalMaxOn theorem

 {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝[s] a] f) (hfga : f a = g a) (h : IsLocalMaxOn f s a) : IsLocalMaxOn g s a

Full source

theorem Filter.EventuallyLE.isLocalMaxOn {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝[s] a] f)
    (hfga : f a = g a) (h : IsLocalMaxOn f s a) : IsLocalMaxOn g s a :=
  hle.isMaxFilter hfga h

Local Maximum Preservation under Eventual Inequality

Informal description

Let $ f, g : \alpha \to \beta $ be functions, $ s \subseteq \alpha $, and $ a \in s $. If $ g \leq f $ eventually near $ a $ within $ s $, $ f(a) = g(a) $, and $ f $ has a local maximum on $ s $ at $ a $, then $ g $ also has a local maximum on $ s $ at $ a $.

IsLocalMaxOn.congr theorem

{f g : α → β} {a : α} (h : IsLocalMaxOn f s a) (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMaxOn g s a

Full source

nonrec theorem IsLocalMaxOn.congr {f g : α → β} {a : α} (h : IsLocalMaxOn f s a)
    (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMaxOn g s a :=
  h.congr heq <| heq.eq_of_nhdsWithin hmem

Local Maximum is Preserved by Eventual Equality

Informal description

Let $f, g : \alpha \to \beta$ be functions, $s \subseteq \alpha$ a subset, and $a \in s$ a point. If $f$ has a local maximum on $s$ at $a$, and $f$ is eventually equal to $g$ in a neighborhood of $a$ within $s$, then $g$ also has a local maximum on $s$ at $a$.

Filter.EventuallyEq.isLocalMaxOn_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMaxOn f s a ↔ IsLocalMaxOn g s a

Full source

theorem Filter.EventuallyEq.isLocalMaxOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g)
    (hmem : a ∈ s) : IsLocalMaxOnIsLocalMaxOn f s a ↔ IsLocalMaxOn g s a :=
  heq.isMaxFilter_iff <| heq.eq_of_nhdsWithin hmem

Local Maximum Criterion for Eventually Equal Functions

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$ a point in the set $s$. If $f$ and $g$ are eventually equal in a neighborhood of $a$ within $s$ (i.e., $f =_{𝓝[s] a} g$), then $f$ has a local maximum on $s$ at $a$ if and only if $g$ has a local maximum on $s$ at $a$.

Filter.EventuallyLE.isLocalMinOn theorem

 {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝[s] a] g) (hfga : f a = g a) (h : IsLocalMinOn f s a) : IsLocalMinOn g s a

Full source

theorem Filter.EventuallyLE.isLocalMinOn {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝[s] a] g)
    (hfga : f a = g a) (h : IsLocalMinOn f s a) : IsLocalMinOn g s a :=
  hle.isMinFilter hfga h

Local minimum is preserved under eventual inequality with equality at the point

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f \leq g$ eventually in a neighborhood of $a$ within $s$, $f(a) = g(a)$, and $f$ has a local minimum on $s$ at $a$, then $g$ also has a local minimum on $s$ at $a$.

IsLocalMinOn.congr theorem

{f g : α → β} {a : α} (h : IsLocalMinOn f s a) (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMinOn g s a

Full source

nonrec theorem IsLocalMinOn.congr {f g : α → β} {a : α} (h : IsLocalMinOn f s a)
    (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMinOn g s a :=
  h.congr heq <| heq.eq_of_nhdsWithin hmem

Preservation of Local Minimum under Eventual Equality

Informal description

Let $f, g : \alpha \to \beta$ be functions, $s \subseteq \alpha$ a set, and $a \in s$ a point. If $f$ has a local minimum on $s$ at $a$, and $f$ and $g$ are eventually equal in a neighborhood of $a$ within $s$, then $g$ also has a local minimum on $s$ at $a$.

Filter.EventuallyEq.isLocalMinOn_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalMinOn f s a ↔ IsLocalMinOn g s a

Full source

nonrec theorem Filter.EventuallyEq.isLocalMinOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g)
    (hmem : a ∈ s) : IsLocalMinOnIsLocalMinOn f s a ↔ IsLocalMinOn g s a :=
  heq.isMinFilter_iff <| heq.eq_of_nhdsWithin hmem

Local Minimum Criterion for Eventually Equal Functions

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in s \subseteq \alpha$. If $f$ and $g$ are eventually equal in a neighborhood of $a$ within $s$ (i.e., $f =ᶠ[𝓝[s] a] g$), then $f$ has a local minimum on $s$ at $a$ if and only if $g$ has a local minimum on $s$ at $a$.

IsLocalExtrOn.congr theorem

{f g : α → β} {a : α} (h : IsLocalExtrOn f s a) (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalExtrOn g s a

Full source

nonrec theorem IsLocalExtrOn.congr {f g : α → β} {a : α} (h : IsLocalExtrOn f s a)
    (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalExtrOn g s a :=
  h.congr heq <| heq.eq_of_nhdsWithin hmem

Local extremum is preserved under eventual equality on a set

Informal description

Let $f, g : \alpha \to \beta$ be functions, $a \in \alpha$ a point, and $s \subseteq \alpha$ a set. If $f$ has a local extremum at $a$ on $s$, and $f$ is eventually equal to $g$ in a neighborhood of $a$ within $s$, and $a \in s$, then $g$ also has a local extremum at $a$ on $s$.

Filter.EventuallyEq.isLocalExtrOn_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g) (hmem : a ∈ s) : IsLocalExtrOn f s a ↔ IsLocalExtrOn g s a

Full source

theorem Filter.EventuallyEq.isLocalExtrOn_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝[s] a] g)
    (hmem : a ∈ s) : IsLocalExtrOnIsLocalExtrOn f s a ↔ IsLocalExtrOn g s a :=
  heq.isExtrFilter_iff <| heq.eq_of_nhdsWithin hmem

Local Extremum Criterion for Eventually Equal Functions on a Set

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in s \subseteq \alpha$. If $f$ and $g$ are eventually equal in a neighborhood of $a$ within $s$ (i.e., $f(x) = g(x)$ for all $x$ sufficiently close to $a$ in $s$), then $f$ has a local extremum on $s$ at $a$ if and only if $g$ has a local extremum on $s$ at $a$.

Filter.EventuallyLE.isLocalMax theorem

{f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝 a] f) (hfga : f a = g a) (h : IsLocalMax f a) : IsLocalMax g a

Full source

theorem Filter.EventuallyLE.isLocalMax {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝 a] f) (hfga : f a = g a)
    (h : IsLocalMax f a) : IsLocalMax g a :=
  hle.isMaxFilter hfga h

Local Maximum Preservation under Eventual Inequality and Pointwise Equality

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$ a point. If $g \leq f$ eventually in a neighborhood of $a$, $f(a) = g(a)$, and $f$ has a local maximum at $a$, then $g$ also has a local maximum at $a$.

IsLocalMax.congr theorem

{f g : α → β} {a : α} (h : IsLocalMax f a) (heq : f =ᶠ[𝓝 a] g) : IsLocalMax g a

Full source

nonrec theorem IsLocalMax.congr {f g : α → β} {a : α} (h : IsLocalMax f a) (heq : f =ᶠ[𝓝 a] g) :
    IsLocalMax g a :=
  h.congr heq heq.eq_of_nhds

Preservation of Local Maximum under Eventual Equality

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f$ has a local maximum at $a$ and $f$ is eventually equal to $g$ in a neighborhood of $a$, then $g$ also has a local maximum at $a$.

Filter.EventuallyEq.isLocalMax_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalMax f a ↔ IsLocalMax g a

Full source

theorem Filter.EventuallyEq.isLocalMax_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
    IsLocalMaxIsLocalMax f a ↔ IsLocalMax g a :=
  heq.isMaxFilter_iff heq.eq_of_nhds

Local Maximum Criterion for Eventually Equal Functions

Informal description

For functions $f, g : \alpha \to \beta$ and a point $a \in \alpha$, if $f$ and $g$ are eventually equal in a neighborhood of $a$ (i.e., $f(x) = g(x)$ for all $x$ sufficiently close to $a$), then $f$ has a local maximum at $a$ if and only if $g$ has a local maximum at $a$.

Filter.EventuallyLE.isLocalMin theorem

{f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝 a] g) (hfga : f a = g a) (h : IsLocalMin f a) : IsLocalMin g a

Full source

theorem Filter.EventuallyLE.isLocalMin {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝 a] g) (hfga : f a = g a)
    (h : IsLocalMin f a) : IsLocalMin g a :=
  hle.isMinFilter hfga h

Local minimum preservation under eventual inequality and point equality

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f \leq g$ eventually in a neighborhood of $a$, $f(a) = g(a)$, and $f$ has a local minimum at $a$, then $g$ also has a local minimum at $a$.

IsLocalMin.congr theorem

{f g : α → β} {a : α} (h : IsLocalMin f a) (heq : f =ᶠ[𝓝 a] g) : IsLocalMin g a

Full source

nonrec theorem IsLocalMin.congr {f g : α → β} {a : α} (h : IsLocalMin f a) (heq : f =ᶠ[𝓝 a] g) :
    IsLocalMin g a :=
  h.congr heq heq.eq_of_nhds

Preservation of Local Minimum under Eventually Equal Functions

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f$ has a local minimum at $a$ and $f$ is eventually equal to $g$ in a neighborhood of $a$ (i.e., $f = g$ for all $x$ sufficiently close to $a$), then $g$ also has a local minimum at $a$.

Filter.EventuallyEq.isLocalMin_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalMin f a ↔ IsLocalMin g a

Full source

theorem Filter.EventuallyEq.isLocalMin_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
    IsLocalMinIsLocalMin f a ↔ IsLocalMin g a :=
  heq.isMinFilter_iff heq.eq_of_nhds

Local Minimum Criterion under Eventual Equality

Informal description

For functions $f, g : \alpha \to \beta$ and a point $a \in \alpha$, if $f$ and $g$ are eventually equal in a neighborhood of $a$ (i.e., $f(x) = g(x)$ for all $x$ sufficiently close to $a$), then $f$ has a local minimum at $a$ if and only if $g$ has a local minimum at $a$.

IsLocalExtr.congr theorem

{f g : α → β} {a : α} (h : IsLocalExtr f a) (heq : f =ᶠ[𝓝 a] g) : IsLocalExtr g a

Full source

nonrec theorem IsLocalExtr.congr {f g : α → β} {a : α} (h : IsLocalExtr f a) (heq : f =ᶠ[𝓝 a] g) :
    IsLocalExtr g a :=
  h.congr heq heq.eq_of_nhds

Preservation of Local Extrema under Eventual Equality

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f$ has a local extremum at $a$ and $f$ is eventually equal to $g$ in a neighborhood of $a$, then $g$ also has a local extremum at $a$.

Filter.EventuallyEq.isLocalExtr_iff theorem

{f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) : IsLocalExtr f a ↔ IsLocalExtr g a

Full source

theorem Filter.EventuallyEq.isLocalExtr_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
    IsLocalExtrIsLocalExtr f a ↔ IsLocalExtr g a :=
  heq.isExtrFilter_iff heq.eq_of_nhds

Local extremum is preserved under eventual equality

Informal description

Let $f, g : \alpha \to \beta$ be functions and $a \in \alpha$. If $f$ and $g$ are eventually equal in a neighborhood of $a$ (i.e., $f = g$ for all points sufficiently close to $a$), then $f$ has a local extremum at $a$ if and only if $g$ has a local extremum at $a$.

isLocalMax_of_mono_anti' theorem

 {α : Type*} [TopologicalSpace α] [LinearOrder α] {β : Type*} [Preorder β] {b : α} {f : α → β} {a : Set α}
  (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b) (h₀ : MonotoneOn f a) (h₁ : AntitoneOn f c) : IsLocalMax f b

Full source

/-- If `f` is monotone to the left and antitone to the right, then it has a local maximum. -/
lemma isLocalMax_of_mono_anti' {α : Type*} [TopologicalSpace α] [LinearOrder α]
    {β : Type*} [Preorder β] {b : α} {f : α → β}
    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
    (h₀ : MonotoneOn f a) (h₁ : AntitoneOn f c) : IsLocalMax f b :=
  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)

Local maximum from left-monotone right-antitone function

Informal description

Let $\alpha$ be a topological space with a linear order, $\beta$ a preorder, and $f : \alpha \to \beta$ a function. For a point $b \in \alpha$, suppose there exist sets $a$ and $c$ such that: 1. $a$ is a neighborhood of $b$ in the left order topology (i.e., $a \in \mathcal{N}_{\leq}(b)$) 2. $c$ is a neighborhood of $b$ in the right order topology (i.e., $c \in \mathcal{N}_{\geq}(b)$) 3. $f$ is monotone on $a$ 4. $f$ is antitone on $c$ Then $f$ has a local maximum at $b$.

isLocalMin_of_anti_mono' theorem

 {α : Type*} [TopologicalSpace α] [LinearOrder α] {β : Type*} [Preorder β] {b : α} {f : α → β} {a : Set α}
  (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b) (h₀ : AntitoneOn f a) (h₁ : MonotoneOn f c) : IsLocalMin f b

Full source

/-- If `f` is antitone to the left and monotone to the right, then it has a local minimum. -/
lemma isLocalMin_of_anti_mono' {α : Type*} [TopologicalSpace α] [LinearOrder α]
    {β : Type*} [Preorder β] {b : α} {f : α → β}
    {a : Set α} (ha : a ∈ 𝓝[≤] b) {c : Set α} (hc : c ∈ 𝓝[≥] b)
    (h₀ : AntitoneOn f a) (h₁ : MonotoneOn f c) : IsLocalMin f b :=
  have : b ∈ a := mem_of_mem_nhdsWithin (by simp) ha
  have : b ∈ c := mem_of_mem_nhdsWithin (by simp) hc
  mem_of_superset (nhds_of_Ici_Iic ha hc) (fun x _ => by rcases le_total x b <;> aesop)

Local Minimum from Antitone-Left and Monotone-Right Behavior

Informal description

Let $\alpha$ be a topological space with a linear order, $\beta$ a preorder, and $f : \alpha \to \beta$ a function. Suppose there exist sets $a$ and $c$ in $\alpha$ such that: 1. $a$ is a neighborhood of $b$ to the left (i.e., $a \in \mathcal{N}_{\leq}(b)$), 2. $c$ is a neighborhood of $b$ to the right (i.e., $c \in \mathcal{N}_{\geq}(b)$), 3. $f$ is antitone on $a$ (i.e., $f$ is decreasing on $a$), 4. $f$ is monotone on $c$ (i.e., $f$ is increasing on $c$). Then $f$ has a local minimum at $b$.

Mathlib.Topology.Order.LocalExtr

Main definitions

Main statements