Update mathlib, generalizing some AnalyticManifold theory to boundaries

`HolomorphicAt` is now `MAnalyticAt` per zulip discussion.

Ray/Analytic/Within.lean

@@ -0,0 +1,47 @@
+import Mathlib.Analysis.Analytic.Within
+import Mathlib.Tactic.Bound
+import Ray.Misc.Topology
+
+/-!
+## Facts about `AnalyticWithin`
+-/
+
+open Filter (atTop)
+open Set
+open scoped Real ENNReal Topology
+noncomputable section
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+
+variable {E F G H : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F]
+  [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [NormedAddCommGroup H]
+  [NormedSpace 𝕜 H]
+
+/-- Congruence w.r.t. the set -/
+lemma AnalyticWithinAt.congr_set {f : E → F} {s t : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x)
+    (hst : (· ∈ s) =ᶠ[𝓝 x] (· ∈ t)) : AnalyticWithinAt 𝕜 f t x := by
+  rcases Metric.eventually_nhds_iff.mp hst with ⟨e, e0, st⟩
+  rcases hf with ⟨p, r, hp⟩
+  exact ⟨p, min (.ofReal e) r, {
+    r_le := min_le_of_right_le hp.r_le
+    r_pos := by bound
+    hasSum := by
+      intro y m n
+      simp only [EMetric.mem_ball, lt_min_iff, edist_lt_ofReal, dist_zero_right] at m n ⊢
+      exact hp.hasSum (by simpa only [mem_def, dist_self_add_left, n.1, @st (x + y)]) n.2
+    continuousWithinAt := by
+      have e : 𝓝[s] x = 𝓝[t] x := nhdsWithin_eq_iff_eventuallyEq.mpr hst
+      simpa only [ContinuousWithinAt, e] using hp.continuousWithinAt }⟩
+
+/-- Analyticity within is open (within the set) -/
+lemma AnalyticWithinAt.eventually_analyticWithinAt [CompleteSpace F] {f : E → F} {s : Set E} {x : E}
+    (hf : AnalyticWithinAt 𝕜 f s x) : ∀ᶠ y in 𝓝[s] x, AnalyticWithinAt 𝕜 f s y := by
+  obtain ⟨_, g, fg, ga⟩ := analyticWithinAt_iff_exists_analyticAt.mp hf
+  simp only [Filter.EventuallyEq, eventually_nhdsWithin_iff] at fg ⊢
+  filter_upwards [fg.eventually_nhds, ga.eventually_analyticAt]
+  intro z fg ga zs
+  refine analyticWithinAt_iff_exists_analyticAt.mpr ⟨?_, g, ?_, ga⟩
+  · refine ga.continuousAt.continuousWithinAt.congr_of_eventuallyEq ?_ (fg.self_of_nhds zs)
+    rw [← eventually_nhdsWithin_iff] at fg
+    exact fg
+  · simpa only [Filter.EventuallyEq, eventually_nhdsWithin_iff]

Ray/AnalyticManifold/Inverse.lean

@@ -59,8 +59,8 @@ def Cinv.h (i : Cinv f c z) : ℂ × ℂ → ℂ × ℂ := fun x ↦ (x.1, i.f'
 -- f' and h are analytic
 theorem Cinv.fa' (i : Cinv f c z) : AnalyticAt ℂ i.f' (c, i.z') := by
   have fa := i.fa
-  simp only [mAnalyticAt_iff, uncurry, extChartAt_prod, Function.comp, PartialEquiv.prod_coe_symm,
-    PartialEquiv.prod_coe] at fa
+  simp only [mAnalyticAt_iff_of_boundaryless, uncurry, extChartAt_prod, Function.comp,
+    PartialEquiv.prod_coe_symm, PartialEquiv.prod_coe] at fa
   exact fa.2
 theorem Cinv.ha (i : Cinv f c z) : AnalyticAt ℂ i.h (c, i.z') := (analyticAt_fst _).prod i.fa'
 

Ray/AnalyticManifold/Nontrivial.lean

@@ -187,7 +187,7 @@ theorem eq_of_pow_eq {p q : X → ℂ} {t : Set X} {d : ℕ} (pc : ContinuousOn
 theorem MAnalyticAt.eventually_eq_or_eventually_ne [T2Space T] {f g : S → T} {z : S}
     (fa : MAnalyticAt I I f z) (ga : MAnalyticAt I I g z) :
     (∀ᶠ w in 𝓝 z, f w = g w) ∨ ∀ᶠ w in 𝓝[{z}ᶜ] z, f w ≠ g w := by
-  simp only [mAnalyticAt_iff, Function.comp] at fa ga
+  simp only [mAnalyticAt_iff_of_boundaryless, Function.comp] at fa ga
   rcases fa with ⟨fc, fa⟩; rcases ga with ⟨gc, ga⟩
   by_cases fg : f z ≠ g z
   · right; contrapose fg; simp only [not_not]
@@ -441,7 +441,10 @@ theorem MAnalyticOn.eq_of_locally_eq [CompleteSpace F] {f g : M → N} [T2Space
       apply ((continuousAt_extChartAt_symm'' J m).eventually e).mp
       refine .of_forall fun z e ↦ ?_; simp only at e
       simp only [← hd, Pi.zero_apply, sub_eq_zero, ex, e]
-    have da : AnalyticAt ℂ d z := by rw [← hd, ← hz]; exact (fa _ xs).2.sub (ga _ xs).2
+    have da : AnalyticAt ℂ d z := by
+      rw [← hd, ← hz]
+      exact (mAnalyticAt_iff_of_boundaryless.mp (fa _ xs)).2.sub
+        (mAnalyticAt_iff_of_boundaryless.mp (ga _ xs)).2
     clear hd ex ex' xt t e fa ga f g xs hz x sp ht
     -- Forget about manifolds
     rcases da.exists_ball_analyticOn with ⟨r, rp, da⟩

Ray/AnalyticManifold/OneDimension.lean

@@ -378,7 +378,7 @@ theorem isClosed_critical {f : ℂ → S → T} (fa : MAnalytic II I (uncurry f)
 theorem osgoodManifold {f : S × T → U} (fc : Continuous f)
     (f0 : ∀ x y, MAnalyticAt I I (fun x ↦ f (x, y)) x)
     (f1 : ∀ x y, MAnalyticAt I I (fun y ↦ f (x, y)) y) : MAnalytic II I f := by
-  rw [mAnalytic_iff]; use fc; intro p; apply osgood_at'
+  rw [mAnalytic_iff_of_boundaryless]; use fc; intro p; apply osgood_at'
   have fm : ∀ᶠ q in 𝓝 (extChartAt II p p),
       f ((extChartAt II p).symm q) ∈ (extChartAt I (f p)).source := by
     refine (fc.continuousAt.comp (continuousAt_extChartAt_symm II p)).eventually_mem

Ray/AnalyticManifold/OpenMapping.lean

@@ -182,7 +182,7 @@ theorem NontrivialMAnalyticAt.nhds_le_map_nhds_param' {f : ℂ → ℂ → ℂ}
 theorem NontrivialMAnalyticAt.inCharts {f : S → T} {z : S} (n : NontrivialMAnalyticAt f z) :
     NontrivialMAnalyticAt (fun w ↦ extChartAt I (f z) (f ((extChartAt I z).symm w)))
       (extChartAt I z z) := by
-  use n.mAnalyticAt.2.mAnalyticAt I I
+  use (mAnalyticAt_iff_of_boundaryless.mp n.mAnalyticAt).2.mAnalyticAt I I
   have c := n.nonconst; contrapose c
   simp only [Filter.not_frequently, not_not, ← extChartAt_map_nhds' I z,
     Filter.eventually_map] at c ⊢
@@ -201,7 +201,8 @@ theorem NontrivialMAnalyticAt.nhds_eq_map_nhds [AnalyticManifold I T] {f : S →
     (n : NontrivialMAnalyticAt f z) : 𝓝 (f z) = Filter.map f (𝓝 z) := by
   refine le_antisymm ?_ n.mAnalyticAt.continuousAt
   generalize hg : (fun x ↦ extChartAt I (f z) (f ((extChartAt I z).symm x))) = g
-  have ga : AnalyticAt ℂ g (extChartAt I z z) := by rw [← hg]; exact n.mAnalyticAt.2
+  have ga : AnalyticAt ℂ g (extChartAt I z z) := by
+    rw [← hg]; exact (mAnalyticAt_iff_of_boundaryless.mp n.mAnalyticAt).2
   cases' ga.eventually_constant_or_nhds_le_map_nhds with h h
   · contrapose h; clear h; simp only [Filter.not_eventually]
     apply n.inCharts.nonconst.mp; simp only [← hg, Ne, imp_self, Filter.eventually_true]
@@ -237,7 +238,7 @@ theorem NontrivialMAnalyticAt.nhds_eq_map_nhds_param [AnalyticManifold I T] {f :
   refine le_antisymm ?_ (continuousAt_fst.prod fa.continuousAt)
   generalize hg : (fun e x ↦ extChartAt I (f c z) (f e ((extChartAt I z).symm x))) = g
   have ga : AnalyticAt ℂ (uncurry g) (c, extChartAt I z z) := by
-    rw [← hg]; exact (mAnalyticAt_iff.mp fa).2
+    rw [← hg]; exact (mAnalyticAt_iff_of_boundaryless.mp fa).2
   have gn : NontrivialMAnalyticAt (g c) (extChartAt I z z) := by rw [← hg]; exact n.inCharts
   have h := gn.nhds_le_map_nhds_param' ga
   -- We follow the 𝓝 ≤ 𝓝 argument of nontrivial_mAnalytic_at.nhds_le_map_nhds

Ray/AnalyticManifold/RiemannSphere.lean

@@ -369,21 +369,27 @@ theorem prod_mem_inf_of_mem_atInf {s : Set (X × ℂ)} {x : X} (f : s ∈ (𝓝
 
 /-- `coe : ℂ → 𝕊` is analytic -/
 theorem mAnalytic_coe : MAnalytic I I (fun z : ℂ ↦ (z : 𝕊)) := by
-  rw [mAnalytic_iff]; use continuous_coe; intro z
+  rw [mAnalytic_iff_of_boundaryless]; use continuous_coe; intro z
   simp only [extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_symm, PartialEquiv.refl_coe,
     Function.comp_id, id_eq, Function.comp, PartialEquiv.invFun_as_coe]
-  rw [← PartialEquiv.invFun_as_coe]; simp only [coePartialEquiv, toComplex_coe]; apply analyticAt_id
+  rw [← PartialEquiv.invFun_as_coe]
+  simp only [coePartialEquiv, toComplex_coe]
+  apply analyticAt_id
 
 /-- `OnePoint.toComplex : 𝕊 → ℂ` is analytic except at `∞` -/
 theorem mAnalyticAt_toComplex {z : ℂ} : MAnalyticAt I I (OnePoint.toComplex : 𝕊 → ℂ) z := by
-  rw [mAnalyticAt_iff]; use continuousAt_toComplex
+  rw [mAnalyticAt_iff_of_boundaryless]
+  use continuousAt_toComplex
   simp only [toComplex_coe, Function.comp, extChartAt_coe, extChartAt_eq_refl, PartialEquiv.refl_coe,
     id, PartialEquiv.symm_symm, coePartialEquiv_apply, coePartialEquiv_symm_apply]
   apply analyticAt_id
 
 /-- Inversion is analytic -/
 theorem mAnalytic_inv : MAnalytic I I fun z : 𝕊 ↦ z⁻¹ := by
-  rw [mAnalytic_iff]; use continuous_inv; intro z; induction' z using OnePoint.rec with z
+  rw [mAnalytic_iff_of_boundaryless]
+  use continuous_inv
+  intro z
+  induction' z using OnePoint.rec with z
   · simp only [inv_inf, extChartAt_inf, ← coe_zero, extChartAt_coe, Function.comp,
       PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, coePartialEquiv_symm_apply,
       toComplex_coe, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm, coePartialEquiv_apply,
@@ -464,7 +470,8 @@ theorem mAnalyticAt_fill_coe {f : ℂ → T} {y : T} (fa : MAnalyticAt I I f z)
 theorem mAnalyticAt_fill_inf [AnalyticManifold I T] {f : ℂ → T} {y : T}
     (fa : ∀ᶠ z in atInf, MAnalyticAt I I f z) (fi : Tendsto f atInf (𝓝 y)) :
     MAnalyticAt I I (fill f y) ∞ := by
-  rw [mAnalyticAt_iff]; use continuousAt_fill_inf fi
+  rw [mAnalyticAt_iff_of_boundaryless]
+  use continuousAt_fill_inf fi
   simp only [Function.comp, extChartAt, PartialHomeomorph.extend, fill, rec_inf,
     modelWithCornersSelf_partialEquiv, PartialEquiv.trans_refl, chartAt_inf,
     PartialHomeomorph.symm_toPartialEquiv, PartialEquiv.symm_symm, PartialHomeomorph.toFun_eq_coe,

Ray/AnalyticManifold/SmoothManifoldWithCorners.lean

@@ -208,4 +208,55 @@ theorem mfderiv_comp' {f : M → N} (x : M) {g : N → O} (hg : MDifferentiableA
     mfderiv I K (fun x ↦ g (f x)) x = (mfderiv J K g (f x)).comp (mfderiv I J f x) :=
   mfderiv_comp _ hg hf
 
+/-- Chart derivatives are invertible (left inverse) -/
+theorem extChartAt_mderiv_left_inverse [I.Boundaryless] {x y : M}
+    (m : y ∈ (extChartAt I x).source) :
+    (mfderiv (modelWithCornersSelf 𝕜 E) I (extChartAt I x).symm (extChartAt I x y)).comp
+        (mfderiv I (modelWithCornersSelf 𝕜 E) (extChartAt I x) y) =
+      ContinuousLinearMap.id 𝕜 (TangentSpace I y) := by
+  have m' : extChartAt I x y ∈ (extChartAt I x).target := PartialEquiv.map_source _ m
+  have mc : y ∈ (chartAt A x).source := by simpa only [mfld_simps] using m
+  have d0 := (contMDiffOn_extChartAt_symm (n := ⊤) _ _ m').mdifferentiableWithinAt le_top
+  have d1 := (contMDiffAt_extChartAt' (I := I) (n := ⊤) mc).mdifferentiableWithinAt le_top
+  replace d0 := d0.mdifferentiableAt (extChartAt_target_mem_nhds' _ m')
+  simp only [mdifferentiableWithinAt_univ] at d1
+  have c := mfderiv_comp y d0 d1
+  refine Eq.trans c.symm ?_
+  rw [← mfderiv_id]
+  apply Filter.EventuallyEq.mfderiv_eq
+  rw [Filter.eventuallyEq_iff_exists_mem]; use(extChartAt I x).source
+  use extChartAt_source_mem_nhds' I m
+  intro z zm
+  simp only [Function.comp, id, PartialEquiv.left_inv _ zm]
+
+/-- Chart derivatives are invertible (right inverse) -/
+theorem extChartAt_mderiv_right_inverse [I.Boundaryless] {x : M} {y : E}
+    (m : y ∈ (extChartAt I x).target) :
+    (mfderiv I (modelWithCornersSelf 𝕜 E) (extChartAt I x) ((extChartAt I x).symm y)).comp
+        (mfderiv (modelWithCornersSelf 𝕜 E) I (extChartAt I x).symm y) =
+      ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) y) := by
+  have m' : (extChartAt I x).symm y ∈ (extChartAt I x).source := PartialEquiv.map_target _ m
+  have mc : (extChartAt I x).symm y ∈ (chartAt A x).source := by simpa only [mfld_simps] using m'
+  have d0 := (contMDiffOn_extChartAt_symm (n := ⊤) _ _ m).mdifferentiableWithinAt le_top
+  have d1 := (contMDiffAt_extChartAt' (I := I) (n := ⊤) mc).mdifferentiableWithinAt le_top
+  replace d0 := d0.mdifferentiableAt (extChartAt_target_mem_nhds' _ m)
+  simp only [mdifferentiableWithinAt_univ] at d1
+  have c := mfderiv_comp y d1 d0
+  refine Eq.trans c.symm ?_; clear c; rw [← mfderiv_id]; apply Filter.EventuallyEq.mfderiv_eq
+  rw [Filter.eventuallyEq_iff_exists_mem]; use(extChartAt I x).target
+  have n := extChartAt_target_mem_nhdsWithin' I m'
+  simp only [ModelWithCorners.range_eq_univ, nhdsWithin_univ,
+    PartialEquiv.right_inv _ m] at n
+  use n; intro z zm
+  simp only [Function.comp, id, PartialEquiv.right_inv _ zm, Function.comp]
+
+/-- Chart derivatives are invertible (right inverse) -/
+theorem extChartAt_mderiv_right_inverse' [I.Boundaryless] {x y : M}
+    (m : y ∈ (extChartAt I x).source) :
+    (mfderiv I (modelWithCornersSelf 𝕜 E) (extChartAt I x) y).comp
+        (mfderiv (modelWithCornersSelf 𝕜 E) I (extChartAt I x).symm (extChartAt I x y)) =
+      ContinuousLinearMap.id 𝕜 (TangentSpace (modelWithCornersSelf 𝕜 E) (extChartAt I x y)) := by
+  have h := extChartAt_mderiv_right_inverse (PartialEquiv.map_source _ m)
+  rw [PartialEquiv.left_inv _ m] at h; exact h
+
 end Deriv

Ray/Dynamics/Multiple.lean

@@ -183,7 +183,7 @@ theorem not_local_inj_of_mfderiv_zero {f : S → T} {c : S} (fa : MAnalyticAt I
     apply mem_extChartAt_source; apply mem_extChartAt_source
     exact MDifferentiableAt.comp _ fd
       (MAnalyticAt.extChartAt_symm (mem_extChartAt_target _ _)).mdifferentiableAt
-  simp only [mAnalyticAt_iff, Function.comp, hg] at fa
+  simp only [mAnalyticAt_iff_of_boundaryless, Function.comp, hg] at fa
   have dg' := fa.2.differentiableAt.mdifferentiableAt.hasMFDerivAt
   rw [dg, hasMFDerivAt_iff_hasFDerivAt] at dg'
   replace dg := dg'.hasDerivAt; clear dg'

Ray/Misc/Topology.lean

@@ -196,3 +196,20 @@ theorem Ne.eventually_ne {X : Type} [TopologicalSpace X] [T2Space X] {x y : X} (
 /-- The `⊥` filter has no cluster_pts -/
 theorem ClusterPt.bot {X : Type} [TopologicalSpace X] {x : X} : ¬ClusterPt x ⊥ := fun h ↦
   (h.neBot.mono inf_le_right).ne rfl
+
+/-- Version of `nhdsWithin_eq_iff_eventuallyEq` that doesn't misuse eventual equality -/
+lemma nhdsWithin_eq_iff_eventuallyEq' {X : Type} [TopologicalSpace X] {s t : Set X} {x : X} :
+    𝓝[s] x = 𝓝[t] x ↔ (· ∈ s) =ᶠ[𝓝 x] (· ∈ t) :=
+  nhdsWithin_eq_iff_eventuallyEq
+
+/-- `ContinuousWithinAt` depends only locally on the set -/
+lemma ContinuousWithinAt.congr_set'' {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y]
+    {f : X → Y} {s t : Set X} {x : X} (fc : ContinuousWithinAt f s x)
+    (hst : (· ∈ s) =ᶠ[𝓝 x] (· ∈ t)) : ContinuousWithinAt f t x := by
+  simpa only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq'.mpr hst] using fc
+
+/-- Turn eventual equality into an intersection into eventual equality w.r.t. `𝓝[s] x` -/
+lemma eventuallyEq_inter {X : Type} [TopologicalSpace X] {s t u : Set X} {x : X} :
+    (· ∈ t ∩ s) =ᶠ[𝓝 x] (· ∈ u ∩ s) ↔ (· ∈ t) =ᶠ[𝓝[s] x] (· ∈ u) := by
+  rw [Filter.EventuallyEq, eventuallyEq_nhdsWithin_iff]
+  simp only [mem_inter_iff, eq_iff_iff, and_congr_left_iff]