PolynomialAnalyticSelection.lean

1 module
2 public import PolynomialAnalyticImplicit
3 
4 @[expose] public section
5 noncomputable section
6 set_option autoImplicit false
7 
8 namespace Komorebi.PolynomialAnalyticSelection
9 open Filter Set
10 open scoped Topology
11 open PolynomialParameterSystem PolynomialAnalyticEvaluation PolynomialAnalyticImplicit
12 
13 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
14 variable {e k : ℕ}
15 
16 /-- Continuity places a supplied local root selection inside the unique local
17 graph, so its germ agrees with the constructed solution germ. -/
18 theorem continuous_selection_eventually_eq
19     (P : (Fin (e + k) → 𝕜) → (Fin e → 𝕜))
20     (g ψ : (Fin k → 𝕜) → (Fin e → 𝕜))
21     (t₀ : Fin k → 𝕜) (y₀ : Fin e → 𝕜)
22     (U : Set (Fin k → 𝕜)) (V : Set (Fin e → 𝕜))
23     (hU : IsOpen U) (hV : IsOpen V) (ht : t₀ ∈ U) (hy : y₀ ∈ V)
24     (hgraph : ∀ t ∈ U, ∀ y ∈ V, P (join y t) = 0 ↔ y = ψ t)
25     (hg : ContinuousAt g t₀) (hg₀ : g t₀ = y₀)
26     (hroot : ∀ᶠ t in 𝓝 t₀, P (join (g t) t) = 0) :
27     g =ᶠ[𝓝 t₀] ψ := by
28   have hgV : ∀ᶠ t in 𝓝 t₀, g t ∈ V := by
29     apply hg.preimage_mem_nhds
30     exact hV.mem_nhds (hg₀ ▸ hy)
31   filter_upwards [hU.mem_nhds ht, hgV, hroot] with t ht' hgt hrt
32   exact (hgraph t ht' (g t) hgt).mp hrt
33 
34 variable [CompleteSpace 𝕜]
35 
36 /-- Every continuous local root selection through a nonsingular point has the
37 analytic implicit germ and the actual derivative -J⁻¹K. No analyticity or
38 derivative hypothesis on the supplied selection is needed. -/
39 theorem continuous_selection_regularity
40     (F : Fin e → MvPolynomial (Fin (e + k)) 𝕜)
41     (a : Fin (e + k) → 𝕜)
42     (hJ : IsUnit (PolynomialJointSystem.solvedJacobian F a))
43     (g : (Fin k → 𝕜) → (Fin e → 𝕜))
44     (hg : ContinuousAt g (freePart a)) (hg₀ : g (freePart a) = solvedPart a)
45     (hroot : ∀ᶠ t in 𝓝 (freePart a), evalSystem F (join (g t) t) = 0) :
46     AnalyticAt 𝕜 g (freePart a) ∧
47       HasStrictFDerivAt g
48         (matrixCLM (-((PolynomialJointSystem.solvedJacobian F a)⁻¹ *
49           PolynomialJointSystem.parameterJacobian F a))) (freePart a) := by
50   have hF : evalSystem F a = 0 := by
51     simpa only [hg₀, join_parts] using hroot.self_of_nhds
52   obtain ⟨ψ, U, V, hU, hV, ht, hy, _hψ₀, hψ, _hψV, hgraph, hdψ⟩ :=
53     exists_analytic_implicit F a hF hJ
54   have heq := continuous_selection_eventually_eq (evalSystem F) g ψ
55     (freePart a) (solvedPart a) U V hU hV ht hy hgraph hg hg₀ hroot
56   exact ⟨(hψ (freePart a) ht).congr heq.symm, hdψ.congr_of_eventuallyEq heq.symm⟩
57 
58 /-- On an open parameter set, any continuous exact root selection with
59 invertible solved Jacobian is analytic everywhere on that set, with its actual
60 implicit derivative at every point. -/
61 theorem continuous_selection_analyticOnNhd
62     (F : Fin e → MvPolynomial (Fin (e + k)) 𝕜)
63     (g : (Fin k → 𝕜) → (Fin e → 𝕜)) (U : Set (Fin k → 𝕜))
64     (hU : IsOpen U) (hg : ContinuousOn g U)
65     (hroot : ∀ t ∈ U, evalSystem F (join (g t) t) = 0)
66     (hJ : ∀ t ∈ U, IsUnit (PolynomialJointSystem.solvedJacobian F (join (g t) t))) :
67     AnalyticOnNhd 𝕜 g U ∧
68       ∀ t ∈ U, HasStrictFDerivAt g
69         (matrixCLM (-((PolynomialJointSystem.solvedJacobian F (join (g t) t))⁻¹ *
70           PolynomialJointSystem.parameterJacobian F (join (g t) t)))) t := by
71   have hpoint (t : Fin k → 𝕜) (ht : t ∈ U) := by
72     have hrt : ∀ᶠ u in 𝓝 t, evalSystem F (join (g u) u) = 0 := by
73       filter_upwards [hU.mem_nhds ht] with u hu using hroot u hu
74     have hgt : ContinuousAt g t := hg.continuousAt (hU.mem_nhds ht)
75     have h := continuous_selection_regularity F (join (g t) t) (hJ t ht) g
76       (by simpa only [freePart_join] using hgt)
77       (by simp only [freePart_join, solvedPart_join])
78       (by simpa only [freePart_join] using hrt)
79     exact h
80   exact ⟨fun t ht => by simpa only [freePart_join] using (hpoint t ht).1,
81     fun t ht => by simpa only [freePart_join] using (hpoint t ht).2⟩
82 
83 end Komorebi.PolynomialAnalyticSelection

Back to source controls