PolynomialRegularityContracts.lean

1 module
2 public import PolynomialRegularityIntegral
3 public import PolynomialAnalyticEvaluation
4 public import PolynomialAnalyticImplicit
5 public import PolynomialAnalyticSelection
6 
7 @[expose] public section
8 noncomputable section
9 set_option autoImplicit false
10 
11 namespace Komorebi.PolynomialRegularityContracts
12 
13 open MvPolynomial
14 open Filter
15 open scoped Topology
16 open Komorebi.PolynomialAnalyticEvaluation
17 
18 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
19 variable {n m e k : ℕ}
20 
21 /-- The analytic input and strict derivative are proved for actual polynomial
22 evaluation and the actual evaluated partial derivatives. -/
23 theorem actual_polynomial_evaluation (F : Fin m → MvPolynomial (Fin n) 𝕜)
24     (a : Fin n → 𝕜) :
25     AnalyticOnNhd 𝕜 (fun x i => eval x (F i)) Set.univ ∧
26       HasStrictFDerivAt (fun x i => eval x (F i))
27         (matrixCLM (fun i j => eval a (pderiv j (F i)))) a := by
28   exact ⟨analyticOnNhd_evalSystem F, hasStrictFDerivAt_evalSystem F a⟩
29 
30 /-- Only the original polynomial root and actual solved-matrix invertibility
31 are hypotheses. The conclusion constructs the analytic local root graph and
32 identifies its strict derivative by the original evaluated partial derivatives. -/
33 theorem actual_padic_analytic_root_graph (p : ℕ) [Fact p.Prime]
34     (F : Fin e → MvPolynomial (Fin (e + k)) ℚ_[p])
35     (a : Fin (e + k) → ℚ_[p]) (hF : ∀ i, eval a (F i) = 0)
36     (hJ : IsUnit (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i)))) :
37     ∃ (ψ : (Fin k → ℚ_[p]) → (Fin e → ℚ_[p])) (U : Set (Fin k → ℚ_[p]))
38       (V : Set (Fin e → ℚ_[p])),
39       IsOpen U ∧ IsOpen V ∧ (fun j => a (Fin.natAdd e j)) ∈ U ∧
40       (fun i => a (Fin.castAdd k i)) ∈ V ∧
41       ψ (fun j => a (Fin.natAdd e j)) = (fun i => a (Fin.castAdd k i)) ∧
42       AnalyticOnNhd ℚ_[p] ψ U ∧ DifferentiableOn ℚ_[p] ψ U ∧
43       (∀ t ∈ U, ψ t ∈ V) ∧
44       (∀ t ∈ U, ∀ y ∈ V, (∀ i, eval (Fin.append y t) (F i) = 0) ↔ y = ψ t) ∧
45       HasStrictFDerivAt ψ
46         (matrixCLM (-((Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i)))⁻¹ *
47           (Matrix.of fun i j => eval a (pderiv (Fin.natAdd e j) (F i))))))
48         (fun j => a (Fin.natAdd e j)) := by
49   obtain ⟨ψ, U, V, hU, hV, ht, hy, hbase, han, hinto, hgraph, hder⟩ :=
50     PolynomialAnalyticImplicit.exists_analytic_implicit F a (funext hF) hJ
51   refine ⟨ψ, U, V, hU, hV, ht, hy, hbase, han, han.differentiableOn, hinto, ?_, hder⟩
52   intro t ht y hy
53   exact (show (∀ i, eval (Fin.append y t) (F i) = 0) ↔ evalSystem F (Fin.append y t) = 0
54     from ⟨fun h => funext h, fun h i => congrFun h i⟩).trans (hgraph t ht y hy)
55 
56 /-- A supplied continuous root selection has the same analytic germ and the
57 same actual implicit derivative. No regularity conclusion is assumed. -/
58 theorem actual_selection_germ (p : ℕ) [Fact p.Prime]
59     (F : Fin e → MvPolynomial (Fin (e + k)) ℚ_[p])
60     (a : Fin (e + k) → ℚ_[p])
61     (hJ : IsUnit (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i))))
62     (g : (Fin k → ℚ_[p]) → (Fin e → ℚ_[p]))
63     (hg : ContinuousAt g (fun j => a (Fin.natAdd e j)))
64     (hg₀ : g (fun j => a (Fin.natAdd e j)) = (fun i => a (Fin.castAdd k i)))
65     (hroot : ∀ᶠ t in 𝓝 (fun j => a (Fin.natAdd e j)),
66       ∀ i, eval (Fin.append (g t) t) (F i) = 0) :
67     AnalyticAt ℚ_[p] g (fun j => a (Fin.natAdd e j)) ∧
68       HasStrictFDerivAt g
69         (matrixCLM (-((Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i)))⁻¹ *
70           (Matrix.of fun i j => eval a (pderiv (Fin.natAdd e j) (F i))))))
71         (fun j => a (Fin.natAdd e j)) := by
72   exact PolynomialAnalyticSelection.continuous_selection_regularity F a hJ g hg hg₀
73     (hroot.mono fun _ ht => funext ht)
74 
75 /-- Every continuous exact polynomial root selection with invertible actual
76 solved matrix on an open set is analytic and has the explicit derivative there. -/
77 theorem actual_selection_analytic_on_open (p : ℕ) [Fact p.Prime]
78     (F : Fin e → MvPolynomial (Fin (e + k)) ℚ_[p])
79     (g : (Fin k → ℚ_[p]) → (Fin e → ℚ_[p])) (U : Set (Fin k → ℚ_[p]))
80     (hU : IsOpen U) (hg : ContinuousOn g U)
81     (hroot : ∀ t ∈ U, ∀ i, eval (Fin.append (g t) t) (F i) = 0)
82     (hJ : ∀ t ∈ U, IsUnit (Matrix.of fun i j =>
83       eval (Fin.append (g t) t) (pderiv (Fin.castAdd k j) (F i)))) :
84     AnalyticOnNhd ℚ_[p] g U ∧
85       ∀ t ∈ U, HasStrictFDerivAt g
86         (matrixCLM (-((Matrix.of fun i j =>
87           eval (Fin.append (g t) t) (pderiv (Fin.castAdd k j) (F i)))⁻¹ *
88           (Matrix.of fun i j =>
89             eval (Fin.append (g t) t) (pderiv (Fin.natAdd e j) (F i)))))) t := by
90   exact PolynomialAnalyticSelection.continuous_selection_analyticOnNhd F g U hU hg
91     (fun t ht => funext (hroot t ht)) hJ
92 
93 /-- Integral coefficients and centers are included in the ambient p-adic field.
94 The input is the original solved Jacobian and the root graph evaluates the
95 original integral polynomials directly via the coefficient inclusion. -/
96 theorem actual_integral_analytic_root_graph (p : ℕ) [Fact p.Prime]
97     (F : Fin e → MvPolynomial (Fin (e + k)) ℤ_[p])
98     (a : Fin (e + k) → ℤ_[p]) (hF : ∀ i, eval a (F i) = 0)
99     (hJ : IsUnit ((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
100       (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i))))) :
101     ∃ (ψ : (Fin k → ℚ_[p]) → (Fin e → ℚ_[p])) (U : Set (Fin k → ℚ_[p]))
102       (V : Set (Fin e → ℚ_[p])),
103       IsOpen U ∧ IsOpen V ∧ (fun j => (a (Fin.natAdd e j) : ℚ_[p])) ∈ U ∧
104       (fun i => (a (Fin.castAdd k i) : ℚ_[p])) ∈ V ∧
105       ψ (fun j => (a (Fin.natAdd e j) : ℚ_[p])) =
106         (fun i => (a (Fin.castAdd k i) : ℚ_[p])) ∧
107       AnalyticOnNhd ℚ_[p] ψ U ∧ DifferentiableOn ℚ_[p] ψ U ∧
108       (∀ t ∈ U, ψ t ∈ V) ∧
109       (∀ t ∈ U, ∀ y ∈ V,
110         (∀ i, eval₂ (algebraMap ℤ_[p] ℚ_[p]) (Fin.append y t) (F i) = 0) ↔ y = ψ t) ∧
111       HasStrictFDerivAt ψ
112         (matrixCLM (-(((algebraMap ℤ_[p] ℚ_[p]).mapMatrix
113           (Matrix.of fun i j => eval a (pderiv (Fin.castAdd k j) (F i))))⁻¹ *
114           (Matrix.of fun i j => (eval a (pderiv (Fin.natAdd e j) (F i)) : ℚ_[p])))))
115         (fun j => (a (Fin.natAdd e j) : ℚ_[p])) := by
116   obtain ⟨ψ, U, V, hU, hV, ht, hy, hbase, han, hinto, hgraph, hder⟩ :=
117     PolynomialRegularityIntegral.exists_analytic_integral_implicit p F a hF hJ
118   exact ⟨ψ, U, V, hU, hV, ht, hy, hbase, han, han.differentiableOn, hinto, hgraph, hder⟩
119 
120 end Komorebi.PolynomialRegularityContracts

Back to source controls