CanonicalConnection.lean

1 module
2 public import Mathlib.Analysis.Calculus.Deriv.Mul
3 public import Mathlib.Analysis.Calculus.Deriv.Star
4 public import Mathlib.Analysis.Calculus.Deriv.Add
5 public import Mathlib.Algebra.Star.BigOperators
6 public import Mathlib.Tactic.NoncommRing
7 public import Mathlib.Tactic.NormNum
8 /-! Author: Komorebi P. Paper VII second block, Theorem 6.3.
9 The differential identities are derived from actual derivatives. -/
10 public section
11 set_option autoImplicit false
12 namespace KomorebiPaperVII.Connection
13 open scoped BigOperators
14 section Algebra
15 variable {R I : Type*} [Ring R] [Fintype I] [DecidableEq I]
16 def canonical (P D : I → R) : R := ∑ a, D a * P a
17 
18 theorem canonical_right (P D : I → R)
19     (hmul : ∀ a b, P a * P b = if a = b then P a else 0) (b : I) :
20     canonical P D * P b = D b * P b := by
21   simp [canonical, Finset.sum_mul, mul_assoc, hmul, mul_ite]
22 
23 theorem canonical_left_relation (P D : I → R)
24     (hmul : ∀ a b, P a * P b = if a = b then P a else 0)
25     (hsum : ∑ a, P a = 1)
26     (hjet : ∀ a b, D a * P b + P a * D b = if a = b then D a else 0)
27     (b : I) : D b + P b * canonical P D = D b * P b := by
28   have term (a : I) : D b * P a + P b * (D a * P a) =
29       if b = a then D b * P b else 0 := by
30     calc
31       _ = (D b * P a + P b * D a) * P a := by
32         simp only [add_mul, mul_assoc, hmul a a, ite_true]
33       _ = _ := by rw [hjet]; split_ifs with h <;> simp_all
34   calc
35     _ = ∑ a, (D b * P a + P b * (D a * P a)) := by
36       simp only [Finset.sum_add_distrib, ← Finset.mul_sum, hsum, mul_one, canonical]
37     _ = D b * P b := by simp_rw [term]; simp
38 
39 theorem canonical_commutator (P D : I → R)
40     (hmul : ∀ a b, P a * P b = if a = b then P a else 0)
41     (hsum : ∑ a, P a = 1)
42     (hjet : ∀ a b, D a * P b + P a * D b = if a = b then D a else 0)
43     (b : I) : canonical P D * P b - P b * canonical P D = D b := by
44   rw [canonical_right P D hmul, ← canonical_left_relation P D hmul hsum hjet b]
45   abel
46 
47 omit [DecidableEq I] in
48 theorem canonical_skewAdjoint [StarRing R] (P D : I → R)
49     (hstarP : ∀ a, star (P a) = P a) (hstarD : ∀ a, star (D a) = D a)
50     (hsumD : ∑ a, D a = 0)
51     (hdiag : ∀ a, D a * P a + P a * D a = D a) :
52     star (canonical P D) = -canonical P D := by
53   have h : canonical P D + star (canonical P D) = 0 := by
54     simp only [canonical, star_sum, star_mul, hstarP, hstarD,
55       ← Finset.sum_add_distrib, hdiag, hsumD]
56   exact (add_eq_zero_iff_eq_neg).mp (by simpa only [add_comm] using h)
57 
58 omit [DecidableEq I] in
59 theorem canonical_half_commutator [Algebra ℝ R] (P D : I → R)
60     (hsumD : ∑ a, D a = 0)
61     (hdiag : ∀ a, D a * P a + P a * D a = D a) :
62     (1 / 2 : ℝ) • (∑ a, (D a * P a - P a * D a)) = canonical P D := by
63   have h : (∑ a, D a * P a) + (∑ a, P a * D a) = 0 := by
64     simp only [← Finset.sum_add_distrib, hdiag, hsumD]
65   have hneg : (∑ a, P a * D a) = -(∑ a, D a * P a) :=
66     (add_eq_zero_iff_eq_neg).mp (by simpa only [add_comm] using h)
67   rw [Finset.sum_sub_distrib, hneg, sub_neg_eq_add, ← two_smul ℝ, smul_smul]
68   norm_num [canonical]
69 end Algebra
70 
71 section Derivatives
72 variable {R I : Type*} [NormedRing R] [NormedAlgebra ℝ R]
73 variable [StarRing R] [StarModule ℝ R] [ContinuousStar R]
74 variable [Fintype I] [DecidableEq I]
75 variable (P : I → ℝ → R) (D : I → R) (t : ℝ)
76 
77 omit [StarRing R] [StarModule ℝ R] [ContinuousStar R] [Fintype I] in
78 theorem differentiated_orthogonality
79     (hd : ∀ a, HasDerivAt (P a) (D a) t)
80     (hmul : ∀ s a b, P a s * P b s = if a = b then P a s else 0)
81     (a b : I) : D a * P b t + P a t * D b = if a = b then D a else 0 := by
82   have h := (hd a).mul (hd b)
83   change HasDerivAt (fun s => P a s * P b s) (D a * P b t + P a t * D b) t at h
84   by_cases hab : a = b
85   · subst b
86     have heq : (fun s => P a s * P a s) = P a := by
87       funext s
88       simpa only [ite_true] using hmul s a a
89     rw [heq] at h
90     simpa only [ite_true] using h.unique (hd a)
91   · have heq : (fun s => P a s * P b s) = fun _ => (0 : R) := by
92       funext s
93       simpa only [hab, ite_false] using hmul s a b
94     rw [heq] at h
95     simpa only [hab, ite_false] using h.unique (hasDerivAt_const t (0 : R))
96 
97 omit [StarRing R] [StarModule ℝ R] [ContinuousStar R] [DecidableEq I] in
98 theorem differentiated_completeness
99     (hd : ∀ a, HasDerivAt (P a) (D a) t)
100     (hsum : ∀ s, ∑ a, P a s = 1) : ∑ a, D a = 0 := by
101   have h := HasDerivAt.fun_sum (u := Finset.univ) (fun a _ => hd a)
102   simp_rw [hsum] at h
103   exact h.unique (hasDerivAt_const t (1 : R))
104 
105 omit [Fintype I] [DecidableEq I] in
106 theorem differentiated_selfAdjoint
107     (hd : ∀ a, HasDerivAt (P a) (D a) t)
108     (hstar : ∀ s a, star (P a s) = P a s) (a : I) : star (D a) = D a := by
109   have h := (hd a).star
110   simp_rw [hstar] at h
111   exact h.unique (hd a)
112 
113 theorem canonical_connection_of_hasDerivAt
114     (hd : ∀ a, HasDerivAt (P a) (D a) t)
115     (hmul : ∀ s a b, P a s * P b s = if a = b then P a s else 0)
116     (hsum : ∀ s, ∑ a, P a s = 1)
117     (hstar : ∀ s a, star (P a s) = P a s) :
118     let C := canonical (fun a => P a t) D
119     star C = -C ∧
120       (∀ b, C * P b t - P b t * C = D b) ∧
121       (1 / 2 : ℝ) • (∑ a, (D a * P a t - P a t * D a)) = C := by
122   dsimp only
123   have hj := differentiated_orthogonality P D t hd hmul
124   have hdiag (a : I) : D a * P a t + P a t * D a = D a := by
125     simpa only [ite_true] using hj a a
126   have hz := differentiated_completeness P D t hd hsum
127   refine ⟨?_, ?_, ?_⟩
128   · exact canonical_skewAdjoint _ _ (hstar t)
129       (differentiated_selfAdjoint P D t hd hstar) hz hdiag
130   · exact canonical_commutator _ _ (hmul t) (hsum t) hj
131   · exact canonical_half_commutator _ _ hz hdiag
132 end Derivatives
133 end KomorebiPaperVII.Connection
134 
135 #print axioms KomorebiPaperVII.Connection.canonical_right
136 #print axioms KomorebiPaperVII.Connection.canonical_left_relation
137 #print axioms KomorebiPaperVII.Connection.canonical_commutator
138 #print axioms KomorebiPaperVII.Connection.canonical_skewAdjoint
139 #print axioms KomorebiPaperVII.Connection.canonical_half_commutator
140 #print axioms KomorebiPaperVII.Connection.differentiated_orthogonality
141 #print axioms KomorebiPaperVII.Connection.differentiated_completeness
142 #print axioms KomorebiPaperVII.Connection.differentiated_selfAdjoint
143 #print axioms KomorebiPaperVII.Connection.canonical_connection_of_hasDerivAt

Back to source controls