PolynomialAnalyticBlocks.lean

1 module
2 public import PolynomialAnalyticEvaluation
3 public import PolynomialBlockInverse
4 
5 @[expose] public section
6 noncomputable section
7 set_option autoImplicit false
8 
9 namespace Komorebi.PolynomialAnalyticBlocks
10 open Matrix
11 open Komorebi.PolynomialParameterSystem
12 open Komorebi.PolynomialBlockInverse
13 open Komorebi.PolynomialAnalyticEvaluation
14 
15 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
16 variable {e k : ℕ}
17 
18 /-- The actual augmented derivative is a continuous linear equivalence whenever
19 its solved block is invertible. Its inverse is the explicit triangular block matrix. -/
20 def upperEquiv (J : Matrix (Fin e) (Fin e) 𝕜)
21     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) :
22     (Fin (e+k) → 𝕜) ≃L[𝕜] (Fin (e+k) → 𝕜) := by
23   let B := upperBlock J K (1 : 𝕜)
24   let C := blockCertificate J⁻¹ K (1 : 𝕜)
25   have hdet := (Matrix.isUnit_iff_isUnit_det J).mp hJ
26   have hCB : C * B = 1 := by
27     simpa only [one_smul] using blockCertificate_mul J⁻¹ J K (1 : 𝕜)
28       (by simpa only [one_smul] using Matrix.nonsing_inv_mul J hdet)
29   have hBC : B * C = 1 := by
30     simpa only [one_smul] using mul_blockCertificate J⁻¹ J K (1 : 𝕜)
31       (by simpa only [one_smul] using Matrix.mul_nonsing_inv J hdet)
32   refine (LinearEquiv.ofLinearMap B.mulVecLin C.mulVecLin ?_ ?_).toContinuousLinearEquiv
33   · apply LinearMap.ext
34     intro v
35     change B.mulVec (C.mulVec v) = v
36     rw [Matrix.mulVec_mulVec, hBC, Matrix.one_mulVec]
37   · apply LinearMap.ext
38     intro v
39     change C.mulVec (B.mulVec v) = v
40     rw [Matrix.mulVec_mulVec, hCB, Matrix.one_mulVec]
41 
42 @[simp] theorem upperEquiv_apply (J : Matrix (Fin e) (Fin e) 𝕜)
43     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) (v : Fin (e+k) → 𝕜) :
44     upperEquiv J K hJ v = (upperBlock J K 1).mulVec v := rfl
45 
46 @[simp] theorem upperEquiv_symm_apply (J : Matrix (Fin e) (Fin e) 𝕜)
47     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) (v : Fin (e+k) → 𝕜) :
48     (upperEquiv J K hJ).symm v = (blockCertificate J⁻¹ K 1).mulVec v := rfl
49 
50 /-- The continuous derivative equivalence is the actual matrix action. -/
51 theorem upperEquiv_toCLM (J : Matrix (Fin e) (Fin e) 𝕜)
52     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) :
53     (upperEquiv J K hJ : (Fin (e+k) → 𝕜) →L[𝕜] (Fin (e+k) → 𝕜)) =
54       matrixCLM (upperBlock J K 1) := by
55   ext v i
56   rfl
57 
58 /-- Restricting the inverse derivative to parameter targets gives exactly -J⁻¹K. -/
59 theorem inverse_solved_zero (J : Matrix (Fin e) (Fin e) 𝕜)
60     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) (v : Fin k → 𝕜) :
61     solvedPart ((upperEquiv J K hJ).symm (join (0 : Fin e → 𝕜) v)) =
62       matrixCLM (-(J⁻¹ * K)) v := by
63   rw [upperEquiv_symm_apply]
64   simp only [blockCertificate, upperBlock_mulVec_join, Matrix.mulVec_zero,
65     zero_add, solvedPart_join]
66   rfl
67 
68 /-- The inverse derivative preserves the prescribed parameter increment exactly. -/
69 theorem inverse_free_zero (J : Matrix (Fin e) (Fin e) 𝕜)
70     (K : Matrix (Fin e) (Fin k) 𝕜) (hJ : IsUnit J) (v : Fin k → 𝕜) :
71     freePart ((upperEquiv J K hJ).symm (join (0 : Fin e → 𝕜) v)) = v := by
72   rw [upperEquiv_symm_apply]
73   simp only [blockCertificate, upperBlock_mulVec_join, freePart_join, one_smul]
74 
75 end Komorebi.PolynomialAnalyticBlocks

Back to source controls