<commit_before>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import order.filter.extr
import topology.continuous_on

/-!
# Local extrema of functions on topological spaces

## Main definitions

This file defines special versions of `is_*_filter f a l`, `*=min/max/extr`,
from `order/filter/extr` for two kinds of filters: `nhds_within` and `nhds`.
These versions are called `is_local_*_on` and `is_local_*`, respectively.

## Main statements

Many lemmas in this file restate those from `order/filter/extr`, and you can find
a detailed documentation there. These convenience lemmas are provided only to make the dot notation
return propositions of expected types, not just `is_*_filter`.

Here is the list of statements specific to these two types of filters:

* `is_local_*.on`, `is_local_*_on.on_subset`: restrict to a subset;
* `is_local_*_on.inter` : intersect the set with another one;
* `is_*_on.localize` : a global extremum is a local extremum too.
* `is_[local_]*_on.is_local_*` : if we have `is_local_*_on f s a` and `s ∈ 𝓝 a`,
  then we have `is_local_* f a`.

-/

universes u v w x

variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α]

open set filter
open_locale topological_space filter

section preorder

variables [preorder β] [preorder γ] (f : α → β) (s : set α) (a : α)

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

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

/-- `is_local_extr_on f s a` means `is_local_min_on f s a ∨ is_local_max_on f s a`. -/
def is_local_extr_on := is_extr_filter f (𝓝[s] a) a

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

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

/-- `is_local_extr_on f s a` means `is_local_min_on f s a ∨ is_local_max_on f s a`. -/
def is_local_extr := is_extr_filter f (𝓝 a) a

variables {f s a}

lemma is_local_extr_on.elim {p : Prop} :
  is_local_extr_on f s a → (is_local_min_on f s a → p) → (is_local_max_on f s a → p) → p :=
or.elim

lemma is_local_extr.elim {p : Prop} :
  is_local_extr f a → (is_local_min f a → p) → (is_local_max f a → p) → p :=
or.elim

/-! ### Restriction to (sub)sets -/

lemma is_local_min.on (h : is_local_min f a) (s) : is_local_min_on f s a :=
h.filter_inf _

lemma is_local_max.on (h : is_local_max f a) (s) : is_local_max_on f s a :=
h.filter_inf _

lemma is_local_extr.on (h : is_local_extr f a) (s) : is_local_extr_on f s a :=
h.filter_inf _

lemma is_local_min_on.on_subset {t : set α} (hf : is_local_min_on f t a) (h : s ⊆ t) :
  is_local_min_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_max_on.on_subset {t : set α} (hf : is_local_max_on f t a) (h : s ⊆ t) :
  is_local_max_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_extr_on.on_subset {t : set α} (hf : is_local_extr_on f t a) (h : s ⊆ t) :
  is_local_extr_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_min_on.inter (hf : is_local_min_on f s a) (t) : is_local_min_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_local_max_on.inter (hf : is_local_max_on f s a) (t) : is_local_max_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_local_extr_on.inter (hf : is_local_extr_on f s a) (t) : is_local_extr_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_min_on.localize (hf : is_min_on f s a) : is_local_min_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_max_on.localize (hf : is_max_on f s a) : is_local_max_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_extr_on.localize (hf : is_extr_on f s a) : is_local_extr_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_local_min_on.is_local_min (hf : is_local_min_on f s a) (hs : s ∈ 𝓝 a) : is_local_min f a :=
have 𝓝 a ≤ 𝓟 s, from le_principal_iff.2 hs,
hf.filter_mono $ le_inf (le_refl _) this

lemma is_local_max_on.is_local_max (hf : is_local_max_on f s a) (hs : s ∈ 𝓝 a) : is_local_max f a :=
have 𝓝 a ≤ 𝓟 s, from le_principal_iff.2 hs,
hf.filter_mono $ le_inf (le_refl _) this

lemma is_local_extr_on.is_local_extr (hf : is_local_extr_on f s a) (hs : s ∈ 𝓝 a) :
  is_local_extr f a :=
hf.elim (λ hf, (hf.is_local_min hs).is_extr) (λ hf, (hf.is_local_max hs).is_extr)

lemma is_min_on.is_local_min (hf : is_min_on f s a) (hs : s ∈ 𝓝 a) : is_local_min f a :=
hf.localize.is_local_min hs

lemma is_max_on.is_local_max (hf : is_max_on f s a) (hs : s ∈ 𝓝 a) : is_local_max f a :=
hf.localize.is_local_max hs

lemma is_extr_on.is_local_extr (hf : is_extr_on f s a) (hs : s ∈ 𝓝 a) : is_local_extr f a :=
hf.localize.is_local_extr hs

/-! ### Constant -/

lemma is_local_min_on_const {b : β} : is_local_min_on (λ _, b) s a := is_min_filter_const
lemma is_local_max_on_const {b : β} : is_local_max_on (λ _, b) s a := is_max_filter_const
lemma is_local_extr_on_const {b : β} : is_local_extr_on (λ _, b) s a := is_extr_filter_const

lemma is_local_min_const {b : β} : is_local_min (λ _, b) a := is_min_filter_const
lemma is_local_max_const {b : β} : is_local_max (λ _, b) a := is_max_filter_const
lemma is_local_extr_const {b : β} : is_local_extr (λ _, b) a := is_extr_filter_const

/-! ### Composition with (anti)monotone functions -/<commit_msg>feat(topology/local_extr): not locally surjective at a local extr (#6076)<commit_after>/-
Copyright (c) 2019 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import order.filter.extr
import topology.continuous_on

/-!
# Local extrema of functions on topological spaces

## Main definitions

This file defines special versions of `is_*_filter f a l`, `*=min/max/extr`,
from `order/filter/extr` for two kinds of filters: `nhds_within` and `nhds`.
These versions are called `is_local_*_on` and `is_local_*`, respectively.

## Main statements

Many lemmas in this file restate those from `order/filter/extr`, and you can find
a detailed documentation there. These convenience lemmas are provided only to make the dot notation
return propositions of expected types, not just `is_*_filter`.

Here is the list of statements specific to these two types of filters:

* `is_local_*.on`, `is_local_*_on.on_subset`: restrict to a subset;
* `is_local_*_on.inter` : intersect the set with another one;
* `is_*_on.localize` : a global extremum is a local extremum too.
* `is_[local_]*_on.is_local_*` : if we have `is_local_*_on f s a` and `s ∈ 𝓝 a`,
  then we have `is_local_* f a`.

-/

universes u v w x

variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [topological_space α]

open set filter
open_locale topological_space filter

section preorder

variables [preorder β] [preorder γ] (f : α → β) (s : set α) (a : α)

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

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

/-- `is_local_extr_on f s a` means `is_local_min_on f s a ∨ is_local_max_on f s a`. -/
def is_local_extr_on := is_extr_filter f (𝓝[s] a) a

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

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

/-- `is_local_extr_on f s a` means `is_local_min_on f s a ∨ is_local_max_on f s a`. -/
def is_local_extr := is_extr_filter f (𝓝 a) a

variables {f s a}

lemma is_local_extr_on.elim {p : Prop} :
  is_local_extr_on f s a → (is_local_min_on f s a → p) → (is_local_max_on f s a → p) → p :=
or.elim

lemma is_local_extr.elim {p : Prop} :
  is_local_extr f a → (is_local_min f a → p) → (is_local_max f a → p) → p :=
or.elim

/-! ### Restriction to (sub)sets -/

lemma is_local_min.on (h : is_local_min f a) (s) : is_local_min_on f s a :=
h.filter_inf _

lemma is_local_max.on (h : is_local_max f a) (s) : is_local_max_on f s a :=
h.filter_inf _

lemma is_local_extr.on (h : is_local_extr f a) (s) : is_local_extr_on f s a :=
h.filter_inf _

lemma is_local_min_on.on_subset {t : set α} (hf : is_local_min_on f t a) (h : s ⊆ t) :
  is_local_min_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_max_on.on_subset {t : set α} (hf : is_local_max_on f t a) (h : s ⊆ t) :
  is_local_max_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_extr_on.on_subset {t : set α} (hf : is_local_extr_on f t a) (h : s ⊆ t) :
  is_local_extr_on f s a :=
hf.filter_mono $ nhds_within_mono a h

lemma is_local_min_on.inter (hf : is_local_min_on f s a) (t) : is_local_min_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_local_max_on.inter (hf : is_local_max_on f s a) (t) : is_local_max_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_local_extr_on.inter (hf : is_local_extr_on f s a) (t) : is_local_extr_on f (s ∩ t) a :=
hf.on_subset (inter_subset_left s t)

lemma is_min_on.localize (hf : is_min_on f s a) : is_local_min_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_max_on.localize (hf : is_max_on f s a) : is_local_max_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_extr_on.localize (hf : is_extr_on f s a) : is_local_extr_on f s a :=
hf.filter_mono $ inf_le_right

lemma is_local_min_on.is_local_min (hf : is_local_min_on f s a) (hs : s ∈ 𝓝 a) : is_local_min f a :=
have 𝓝 a ≤ 𝓟 s, from le_principal_iff.2 hs,
hf.filter_mono $ le_inf (le_refl _) this

lemma is_local_max_on.is_local_max (hf : is_local_max_on f s a) (hs : s ∈ 𝓝 a) : is_local_max f a :=
have 𝓝 a ≤ 𝓟 s, from le_principal_iff.2 hs,
hf.filter_mono $ le_inf (le_refl _) this

lemma is_local_extr_on.is_local_extr (hf : is_local_extr_on f s a) (hs : s ∈ 𝓝 a) :
  is_local_extr f a :=
hf.elim (λ hf, (hf.is_local_min hs).is_extr) (λ hf, (hf.is_local_max hs).is_extr)

lemma is_min_on.is_local_min (hf : is_min_on f s a) (hs : s ∈ 𝓝 a) : is_local_min f a :=
hf.localize.is_local_min hs

lemma is_max_on.is_local_max (hf : is_max_on f s a) (hs : s ∈ 𝓝 a) : is_local_max f a :=
hf.localize.is_local_max hs

lemma is_extr_on.is_local_extr (hf : is_extr_on f s a) (hs : s ∈ 𝓝 a) : is_local_extr f a :=
hf.localize.is_local_extr hs

lemma is_local_min_on.not_nhds_le_map [topological_space β]
  (hf : is_local_min_on f s a) [ne_bot (𝓝[Iio (f a)] (f a))] :
  ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
λ hle,
have ∀ᶠ y in 𝓝[Iio (f a)] (f a), f a ≤ y,
  from (eventually_map.2 hf).filter_mono (inf_le_left.trans hle),
let ⟨y, hy⟩ := (this.and self_mem_nhds_within).exists in hy.1.not_lt hy.2

lemma is_local_max_on.not_nhds_le_map [topological_space β]
  (hf : is_local_max_on f s a) [ne_bot (𝓝[Ioi (f a)] (f a))] :
  ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
@is_local_min_on.not_nhds_le_map α (order_dual β) _ _ _ _ _ ‹_› hf ‹_›

lemma is_local_extr_on.not_nhds_le_map [topological_space β]
  (hf : is_local_extr_on f s a) [ne_bot (𝓝[Iio (f a)] (f a))] [ne_bot (𝓝[Ioi (f a)] (f a))] :
  ¬𝓝 (f a) ≤ map f (𝓝[s] a) :=
hf.elim (λ h, h.not_nhds_le_map) (λ h, h.not_nhds_le_map)

/-! ### Constant -/

lemma is_local_min_on_const {b : β} : is_local_min_on (λ _, b) s a := is_min_filter_const
lemma is_local_max_on_const {b : β} : is_local_max_on (λ _, b) s a := is_max_filter_const
lemma is_local_extr_on_const {b : β} : is_local_extr_on (λ _, b) s a := is_extr_filter_const

lemma is_local_min_const {b : β} : is_local_min (λ _, b) a := is_min_filter_const
lemma is_local_max_const {b : β} : is_local_max (λ _, b) a := is_max_filter_const
lemma is_local_extr_const {b : β} : is_local_extr (λ _, b) a := is_extr_filter_const

/-! ### Composition with (anti)monotone functions -/
{'fraction_non_alphanumeric': 0.1172362185083562, 'fraction_numerical': 0.0019123638480086473, 'mean_word_length': 3.933552091878589, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 7, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '898687', 'n_tokens_mistral': 5414, 'n_tokens_neox': 5362, 'n_words': 1703}