PolynomialRegularityControls.lean

1 module
2 public import PolynomialJointSystem
3 public import PolynomialAnalyticInverse
4 public import PolynomialAnalyticImplicit
5 
6 @[expose] public section
7 noncomputable section
8 set_option autoImplicit false
9 
10 namespace Komorebi.PolynomialRegularityControls
11 
12 open MvPolynomial Matrix
13 open Komorebi.PolynomialParameterSystem
14 
15 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
16 
17 /-- A genuine mixed solved/parameter equation, with nonzero parameter derivative. -/
18 def linearSystem : Fin 1 → MvPolynomial (Fin (1 + 1)) 𝕜 :=
19   fun _ => X (Fin.castAdd 1 0) + X (Fin.natAdd 1 0)
20 
21 theorem linear_solvedJacobian (a : Fin (1 + 1) → 𝕜) :
22     Komorebi.PolynomialJointSystem.solvedJacobian linearSystem a = 1 := by
23   ext i j
24   have hi : i = 0 := Fin.eq_zero i
25   have hj : j = 0 := Fin.eq_zero j
26   subst i
27   subst j
28   simp [Komorebi.PolynomialJointSystem.solvedJacobian, linearSystem, pderiv_X]
29 
30 theorem linear_parameterJacobian (a : Fin (1 + 1) → 𝕜) :
31     Komorebi.PolynomialJointSystem.parameterJacobian linearSystem a = 1 := by
32   ext i j
33   have hi : i = 0 := Fin.eq_zero i
34   have hj : j = 0 := Fin.eq_zero j
35   subst i
36   subst j
37   simp [Komorebi.PolynomialJointSystem.parameterJacobian, linearSystem, pderiv_X]
38 
39 /-- The explicit global branch is analytic at every parameter, including p = 2. -/
40 theorem linear_analytic (t : Fin 1 → 𝕜) :
41     AnalyticAt 𝕜 (fun u : Fin 1 → 𝕜 => -u) t := by
42   exact analyticAt_id.neg
43 
44 /-- The actual root equation forces precisely the explicit branch. -/
45 theorem linear_root_graph (y t : Fin 1 → 𝕜) :
46     (∀ i, eval (join y t) (linearSystem i) = 0) ↔ y = -t := by
47   constructor
48   · intro h
49     ext i
50     have hi : i = 0 := Fin.eq_zero i
51     subst i
52     have h0 := h 0
53     simp only [linearSystem, map_add, eval_X, join_solved, join_free] at h0
54     exact eq_neg_of_add_eq_zero_left h0
55   · intro h i
56     subst y
57     simp only [linearSystem, map_add, eval_X, join_solved, join_free, Pi.neg_apply,
58       neg_add_cancel]
59 
60 /-- The sign in the implicit derivative is negative. -/
61 theorem linear_strict_derivative (t : Fin 1 → 𝕜) :
62     HasStrictFDerivAt (fun u : Fin 1 → 𝕜 => -u)
63       (-ContinuousLinearMap.id 𝕜 (Fin 1 → 𝕜)) t := by
64   exact (hasStrictFDerivAt_id t).neg
65 
66 /-- In characteristic zero, the positive derivative is incompatible with this root graph. -/
67 theorem linear_derivative_not_positive [CharZero 𝕜] (t : Fin 1 → 𝕜) :
68     ¬ HasStrictFDerivAt (fun u : Fin 1 → 𝕜 => -u)
69       (ContinuousLinearMap.id 𝕜 (Fin 1 → 𝕜)) t := by
70   intro h
71   have hd := h.hasFDerivAt.unique (linear_strict_derivative t).hasFDerivAt
72   have h1 := congrArg (fun L : (Fin 1 → 𝕜) →L[𝕜] (Fin 1 → 𝕜) => L (fun _ => 1) 0) hd
73   norm_num at h1
74 
75 /-- A nonlinear equation whose local branch is selected by the actual implicit theorem. -/
76 def quadraticSystem : Fin 1 → MvPolynomial (Fin (1 + 1)) 𝕜 :=
77   fun _ => X (Fin.castAdd 1 0) + X (Fin.castAdd 1 0) ^ 2 + X (Fin.natAdd 1 0)
78 
79 theorem quadratic_root :
80     ∀ i, eval (0 : Fin (1 + 1) → 𝕜) (quadraticSystem i) = 0 := by
81   intro i
82   simp [quadraticSystem]
83 
84 theorem quadratic_solvedJacobian :
85     Komorebi.PolynomialJointSystem.solvedJacobian quadraticSystem
86       (0 : Fin (1 + 1) → 𝕜) = 1 := by
87   ext i j
88   have hi : i = 0 := Fin.eq_zero i
89   have hj : j = 0 := Fin.eq_zero j
90   subst i
91   subst j
92   simp [Komorebi.PolynomialJointSystem.solvedJacobian, quadraticSystem, pderiv_X]
93 
94 theorem quadratic_parameterJacobian :
95     Komorebi.PolynomialJointSystem.parameterJacobian quadraticSystem
96       (0 : Fin (1 + 1) → 𝕜) = 1 := by
97   ext i j
98   have hi : i = 0 := Fin.eq_zero i
99   have hj : j = 0 := Fin.eq_zero j
100   subst i
101   subst j
102   simp [Komorebi.PolynomialJointSystem.parameterJacobian, quadraticSystem, pderiv_X]
103 
104 /-- A nonlinear invocation of the complete polynomial theorem, with the correct negative slope.
105 This control remains valid over every complete nontrivially normed field, including Q₂. -/
106 theorem quadratic_analytic_branch [CompleteSpace 𝕜] :
107     ∃ (ψ : (Fin 1 → 𝕜) → (Fin 1 → 𝕜)) (U V : Set (Fin 1 → 𝕜)),
108       IsOpen U ∧ IsOpen V ∧ (0 : Fin 1 → 𝕜) ∈ U ∧ (0 : Fin 1 → 𝕜) ∈ V ∧
109       ψ 0 = 0 ∧ AnalyticOnNhd 𝕜 ψ U ∧ (∀ t ∈ U, ψ t ∈ V) ∧
110       (∀ t ∈ U, ∀ y ∈ V,
111         (∀ i, eval (join y t) (quadraticSystem i) = 0) ↔ y = ψ t) ∧
112       HasStrictFDerivAt ψ (-ContinuousLinearMap.id 𝕜 (Fin 1 → 𝕜)) 0 := by
113   have hroot : Komorebi.PolynomialAnalyticEvaluation.evalSystem quadraticSystem
114       (0 : Fin (1 + 1) → 𝕜) = 0 := by
115     ext i
116     exact quadratic_root i
117   have hunit : IsUnit (Komorebi.PolynomialJointSystem.solvedJacobian quadraticSystem
118       (0 : Fin (1 + 1) → 𝕜)) := by
119     rw [quadratic_solvedJacobian]
120     exact isUnit_one
121   obtain ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, hgraph, hder⟩ :=
122     Komorebi.PolynomialAnalyticImplicit.exists_analytic_implicit quadraticSystem
123       (0 : Fin (1 + 1) → 𝕜) hroot hunit
124   refine ⟨ψ, U, V, hU, hV, ht, hy, hψa, hψan, hψV, ?_, ?_⟩
125   · intro t ht' y hy'
126     simpa only [Komorebi.PolynomialAnalyticEvaluation.evalSystem,
127       funext_iff, Pi.zero_apply] using hgraph t ht' y hy'
128   · have heq : Komorebi.PolynomialAnalyticEvaluation.matrixCLM
129         (-(1 : Matrix (Fin 1) (Fin 1) 𝕜)) =
130         -ContinuousLinearMap.id 𝕜 (Fin 1 → 𝕜) := by
131       ext v i
132       simp [Matrix.neg_mulVec]
133     have hz : freePart (0 : Fin (1 + 1) → 𝕜) = (0 : Fin 1 → 𝕜) := rfl
134     rw [hz] at hder
135     simpa only [quadratic_solvedJacobian, quadratic_parameterJacobian,
136       inv_one, one_mul, heq] using hder
137 
138 end Komorebi.PolynomialRegularityControls

Back to source controls