Source: ProCGroups.FoxDifferential.Common.Jacobian
1import Mathlib.Algebra.Module.LinearMap.Basic
2import Mathlib.Data.Matrix.Mul
4/-!
5# Fox differential: common — jacobian
7The principal declarations in this module are:
9- `foxJacobianMatrix`
10 A Fox-Jacobian family packaged as a finite matrix.
11- `foxJacobianId`
12 The identity Fox-Jacobian family with Kronecker-delta entries.
13- `foxJacobianMatrix_apply`
14 The packaged Fox-Jacobian matrix entry is the corresponding Jacobian family entry.
15- `foxJacobianId_apply`
16 The identity Fox-Jacobian evaluates to the Kronecker-delta coefficient at the chosen pair of
17 indices.
18-/
20namespace FoxDifferential
22noncomputable section
24open scoped BigOperators
26universe u v w z
28section JacobianLinearMap
30variable {R : Type u} [Ring R]
31variable {X : Type v}
32variable {Y : Type w}
34/-- A Fox-Jacobian family packaged as a finite matrix. -/
35def foxJacobianMatrix (jac : X → Y → R) : Matrix X Y R :=
36 jac
38omit [Ring R] in
39/-- The packaged Fox-Jacobian matrix entry is the corresponding Jacobian family entry. -/
40@[simp]
41theorem foxJacobianMatrix_apply (jac : X → Y → R) (x : X) (y : Y) :
42 foxJacobianMatrix jac x y = jac x y :=
43 rfl
45section Identity
47variable [DecidableEq X]
49/-- The identity Fox-Jacobian family with Kronecker-delta entries. -/
50def foxJacobianId : X → X → R := fun x => Pi.single x (1 : R)
52/--
53The identity Fox-Jacobian evaluates to the Kronecker-delta coefficient at the chosen pair of
54indices.
55-/
56@[simp]
57theorem foxJacobianId_apply (x y : X) :
58 foxJacobianId (R := R) (X := X) x y = (Pi.single x (1 : R) : X → R) y :=
59 rfl
61/-- The identity Fox-Jacobian family is the identity matrix. -/
62@[simp]
63theorem foxJacobianMatrix_id :
64 foxJacobianMatrix (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
65 (1 : Matrix X X R) := by
66 ext x y
67 by_cases hxy : x = y
68 · subst y
69 simp only [foxJacobianMatrix, foxJacobianId, Pi.single_eq_same, Matrix.one_apply_eq]
70 · simp only [foxJacobianMatrix, foxJacobianId, ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne',
71 Matrix.one_apply_ne]
73end Identity
75/--
76A Fox-Jacobian family determines the corresponding finite linear map between free coefficient
77modules.
78-/
79def foxJacobianLinearMap [Fintype X] (jac : X → Y → R) :
80 (X → R) →ₗ[R] (Y → R) where
81 toFun v := fun y => ∑ x : X, v x * jac x y
82 map_add' v w := by
83 funext y
84 simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
85 map_smul' a v := by
86 funext y
87 simp only [Pi.smul_apply]
88 change (∑ x : X, (a * v x) * jac x y) = a * ∑ x : X, v x * jac x y
89 simp only [mul_assoc, Finset.mul_sum]
91/--
92The linear map associated with a Fox-Jacobian family is evaluated by the finite matrix
93coefficient formula.
94-/
95@[simp]
96theorem foxJacobianLinearMap_apply
97 [Fintype X]
98 (jac : X → Y → R) (v : X → R) (y : Y) :
99 foxJacobianLinearMap jac v y = ∑ x : X, v x * jac x y :=
100 rfl
102/-- The Fox-Jacobian linear map is row-vector multiplication by the corresponding matrix. -/
103theorem foxJacobianLinearMap_eq_vecMul
104 [Fintype X]
105 (jac : X → Y → R) (v : X → R) :
106 foxJacobianLinearMap jac v = Matrix.vecMul v (foxJacobianMatrix jac) := by
107 funext y
108 simp only [foxJacobianLinearMap_apply, Matrix.vecMul, dotProduct, foxJacobianMatrix]
110/--
111The identity Fox-Jacobian induces the identity linear map on the finite free coefficient module.
112-/
113@[simp]
114theorem foxJacobianLinearMap_id [Fintype X] [DecidableEq X] :
115 foxJacobianLinearMap (R := R) (X := X) (Y := X) (foxJacobianId (R := R) (X := X)) =
116 (LinearMap.id : (X → R) →ₗ[R] (X → R)) := by
117 apply LinearMap.ext
118 intro v
119 funext y
120 change (∑ x : X, v x * (Pi.single x (1 : R) : X → R) y) = v y
121 rw [Finset.sum_eq_single y]
122 · simp only [Pi.single_eq_same, mul_one]
123 · intro x _ hxy
124 rw [Pi.single_eq_of_ne (Ne.symm hxy)]
125 simp only [mul_zero]
126 · intro hy
127 simp only [Finset.mem_univ, not_true_eq_false] at hy
129variable {Z : Type z}
131/--
132Composition of finite Fox-Jacobian linear maps is given by multiplication of the corresponding
133Jacobian matrices.
134-/
135theorem foxJacobianLinearMap_comp
136 [Fintype X] [Fintype Y]
137 (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
138 (foxJacobianLinearMap jacYZ).comp (foxJacobianLinearMap jacXY) =
139 foxJacobianLinearMap (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) := by
140 ext v z
141 change
142 (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
143 ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z
144 calc
145 (∑ y : Y, (∑ x : X, v x * jacXY x y) * jacYZ y z) =
146 ∑ y : Y, ∑ x : X, (v x * jacXY x y) * jacYZ y z := by
147 simp only [Finset.sum_mul]
148 _ = ∑ x : X, ∑ y : Y, (v x * jacXY x y) * jacYZ y z := by
149 rw [Finset.sum_comm]
150 _ = ∑ x : X, v x * ∑ y : Y, jacXY x y * jacYZ y z := by
151 refine Finset.sum_congr rfl ?_
152 intro x _
153 rw [Finset.mul_sum]
154 refine Finset.sum_congr rfl ?_
155 intro y _
156 rw [mul_assoc]
158/-- Composition of Fox-Jacobian matrices is finite matrix multiplication. -/
159theorem foxJacobianMatrix_comp
160 [Fintype Y]
161 (jacXY : X → Y → R) (jacYZ : Y → Z → R) :
162 foxJacobianMatrix (R := R) (X := X) (Y := Z)
163 (fun x z => ∑ y : Y, jacXY x y * jacYZ y z) =
164 foxJacobianMatrix (R := R) (X := X) (Y := Y) jacXY *
165 foxJacobianMatrix (R := R) (X := Y) (Y := Z) jacYZ := by
166 apply Matrix.ext
167 intro x z
168 simp only [foxJacobianMatrix, Matrix.mul_apply]
170/--
171A Fox-Jacobian linear map sends a standard source coordinate to the corresponding Jacobian row.
172-/
173@[simp]
174theorem foxJacobianLinearMap_single [Fintype X] [DecidableEq X] (jac : X → Y → R) (x : X) :
175 foxJacobianLinearMap jac (Pi.single x (1 : R)) = jac x := by
176 funext y
177 change (∑ z : X, ((Pi.single x (1 : R) : X → R) z) * jac z y) = jac x y
178 rw [Finset.sum_eq_single x]
179 · simp only [Pi.single_eq_same, one_mul]
180 · intro z _ hz
181 simp only [Pi.single_eq_of_ne hz, zero_mul]
182 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]
184variable {M : Type*} [AddCommMonoid M] [Module R M]
186/--
187Linear maps out of finite coordinate vectors are determined by their values on the standard
188coordinate vectors.
189-/
190theorem linearMap_ext_pi_single
191 [Finite X] [DecidableEq X]
192 {L₁ L₂ : (X → R) →ₗ[R] M}
193 (h : ∀ x : X, L₁ (Pi.single x (1 : R)) = L₂ (Pi.single x (1 : R))) :
194 L₁ = L₂ := by
195 classical
196 letI := Fintype.ofFinite X
197 apply LinearMap.ext
198 intro v
199 have hv : v = ∑ x : X, v x • (Pi.single x (1 : R) : X → R) := by
200 funext y
201 rw [Finset.sum_apply]
202 rw [Finset.sum_eq_single y]
203 · simp only [Pi.smul_apply, Pi.single_eq_same, smul_eq_mul, mul_one]
204 · intro x _ hxy
205 change v x * ((Pi.single x (1 : R) : X → R) y) = 0
206 rw [Pi.single_eq_of_ne (Ne.symm hxy)]
207 simp only [mul_zero]
208 · intro hy
209 simp only [Finset.mem_univ, not_true_eq_false] at hy
210 calc
211 L₁ v = L₁ (∑ x : X, v x • (Pi.single x (1 : R) : X → R)) := by
212 exact congrArg L₁ hv
213 _ = ∑ x : X, v x • L₁ (Pi.single x (1 : R)) := by simp only [map_sum, map_smul]
214 _ = ∑ x : X, v x • L₂ (Pi.single x (1 : R)) := by simp only [h]
215 _ = L₂ (∑ x : X, v x • (Pi.single x (1 : R) : X → R)) := by simp only [map_sum, map_smul]
216 _ = L₂ v := by
217 exact (congrArg L₂ hv).symm
219end JacobianLinearMap
221end
223end FoxDifferential