feat(order/filter/extr, topology/local_extr): links between extremas …

…of two eventually le/eq functions (#3624)

Add many lemmas that look similar to e.g : if f and g are equal at `a`, and `f ≤ᶠ[l] g` for some filter `l`, then `is_min_filter l f a`implies `is_min_filter l g a`

src/order/filter/extr.lean

@@ -477,3 +477,56 @@ lemma is_max_on.max (hf : is_max_on f s a) (hg : is_max_on g s a) :
 hf.max hg
 
 end decidable_linear_order
+
+section eventually
+
+/-! ### Relation with `eventually` comparisons of two functions -/
+
+lemma filter.eventually_le.is_max_filter {α β : Type*} [preorder β] {f g : α → β} {a : α}
+  {l : filter α} (hle : g ≤ᶠ[l] f) (hfga : f a = g a) (h : is_max_filter f l a) :
+  is_max_filter g l a :=
+begin
+  refine hle.mp (h.mono $ λ x hf hgf, _),
+  rw ← hfga,
+  exact le_trans hgf hf
+end
+
+lemma is_max_filter.congr {α β : Type*} [preorder β] {f g : α → β} {a : α} {l : filter α}
+  (h : is_max_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_max_filter g l a :=
+heq.symm.le.is_max_filter hfga h
+
+lemma filter.eventually_eq.is_max_filter_iff {α β : Type*} [preorder β] {f g : α → β} {a : α}
+  {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_max_filter f l a ↔ is_max_filter g l a :=
+⟨λ h, h.congr heq hfga, λ h, h.congr heq.symm hfga.symm⟩
+
+lemma filter.eventually_le.is_min_filter {α β : Type*} [preorder β] {f g : α → β} {a : α}
+  {l : filter α} (hle : f ≤ᶠ[l] g) (hfga : f a = g a) (h : is_min_filter f l a) :
+  is_min_filter g l a :=
+@filter.eventually_le.is_max_filter _ (order_dual β) _ _ _ _ _ hle hfga h
+
+lemma is_min_filter.congr {α β : Type*} [preorder β] {f g : α → β} {a : α} {l : filter α}
+  (h : is_min_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_min_filter g l a :=
+heq.le.is_min_filter hfga h
+
+lemma filter.eventually_eq.is_min_filter_iff {α β : Type*} [preorder β] {f g : α → β} {a : α}
+  {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_min_filter f l a ↔ is_min_filter g l a :=
+⟨λ h, h.congr heq hfga, λ h, h.congr heq.symm hfga.symm⟩
+
+lemma is_extr_filter.congr {α β : Type*} [preorder β] {f g : α → β} {a : α} {l : filter α}
+  (h : is_extr_filter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_extr_filter g l a :=
+begin
+  rw is_extr_filter at *,
+  rwa [← heq.is_max_filter_iff hfga, ← heq.is_min_filter_iff hfga],
+end
+
+lemma filter.eventually_eq.is_extr_filter_iff {α β : Type*} [preorder β] {f g : α → β} {a : α}
+  {l : filter α} (heq : f =ᶠ[l] g) (hfga : f a = g a) :
+  is_extr_filter f l a ↔ is_extr_filter g l a :=
+⟨λ h, h.congr heq hfga, λ h, h.congr heq.symm hfga.symm⟩
+
+end eventually

src/topology/continuous_on.lean

@@ -247,6 +247,10 @@ lemma tendsto_nhds_within_of_tendsto_nhds_of_eventually_within {β : Type*} {a :
   tendsto f l (nhds_within a s) :=
 tendsto_inf.2 ⟨h1, tendsto_principal.2 h2⟩
 
+lemma filter.eventually_eq.eq_of_nhds_within {s : set α} {f g : α → β} {a : α}
+  (h : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : f a = g a :=
+h.self_of_nhds_within hmem
+
 /-
 nhds_within and subtypes
 -/

src/topology/local_extr.lean

@@ -423,3 +423,75 @@ lemma is_local_max_on.max (hf : is_local_max_on f s a) (hg : is_local_max_on g s
 hf.max hg
 
 end decidable_linear_order
+
+section eventually
+
+/-! ### Relation with `eventually` comparisons of two functions -/
+
+variables [preorder β] {s : set α}
+
+lemma filter.eventually_le.is_local_max_on {f g : α → β} {a : α} (hle : g ≤ᶠ[nhds_within a s] f)
+  (hfga : f a = g a) (h : is_local_max_on f s a) : is_local_max_on g s a :=
+hle.is_max_filter hfga h
+
+lemma is_local_max_on.congr {f g : α → β} {a : α} (h : is_local_max_on f s a)
+  (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_max_on g s a :=
+h.congr heq $ heq.eq_of_nhds_within hmem
+
+lemma filter.eventually_eq.is_local_max_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g)
+  (hmem : a ∈ s) : is_local_max_on f s a ↔ is_local_max_on g s a :=
+heq.is_max_filter_iff $ heq.eq_of_nhds_within hmem
+
+lemma filter.eventually_le.is_local_min_on {f g : α → β} {a : α} (hle : f ≤ᶠ[nhds_within a s] g)
+  (hfga : f a = g a) (h : is_local_min_on f s a) : is_local_min_on g s a :=
+hle.is_min_filter hfga h
+
+lemma is_local_min_on.congr {f g : α → β} {a : α} (h : is_local_min_on f s a)
+  (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_min_on g s a :=
+h.congr heq $ heq.eq_of_nhds_within hmem
+
+lemma filter.eventually_eq.is_local_min_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g)
+  (hmem : a ∈ s) : is_local_min_on f s a ↔ is_local_min_on g s a :=
+heq.is_min_filter_iff $ heq.eq_of_nhds_within hmem
+
+lemma is_local_extr_on.congr {f g : α → β} {a : α} (h : is_local_extr_on f s a)
+  (heq : f =ᶠ[nhds_within a s] g) (hmem : a ∈ s) : is_local_extr_on g s a :=
+h.congr heq $ heq.eq_of_nhds_within hmem
+
+lemma filter.eventually_eq.is_local_extr_on_iff {f g : α → β} {a : α} (heq : f =ᶠ[nhds_within a s] g)
+  (hmem : a ∈ s) : is_local_extr_on f s a ↔ is_local_extr_on g s a :=
+heq.is_extr_filter_iff $ heq.eq_of_nhds_within hmem
+
+lemma filter.eventually_le.is_local_max {f g : α → β} {a : α} (hle : g ≤ᶠ[𝓝 a] f) (hfga : f a = g a)
+  (h : is_local_max f a) : is_local_max g a :=
+hle.is_max_filter hfga h
+
+lemma is_local_max.congr {f g : α → β} {a : α} (h : is_local_max f a) (heq : f =ᶠ[𝓝 a] g) :
+  is_local_max g a :=
+h.congr heq heq.eq_of_nhds
+
+lemma filter.eventually_eq.is_local_max_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
+  is_local_max f a ↔ is_local_max g a :=
+heq.is_max_filter_iff heq.eq_of_nhds
+
+lemma filter.eventually_le.is_local_min {f g : α → β} {a : α} (hle : f ≤ᶠ[𝓝 a] g) (hfga : f a = g a)
+  (h : is_local_min f a) : is_local_min g a :=
+hle.is_min_filter hfga h
+
+lemma is_local_min.congr {f g : α → β} {a : α} (h : is_local_min f a) (heq : f =ᶠ[𝓝 a] g) :
+  is_local_min g a :=
+h.congr heq heq.eq_of_nhds
+
+lemma filter.eventually_eq.is_local_min_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
+  is_local_min f a ↔ is_local_min g a :=
+heq.is_min_filter_iff heq.eq_of_nhds
+
+lemma is_local_extr.congr {f g : α → β} {a : α} (h : is_local_extr f a) (heq : f =ᶠ[𝓝 a] g) :
+  is_local_extr g a :=
+h.congr heq heq.eq_of_nhds
+
+lemma filter.eventually_eq.is_local_extr_iff {f g : α → β} {a : α} (heq : f =ᶠ[𝓝 a] g) :
+  is_local_extr f a ↔ is_local_extr g a :=
+heq.is_extr_filter_iff heq.eq_of_nhds
+
+end eventually