PolynomialAnalyticImplicit.lean

1 module
2 public import PolynomialAnalyticInverse
3 public import PolynomialJointSystem
4 public import PolynomialAnalyticBlocks
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialAnalyticImplicit
11 open Filter Set
12 open scoped Topology
13 open Komorebi.PolynomialParameterSystem
14 open Komorebi.PolynomialAnalyticInverse
15 
16 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
17 variable {e k : ℕ}
18 
19 /-- The solved-coordinate projection as a continuous linear map. -/
20 def solvedPartCLM : (Fin (e + k) → 𝕜) →L[𝕜] (Fin e → 𝕜) :=
21   ContinuousLinearMap.pi fun i => ContinuousLinearMap.proj (Fin.castAdd k i)
22 
23 @[simp] theorem solvedPartCLM_apply (z : Fin (e + k) → 𝕜) :
24     solvedPartCLM z = solvedPart z := rfl
25 
26 /-- Insert a parameter displacement and zero solved-coordinate displacement. -/
27 def parameterInjectionCLM : (Fin k → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜) :=
28   ContinuousLinearMap.pi fun i => Fin.addCases (fun _ => 0)
29     (fun j => ContinuousLinearMap.proj j) i
30 
31 @[simp] theorem parameterInjectionCLM_apply (v : Fin k → 𝕜) :
32     parameterInjectionCLM (e := e) v = join 0 v := by
33   ext i
34   refine Fin.addCases (fun j => ?_) (fun j => ?_) i <;>
35     simp [parameterInjectionCLM]
36 
37 variable [CompleteSpace 𝕜]
38 
39 /-- An analytic inverse of an augmented map supplies an exact open local graph.
40 This helper retains the inverse derivative explicitly for the polynomial specialization. -/
41 theorem exists_analytic_graph
42     (P : (Fin (e + k) → 𝕜) → (Fin e → 𝕜))
43     (a : Fin (e + k) → 𝕜) (hP : P a = 0)
44     (A : (Fin (e + k) → 𝕜) ≃L[𝕜] (Fin (e + k) → 𝕜))
45     (ha : AnalyticAt 𝕜 (fun z => join (P z) (freePart z)) a)
46     (hd : HasStrictFDerivAt (fun z => join (P z) (freePart z))
47       (A : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)) a) :
48     ∃ (ψ : (Fin k → 𝕜) → (Fin e → 𝕜)) (U : Set (Fin k → 𝕜))
49       (V : Set (Fin e → 𝕜)),
50       IsOpen U ∧ IsOpen V ∧ freePart a ∈ U ∧ solvedPart a ∈ V ∧
51       ψ (freePart a) = solvedPart a ∧ AnalyticOnNhd 𝕜 ψ U ∧
52       (∀ t ∈ U, ψ t ∈ V) ∧
53       (∀ t ∈ U, ∀ y ∈ V, P (join y t) = 0 ↔ y = ψ t) ∧
54       HasStrictFDerivAt ψ
55         ((solvedPartCLM (e := e) (k := k)).comp
56         ((A.symm : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)).comp
57           (parameterInjectionCLM (e := e) (k := k))))
58         (freePart a) := by
59   let f := fun z => join (P z) (freePart z)
60   let g := hd.localInverse f A a
61   let ψ := fun t => solvedPart (g (join 0 t))
62   have hfa : f a = join 0 (freePart a) := by simp [f, hP]
63   have hga : g (join 0 (freePart a)) = a := by
64     rw [← hfa]
65     exact hd.localInverse_apply_image
66   have hψa : ψ (freePart a) = solvedPart a := by simp [ψ, hga]
67   have hag : AnalyticAt 𝕜 g (join 0 (freePart a)) := by
68     rw [← hfa]
69     exact analyticAt_inverse ha hd
70   have hag' : AnalyticAt 𝕜 g
71       (parameterInjectionCLM (e := e) (k := k) (freePart a)) := by
72     simpa only [parameterInjectionCLM_apply] using hag
73   have haψ : AnalyticAt 𝕜 ψ (freePart a) := by
74     have hi := (parameterInjectionCLM (𝕜 := 𝕜) (e := e) (k := k)).analyticAt
75       (freePart a)
76     have hg := hag'.comp hi
77     have h := ((solvedPartCLM (𝕜 := 𝕜) (e := e) (k := k)).analyticAt _).comp hg
78     simpa only [Function.comp_def, solvedPartCLM_apply, parameterInjectionCLM_apply] using h
79   have hdg : HasStrictFDerivAt g (A.symm : _ →L[𝕜] _)
80       (parameterInjectionCLM (e := e) (k := k) (freePart a)) := by
81     simpa only [parameterInjectionCLM_apply, ← hfa] using hd.to_localInverse
82   have hdψ : HasStrictFDerivAt ψ
83       ((solvedPartCLM (e := e) (k := k)).comp
84         ((A.symm : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)).comp
85           (parameterInjectionCLM (e := e) (k := k))))
86       (freePart a) := by
87     have hi := (parameterInjectionCLM (𝕜 := 𝕜) (e := e) (k := k)).hasStrictFDerivAt
88       (x := freePart a)
89     have hg := hdg.comp (freePart a) hi
90     have h := (solvedPartCLM (𝕜 := 𝕜) (e := e) (k := k)).hasStrictFDerivAt.comp
91       (freePart a) hg
92     simpa only [Function.comp_def, solvedPartCLM_apply, parameterInjectionCLM_apply] using h
93   let R := hd.toOpenPartialHomeomorph f
94   have hopen : IsOpen {yt : (Fin e → 𝕜) × (Fin k → 𝕜) |
95       join yt.1 yt.2 ∈ R.source} := R.open_source.preimage continuous_join
96   have hbase : (solvedPart a, freePart a) ∈
97       {yt : (Fin e → 𝕜) × (Fin k → 𝕜) | join yt.1 yt.2 ∈ R.source} := by
98     simpa using hd.mem_toOpenPartialHomeomorph_source
99   obtain ⟨V, U₀, hV, hU₀, hy₀, ht₀, hrect⟩ :=
100     isOpen_prod_iff.mp hopen (solvedPart a) (freePart a) hbase
101   obtain ⟨W, hW, haW, hanalyticW, hrightW⟩ := exists_open_analytic_inverse ha hd
102   let U := U₀ ∩ (parameterInjectionCLM (𝕜 := 𝕜) (e := e) ⁻¹' W) ∩
103     {t | AnalyticAt 𝕜 ψ t} ∩ interior (ψ ⁻¹' V)
104   have hU : IsOpen U := ((hU₀.inter
105     (hW.preimage parameterInjectionCLM.continuous)).inter
106     (isOpen_analyticAt 𝕜 ψ)).inter isOpen_interior
107   have htU : freePart a ∈ U := by
108     refine ⟨⟨⟨ht₀, ?_⟩, haψ⟩, ?_⟩
109     · simpa only [Set.mem_preimage, parameterInjectionCLM_apply, hP] using haW
110     · rw [mem_interior_iff_mem_nhds]
111       exact haψ.continuousAt.preimage_mem_nhds (hV.mem_nhds (hψa ▸ hy₀))
112   refine ⟨ψ, U, V, hU, hV, htU, hy₀, hψa, ?_, ?_, ?_, hdψ⟩
113   · intro t ht
114     exact ht.1.2
115   · intro t ht
116     exact (interior_subset (s := ψ ⁻¹' V)) ht.2
117   · intro t ht y hy
118     constructor
119     · intro hroot
120       have hz : join y t ∈ R.source := hrect (show (y, t) ∈ V ×ˢ U₀ from ⟨hy, ht.1.1.1⟩)
121       have hfz : f (join y t) = join 0 t := by simp [f, hroot]
122       have hg : g (join 0 t) = join y t := by
123         rw [← hfz]
124         exact R.left_inv hz
125       simp [ψ, hg]
126     · intro hsol
127       subst y
128       have hr : f (g (join 0 t)) = join 0 t := by
129         exact hrightW (join 0 t) (by
130           simpa only [Set.mem_preimage, parameterInjectionCLM_apply] using ht.1.1.2)
131       have hparam : freePart (g (join 0 t)) = t := by
132         have := congrArg (freePart (e := e) (q := k)) hr
133         simpa [f] using this
134       have hroot : P (g (join 0 t)) = 0 := by
135         have := congrArg (solvedPart (e := e) (q := k)) hr
136         simpa [f] using this
137       have hz : join (ψ t) t = g (join 0 t) := by
138         change join (solvedPart (g (join 0 t))) t = g (join 0 t)
139         calc
140           _ = join (solvedPart (g (join 0 t))) (freePart (g (join 0 t))) :=
141             congrArg (join (solvedPart (g (join 0 t)))) hparam.symm
142           _ = _ := join_parts _
143       rw [hz]
144       exact hroot
145 
146 open Komorebi.PolynomialAnalyticEvaluation
147 open Komorebi.PolynomialAnalyticBlocks
148 
149 /-- The actual polynomial implicit function theorem: open local graph, analyticity,
150 and the strict derivative obtained from the actual solved and parameter Jacobians. -/
151 theorem exists_analytic_implicit
152     (F : Fin e → MvPolynomial (Fin (e + k)) 𝕜)
153     (a : Fin (e + k) → 𝕜) (hF : evalSystem F a = 0)
154     (hJ : IsUnit (Komorebi.PolynomialJointSystem.solvedJacobian F a)) :
155     ∃ (ψ : (Fin k → 𝕜) → (Fin e → 𝕜)) (U : Set (Fin k → 𝕜))
156       (V : Set (Fin e → 𝕜)),
157       IsOpen U ∧ IsOpen V ∧ freePart a ∈ U ∧ solvedPart a ∈ V ∧
158       ψ (freePart a) = solvedPart a ∧ AnalyticOnNhd 𝕜 ψ U ∧
159       (∀ t ∈ U, ψ t ∈ V) ∧
160       (∀ t ∈ U, ∀ y ∈ V, evalSystem F (join y t) = 0 ↔ y = ψ t) ∧
161       HasStrictFDerivAt ψ
162         (matrixCLM (-((Komorebi.PolynomialJointSystem.solvedJacobian F a)⁻¹ *
163           Komorebi.PolynomialJointSystem.parameterJacobian F a))) (freePart a) := by
164   let J := Komorebi.PolynomialJointSystem.solvedJacobian F a
165   let K := Komorebi.PolynomialJointSystem.parameterJacobian F a
166   let A := upperEquiv J K hJ
167   have hshape : evalSystem (Komorebi.PolynomialJointSystem.augmented F 0) =
168       fun z => join (evalSystem F z) (freePart z) := by
169     funext z
170     change (fun i => MvPolynomial.eval z
171       (Komorebi.PolynomialJointSystem.augmented F 0 i)) =
172         join (fun i => MvPolynomial.eval z (F i)) (freePart z)
173     simpa only [sub_zero] using
174       Komorebi.PolynomialJointSystem.eval_augmented F (0 : Fin k → 𝕜) z
175   have ha := analyticAt_evalSystem (Komorebi.PolynomialJointSystem.augmented F 0) a
176   have hd : HasStrictFDerivAt
177       (evalSystem (Komorebi.PolynomialJointSystem.augmented F 0))
178       (A : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)) a := by
179     rw [show (A : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)) =
180       matrixCLM (Komorebi.PolynomialBlockInverse.upperBlock J K 1) from
181       upperEquiv_toCLM J K hJ]
182     simpa only [Komorebi.PolynomialJointSystem.jacobian_augmented] using
183       hasStrictFDerivAt_evalSystem (Komorebi.PolynomialJointSystem.augmented F 0) a
184   rw [hshape] at ha hd
185   obtain ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, hgraph, hder⟩ :=
186     exists_analytic_graph (evalSystem F) a hF A ha hd
187   refine ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, hgraph, ?_⟩
188   have heq : (solvedPartCLM (𝕜 := 𝕜) (e := e) (k := k)).comp
189       ((A.symm : (Fin (e + k) → 𝕜) →L[𝕜] (Fin (e + k) → 𝕜)).comp
190         (parameterInjectionCLM (e := e) (k := k))) = matrixCLM (-(J⁻¹ * K)) := by
191     apply ContinuousLinearMap.ext
192     intro v
193     simp only [ContinuousLinearMap.comp_apply, solvedPartCLM_apply,
194       parameterInjectionCLM_apply]
195     exact inverse_solved_zero J K hJ v
196   simpa only [heq] using hder
197 
198 omit [CompleteSpace 𝕜] in
199 /-- Analyticity supplied by the local graph theorem includes differentiability
200 at every parameter in its open domain. -/
201 theorem differentiableOn_of_analytic_graph
202     {ψ : (Fin k → 𝕜) → (Fin e → 𝕜)} {U : Set (Fin k → 𝕜)}
203     (hψ : AnalyticOnNhd 𝕜 ψ U) : DifferentiableOn 𝕜 ψ U :=
204   hψ.differentiableOn
205 
206 end Komorebi.PolynomialAnalyticImplicit

Back to source controls