PolynomialAnalyticInverse.lean

1 module
2 public import Mathlib.Analysis.Calculus.FDeriv.Analytic
3 public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
4 
5 /-!
6 Analyticity of the generic local inverse over any nontrivially normed field.
7 The result applies to finite-dimensional p-adic spaces without restricting the
8 field to the real or complex numbers.
9 -/
10 
11 @[expose] public section
12 noncomputable section
13 set_option autoImplicit false
14 
15 namespace Komorebi.PolynomialAnalyticInverse
16 
17 open Filter Set
18 open scoped Topology
19 
20 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
21 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
22 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
23 variable [CompleteSpace E]
24 variable {f : E → F} {a : E} {i : E ≃L[𝕜] F}
25 
26 /-- An analytic function with an invertible strict derivative has an analytic
27 local inverse. The only completeness hypothesis is on the original domain. -/
28 theorem analyticAt_inverse (ha : AnalyticAt 𝕜 f a)
29     (hd : HasStrictFDerivAt f (i : E →L[𝕜] F) a) :
30     AnalyticAt 𝕜 (hd.localInverse f i a) (f a) := by
31   exact (hd.toOpenPartialHomeomorph f).analyticAt_symm'
32     hd.mem_toOpenPartialHomeomorph_source ha hd.hasFDerivAt.fderiv
33 
34 /-- The same inverse is analytic throughout some open neighborhood of the
35 image point, where its right inverse identity holds exactly. -/
36 theorem exists_open_analytic_inverse (ha : AnalyticAt 𝕜 f a)
37     (hd : HasStrictFDerivAt f (i : E →L[𝕜] F) a) :
38     ∃ U : Set F, IsOpen U ∧ f a ∈ U ∧
39       AnalyticOnNhd 𝕜 (hd.localInverse f i a) U ∧
40       ∀ y ∈ U, f (hd.localInverse f i a y) = y := by
41   let R := hd.toOpenPartialHomeomorph f
42   let U := {y | AnalyticAt 𝕜 (hd.localInverse f i a) y} ∩ R.target
43   refine ⟨U, (isOpen_analyticAt 𝕜 _).inter R.open_target, ?_, ?_, ?_⟩
44   · exact ⟨analyticAt_inverse ha hd, hd.image_mem_toOpenPartialHomeomorph_target⟩
45   · intro y hy
46     exact hy.1
47   · intro y hy
48     exact R.right_inv hy.2
49 
50 end Komorebi.PolynomialAnalyticInverse

Back to source controls