PolynomialAnalyticEvaluation.lean

1 module
2 public import PolynomialWeightedInverse
3 public import Mathlib.Analysis.Analytic.Polynomial
4 public import Mathlib.Analysis.Analytic.Constructions
5 public import Mathlib.Analysis.Calculus.FDeriv.Mul
6 public import Mathlib.Analysis.Calculus.FDeriv.Prod
7 public import Mathlib.Analysis.Normed.Module.FiniteDimension
8 
9 @[expose] public section
10 noncomputable section
11 set_option autoImplicit false
12 
13 namespace Komorebi.PolynomialAnalyticEvaluation
14 open Matrix
15 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
16 variable {n m : ℕ}
17 
18 /-- The continuous linear map represented by a finite matrix. -/
19 def matrixCLM (A : Matrix (Fin m) (Fin n) 𝕜) :
20     (Fin n → 𝕜) →L[𝕜] (Fin m → 𝕜) := A.mulVecLin.toContinuousLinearMap
21 
22 @[simp] theorem matrixCLM_apply (A : Matrix (Fin m) (Fin n) 𝕜) (v : Fin n → 𝕜) :
23     matrixCLM A v = A.mulVec v := rfl
24 
25 /-- Actual evaluation of each polynomial in a system. -/
26 def evalSystem (F : Fin m → MvPolynomial (Fin n) 𝕜) (a : Fin n → 𝕜) : Fin m → 𝕜 :=
27   fun i => MvPolynomial.eval a (F i)
28 
29 /-- The formal partial derivatives give a continuous linear functional. -/
30 def polynomialDeriv (P : MvPolynomial (Fin n) 𝕜) (a : Fin n → 𝕜) :
31     (Fin n → 𝕜) →L[𝕜] 𝕜 :=
32   ∑ j, MvPolynomial.eval a (MvPolynomial.pderiv j P) • ContinuousLinearMap.proj j
33 
34 omit [CompleteSpace 𝕜] in
35 @[simp] theorem polynomialDeriv_apply (P : MvPolynomial (Fin n) 𝕜)
36     (a v : Fin n → 𝕜) :
37     polynomialDeriv P a v = ∑ j, MvPolynomial.eval a (MvPolynomial.pderiv j P) * v j := by
38   simp [polynomialDeriv]
39 
40 omit [CompleteSpace 𝕜] in
41 /-- Polynomial evaluation has strict derivative equal to its actual formal gradient. -/
42 theorem hasStrictFDerivAt_eval (P : MvPolynomial (Fin n) 𝕜) (a : Fin n → 𝕜) :
43     HasStrictFDerivAt (fun x => MvPolynomial.eval x P) (polynomialDeriv P a) a := by
44   induction P using MvPolynomial.induction_on with
45   | C c =>
46       have hder : polynomialDeriv (MvPolynomial.C c) a = 0 := by
47         ext v
48         simp
49       rw [hder]
50       convert! (hasStrictFDerivAt_const (𝕜 := 𝕜) c a) using 1; ext x; simp
51   | add P Q hP hQ =>
52       have hder : polynomialDeriv (P + Q) a = polynomialDeriv P a + polynomialDeriv Q a := by
53         ext v
54         simp [Finset.sum_add_distrib, add_mul]
55       rw [hder]
56       convert! hP.add hQ using 1; ext x; simp
57   | mul_X P j hP =>
58       have hder : polynomialDeriv (P * MvPolynomial.X j) a =
59           MvPolynomial.eval a P • ContinuousLinearMap.proj j + a j • polynomialDeriv P a := by
60         ext v
61         simp [MvPolynomial.pderiv_X, Pi.single_apply, apply_ite, Finset.sum_add_distrib,
62           mul_add, Finset.mul_sum, mul_left_comm, mul_comm]
63       rw [hder]
64       convert! hP.mul (hasStrictFDerivAt_apply j a) using 1; ext x; simp
65 
66 /-- Actual finite polynomial systems are analytic at every point. -/
67 theorem analyticAt_evalSystem (F : Fin m → MvPolynomial (Fin n) 𝕜) (a : Fin n → 𝕜) :
68     AnalyticAt 𝕜 (evalSystem F) a := by
69   exact AnalyticAt.pi fun i => AnalyticOnNhd.eval_mvPolynomial (F i) a (Set.mem_univ a)
70 
71 /-- Actual finite polynomial systems are analytic on the whole ambient space. -/
72 theorem analyticOnNhd_evalSystem (F : Fin m → MvPolynomial (Fin n) 𝕜) :
73     AnalyticOnNhd 𝕜 (evalSystem F) Set.univ := fun a _ => analyticAt_evalSystem F a
74 
75 /-- The derivative matrix is exactly the evaluated formal Jacobian, with no derivative hypothesis. -/
76 theorem hasStrictFDerivAt_evalSystem (F : Fin m → MvPolynomial (Fin n) 𝕜)
77     (a : Fin n → 𝕜) :
78     HasStrictFDerivAt (evalSystem F) (matrixCLM (PolynomialWeightedInverse.jacobian F a)) a := by
79   have h := hasStrictFDerivAt_pi.mpr (fun i => hasStrictFDerivAt_eval (F i) a)
80   have hder : ContinuousLinearMap.pi (fun i => polynomialDeriv (F i) a) =
81       matrixCLM (PolynomialWeightedInverse.jacobian F a) := by
82     ext v i
83     simp [PolynomialWeightedInverse.jacobian, Matrix.mulVec, dotProduct]
84   rw [← hder]
85   convert! h using 1
86 
87 end Komorebi.PolynomialAnalyticEvaluation

Back to source controls