Exact source: MathlibAnnex/Analysis/Calculus/Piola.lean
Pinned GitHub source · Raw UTF-8 source
Back to Zero integral of a compactly supported divergence · Back to Smooth compact perturbations preserve the determinant integral difference
1import Mathlib.Analysis.Calculus.FDeriv.Symmetric2import Mathlib.Analysis.Calculus.FDeriv.Const3import Mathlib.LinearAlgebra.Matrix.Determinant.Basic4import Mathlib.MeasureTheory.Integral.DivergenceTheorem5import Mathlib.MeasureTheory.SpecificCodomains.Pi6import Mathlib.Tactic78/-!9# Smooth Piola identity in finite coordinate spaces1011Hessian symmetry and antisymmetry of two-row replacement determinants give12the divergence-free cofactor identity. The compact-support divergence theorem13and a finite coordinate telescope then show that smooth compact perturbations14have determinant differences of integral zero.15-/1617namespace MathlibAnnex18namespace Piola1920/-- Matrix entries evaluated on standard coordinate vectors. -/21private noncomputable def stdMatrix {n N : ℕ}22 (A : (Fin n → ℝ) →L[ℝ] (Fin N → ℝ)) : Matrix (Fin N) (Fin n) ℝ :=23 fun i j => A (Pi.single j 1) i2425end Piola26end MathlibAnnex2728/-!29# Cofactor identities3031Cofactors are defined directly by determinant row replacement. This avoids32adjugate transpose conventions and keeps every later identity in the same row33language as the determinant telescope.34-/3536noncomputable section3738open scoped BigOperators3940namespace MathlibAnnex41namespace Piola4243/-- Standard coordinate row. -/44def basisRow {n : ℕ} (j : Fin n) : (Fin n → ℝ) := Pi.single j 14546@[simp] theorem basisRow_apply {n : ℕ} (j q : Fin n) :47 basisRow j q = if q = j then 1 else 0 := by48 classical49 simp [basisRow, Pi.single_apply, eq_comm]5051/-- Cofactor row, defined without choosing an adjugate convention. -/52def cofactorRow {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)53 (i : Fin n) : (Fin n → ℝ) :=54 fun j => (A.updateRow i (basisRow j)).det5556/-- Matrix with two designated rows replaced by coordinate rows. -/57def twoRowReplacement {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ)58 (i k j q : Fin n) : Matrix (Fin n) (Fin n) ℝ :=59 (A.updateRow i (basisRow j)).updateRow k (basisRow q)6061/-- Divergence in the coordinate basis consumed by Mathlib's box theorem. -/62def coordinateDivergence {m : ℕ}63 (F : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)) (x : (Fin (m + 1) → ℝ)) : ℝ :=64 ∑ i, fderiv ℝ F x (Pi.single i 1) i6566end Piola67end MathlibAnnex686970/-!71# Cofactor identities72-/7374noncomputable section7576open scoped BigOperators7778namespace MathlibAnnex79namespace Piola8081/-- Coordinate-basis expansion of a row vector. -/82theorem sum_smul_basisRow {n : ℕ} (v : (Fin n → ℝ)) :83 (∑ j, v j • basisRow j) = v := by84 classical85 ext q86 simp [basisRow, Pi.single_apply]8788/-- Determinant is linear in one updated row over a finite sum. -/89theorem det_updateRow_finset_sum {n : ℕ}90 (A : Matrix (Fin n) (Fin n) ℝ) (i : Fin n)91 (s : Finset (Fin n)) (v : Fin n → (Fin n → ℝ)) :92 (A.updateRow i (s.sum v)).det =93 s.sum (fun j => (A.updateRow i (v j)).det) := by94 classical95 induction s using Finset.induction_on with96 | empty =>97 apply Matrix.det_eq_zero_of_row_eq_zero i98 intro j99 simp100 | @insert j s hj ih =>101 rw [Finset.sum_insert hj, Matrix.det_updateRow_add, ih, Finset.sum_insert hj]102103/-- Expansion along the updated row in the row-replacement cofactor convention. -/104theorem det_updateRow_eq_sum_mul_cofactorRow {n : ℕ}105 (A : Matrix (Fin n) (Fin n) ℝ) (i : Fin n) (v : (Fin n → ℝ)) :106 (A.updateRow i v).det = ∑ j, v j * cofactorRow A i j := by107 classical108 calc109 (A.updateRow i v).det =110 (A.updateRow i (∑ j, v j • basisRow j)).det := by111 rw [sum_smul_basisRow]112 _ = ∑ j, (A.updateRow i (v j • basisRow j)).det := by113 simpa using114 (det_updateRow_finset_sum A i Finset.univ115 (fun j => v j • basisRow j))116 _ = ∑ j, v j * cofactorRow A i j := by117 apply Finset.sum_congr rfl118 intro j _119 rw [Matrix.det_updateRow_smul]120 rfl121122end Piola123end MathlibAnnex124125126/-!127# Cofactor identities128129The completed field definition is isolated from the differential Piola proof so130that it remains an independent node of the existing import DAG.131-/132133noncomputable section134135namespace MathlibAnnex136namespace Piola137138/-- Cofactor row field of the derivative of a smooth square map. -/139def cofactorRowField {n : ℕ} (H : (Fin n → ℝ) → (Fin n → ℝ)) (i : Fin n) :140 (Fin n → ℝ) → (Fin n → ℝ) :=141 fun x => cofactorRow (stdMatrix (fderiv ℝ H x)) i142143end Piola144end MathlibAnnex145146147/-!148# Cofactor identities149150This packet is purely finite-dimensional algebra. It does not import151calculus, integration, or compact-support machinery.152-/153154noncomputable section155156open scoped BigOperators157158namespace MathlibAnnex159namespace Piola160161/-- Exchanging the two replacement rows negates the determinant. -/162theorem det_twoRowReplacement_swap {n : ℕ}163 (A : Matrix (Fin n) (Fin n) ℝ) (i k j q : Fin n) (hik : i ≠ k) :164 (twoRowReplacement A i k j q).det =165 -(twoRowReplacement A i k q j).det := by166 classical167 have hswap :168 twoRowReplacement A i k q j ∘ Equiv.swap i k =169 twoRowReplacement A i k j q := by170 funext r171 by_cases hri : r = i172 · subst r173 simp [twoRowReplacement, Function.comp_apply, hik]174 · by_cases hrk : r = k175 · subst r176 simp [twoRowReplacement, Function.comp_apply, hik]177 · rw [Function.comp_apply, Equiv.swap_apply_of_ne_of_ne hri hrk]178 simp [twoRowReplacement, hri, hrk]179 change (Matrix.detRowAlternating180 (R := ℝ) (n := Fin n)) (twoRowReplacement A i k j q) =181 -(Matrix.detRowAlternating182 (R := ℝ) (n := Fin n)) (twoRowReplacement A i k q j)183 calc184 (Matrix.detRowAlternating185 (R := ℝ) (n := Fin n)) (twoRowReplacement A i k j q) =186 (Matrix.detRowAlternating187 (R := ℝ) (n := Fin n))188 (twoRowReplacement A i k q j ∘ Equiv.swap i k) := by189 rw [hswap]190 _ = -(Matrix.detRowAlternating191 (R := ℝ) (n := Fin n)) (twoRowReplacement A i k q j) :=192 (Matrix.detRowAlternating193 (R := ℝ) (n := Fin n)).map_swap194 (twoRowReplacement A i k q j) hik195196/-- A symmetric coefficient matrix contracted with an antisymmetric matrix has197zero finite double sum. -/198theorem sum_symmetric_mul_antisymmetric_eq_zero199 {ι : Type*} [Fintype ι]200 (B D : ι → ι → ℝ)201 (hB : ∀ i j, B i j = B j i)202 (hD : ∀ i j, D i j = -D j i) :203 (∑ i, ∑ j, B i j * D i j) = 0 := by204 have hneg : (∑ i, ∑ j, B i j * D i j) =205 -(∑ i, ∑ j, B i j * D i j) := by206 calc207 (∑ i, ∑ j, B i j * D i j) =208 ∑ i, ∑ j, B j i * D j i := by209 rw [Finset.sum_comm]210 _ = ∑ i, ∑ j, -(B i j * D i j) := by211 apply Fintype.sum_congr212 intro i213 apply Fintype.sum_congr214 intro j215 rw [hB j i, hD j i]216 ring217 _ = -(∑ i, ∑ j, B i j * D i j) := by218 simp only [Finset.sum_neg_distrib]219 linarith220221/-- Algebraic cancellation form used after Hessian symmetry is exposed. -/222theorem sum_hessian_twoRowReplacement_eq_zero {n : ℕ}223 (A : Matrix (Fin n) (Fin n) ℝ) (i k : Fin n) (hik : i ≠ k)224 (B : Fin n → Fin n → ℝ) (hB : ∀ j q, B j q = B q j) :225 (∑ j, ∑ q, B j q * (twoRowReplacement A i k j q).det) = 0 := by226 apply sum_symmetric_mul_antisymmetric_eq_zero B227 (fun j q => (twoRowReplacement A i k j q).det) hB228 intro j q229 exact det_twoRowReplacement_swap A i k j q hik230231end Piola232end MathlibAnnex233234235/-!236# Cofactor identities237238This module separates the already available symmetry of the second derivative239and the already compiled two-row determinant alternation from the remaining240calculus expansion of the cofactor derivative.241-/242243noncomputable section244245open scoped BigOperators Topology246247namespace MathlibAnnex248namespace Piola249250/-- One scalar coordinate of the second Fréchet derivative. -/251def hessianCoordinate {n : ℕ} (H : (Fin n → ℝ) → (Fin n → ℝ))252 (x : (Fin n → ℝ)) (k j q : Fin n) : ℝ :=253 fderiv ℝ (fderiv ℝ H) x (basisRow j) (basisRow q) k254255/-- Coordinate Hessian coefficients are symmetric in their two input rows. -/256theorem hessianCoordinate_comm {n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)}257 (hH : ContDiff ℝ 2 H) (x : (Fin n → ℝ)) (k j q : Fin n) :258 hessianCoordinate H x k j q = hessianCoordinate H x k q j :=259 by260 have hsymm : IsSymmSndFDerivAt ℝ H x :=261 hH.contDiffAt.isSymmSndFDerivAt (by norm_num)262 unfold hessianCoordinate263 exact congrArg (fun y : (Fin n → ℝ) => y k)264 (hsymm (basisRow j) (basisRow q))265266/-- The scalar Hessian coefficients cancel against an antisymmetric pair of267replacement rows. -/268theorem sum_hessianCoordinate_twoRowReplacement_eq_zero269 {n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)}270 (hH : ContDiff ℝ 2 H) (x : (Fin n → ℝ))271 (A : Matrix (Fin n) (Fin n) ℝ)272 (i k : Fin n) (hik : i ≠ k) :273 (∑ j, ∑ q,274 hessianCoordinate H x k j q *275 (twoRowReplacement A i k j q).det) = 0 :=276 by277 apply sum_hessian_twoRowReplacement_eq_zero A i k hik278 intro j q279 exact hessianCoordinate_comm hH x k j q280281/-- Once the derivative of the cofactor row is expanded into its rowwise282Hessian formula, Piola cancellation follows from the preceding finite lemma. -/283theorem piola_divergence_eq_zero_of_expansion284 {n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)}285 (hH : ContDiff ℝ 2 H) (i : Fin n) (x : (Fin n → ℝ))286 (hexpand :287 (∑ j, fderiv ℝ (cofactorRowField H i) x288 (Pi.single j 1) j) =289 ∑ k ∈ Finset.univ.erase i, ∑ j, ∑ q,290 hessianCoordinate H x k j q *291 (twoRowReplacement292 (stdMatrix (fderiv ℝ H x)) i k j q).det) :293 ∑ j, fderiv ℝ (cofactorRowField H i) x294 (Pi.single j 1) j = 0 :=295 by296 rw [hexpand]297 apply Finset.sum_eq_zero298 intro k hk299 have hik : i ≠ k := (Finset.mem_erase.mp hk).1.symm300 exact sum_hessianCoordinate_twoRowReplacement_eq_zero301 hH x (stdMatrix (fderiv ℝ H x)) i k hik302303end Piola304end MathlibAnnex305306307/-!308# Cofactor identities309310Hessian symmetry and the finite antisymmetric cancellation are now isolated in311`PiolaHessian`. This module has one remaining obligation: expose the derivative312of the cofactor determinant as the exact rowwise Hessian sum.313-/314315noncomputable section316317open Set318open scoped BigOperators Topology319320namespace MathlibAnnex321namespace Piola322323/-- The cofactor row field has zero divergence (Piola identity). -/324theorem divergence_cofactorRowField_eq_zero325 {n : ℕ} {H : (Fin n → ℝ) → (Fin n → ℝ)}326 (hH : ContDiff ℝ 2 H) (i : Fin n) (x : (Fin n → ℝ)) :327 ∑ j, fderiv ℝ (cofactorRowField H i) x (Pi.single j 1) j = 0 :=328 by329 apply piola_divergence_eq_zero_of_expansion hH i x330 classical331 have hdf : DifferentiableAt ℝ (fderiv ℝ H) x := by332 fun_prop333 change (∑ j, fderiv ℝ334 (fun y r => ((stdMatrix (fderiv ℝ H y)).updateRow i335 (basisRow r)).det) x (Pi.single j 1) j) = _336 simp only [hessianCoordinate,337 twoRowReplacement, Matrix.det_apply]338 have hprod (r : Fin n) (σ : Equiv.Perm (Fin n)) :339 HasFDerivAt340 (fun y => ∏ k,341 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k)342 (∑ k,343 (∏ l ∈ Finset.univ.erase k,344 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l) •345 fderiv ℝ (fun y =>346 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x) x := by347 apply HasFDerivAt.finsetProd348 intro k hk349 by_cases hki : σ k = i350 · simpa [Matrix.updateRow_apply, hki] using351 (differentiableAt_const (c := basisRow r k)).hasFDerivAt352 · exact (by353 simp only [Matrix.updateRow_apply, hki, ↓reduceIte, stdMatrix]354 fun_prop : DifferentiableAt ℝ (fun y =>355 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x).hasFDerivAt356 have hscalar (r : Fin n) :357 HasFDerivAt358 (fun y => ∑ σ, Equiv.Perm.sign σ • ∏ k,359 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k)360 (∑ σ, Equiv.Perm.sign σ •361 (∑ k,362 (∏ l ∈ Finset.univ.erase k,363 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l) •364 fderiv ℝ (fun y =>365 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x)) x := by366 have hs : HasFDerivAt367 (∑ σ, Equiv.Perm.sign σ • (fun y : (Fin n → ℝ) => ∏ k,368 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k))369 (∑ σ, Equiv.Perm.sign σ •370 (∑ k,371 (∏ l ∈ Finset.univ.erase k,372 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l) •373 fderiv ℝ (fun y =>374 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x)) x :=375 HasFDerivAt.sum (u := Finset.univ) (fun σ _ =>376 (hprod r σ).const_smul (Equiv.Perm.sign σ))377 have hfun :378 (∑ σ, Equiv.Perm.sign σ • (fun y : (Fin n → ℝ) => ∏ k,379 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k)) =380 (fun y => ∑ σ, Equiv.Perm.sign σ • ∏ k,381 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) := by382 funext y383 simp only [Finset.sum_apply, Pi.smul_apply]384 rw [hfun] at hs385 exact hs386 have hentry (r : Fin n) (σ : Equiv.Perm (Fin n)) (k : Fin n) :387 fderiv ℝ (fun y =>388 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x389 (Pi.single r 1) =390 if σ k = i then 0 else391 (fderiv ℝ (fderiv ℝ H) x) (basisRow r) (basisRow k) (σ k) := by392 change fderiv ℝ (fun y =>393 (stdMatrix (fderiv ℝ H y)).updateRow i (basisRow r) (σ k) k) x394 (basisRow r) = _395 by_cases hki : σ k = i396 · simp [Matrix.updateRow_apply, hki]397 · simp only [Matrix.updateRow_apply, hki, ↓reduceIte, stdMatrix]398 calc399 fderiv ℝ (fun y => (fderiv ℝ H y) (basisRow k) (σ k)) x400 (basisRow r) =401 (fderiv ℝ (fun y => (fderiv ℝ H y) (basisRow k)) x)402 (basisRow r) (σ k) := by403 have hp := fderiv_pi (x := x)404 (φ := fun a y => (fderiv ℝ H y) (basisRow k) a)405 (fun a => show DifferentiableAt ℝ406 (fun y => (fderiv ℝ H y) (basisRow k) a) x from by fun_prop)407 exact (congrArg (fun L => L (basisRow r) (σ k)) hp).symm408 _ = (fderiv ℝ (fderiv ℝ H) x) (basisRow r) (basisRow k) (σ k) := by409 rw [fderiv_clm_apply hdf (differentiableAt_const (c := basisRow k))]410 simp411 have hdetprod (r K q : Fin n) (σ : Equiv.Perm (Fin n)) :412 (∏ l, ((stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r)).updateRow413 K (basisRow q) (σ l) l) =414 if σ q = K then415 ∏ l ∈ Finset.univ.erase q,416 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l417 else 0 := by418 by_cases hq : σ q = K419 · subst K420 rw [← Finset.prod_erase_mul Finset.univ421 (fun l => ((stdMatrix (fderiv ℝ H x)).updateRow i422 (basisRow r)).updateRow (σ q) (basisRow q) (σ l) l)423 (Finset.mem_univ q)]424 simp only [Matrix.updateRow_apply, basisRow_apply, σ.injective.eq_iff,425 if_pos]426 rw [mul_one]427 apply Finset.prod_congr rfl428 intro l hl429 have hlq : l ≠ q := (Finset.mem_erase.mp hl).1430 simp [hlq]431 · rw [if_neg hq]432 apply Finset.prod_eq_zero (Finset.mem_univ (σ.symm K))433 have hne : σ.symm K ≠ q := by434 intro heq435 apply hq436 rw [← heq, σ.apply_symm_apply]437 simp [Matrix.updateRow_apply, basisRow_apply, hne]438 rw [fderiv_pi (fun r => (hscalar r).differentiableAt)]439 simp only [ContinuousLinearMap.pi_apply]440 simp_rw [(hscalar _).fderiv]441 simp only [_root_.sum_apply, smul_apply]442 simp_rw [hentry]443 simp_rw [hdetprod]444 have hsumK (r q : Fin n) (σ : Equiv.Perm (Fin n)) :445 (∑ K ∈ Finset.univ.erase i,446 ((fderiv ℝ (fderiv ℝ H) x) (basisRow r)) (basisRow q) K *447 (Equiv.Perm.sign σ •448 if σ q = K then449 ∏ l ∈ Finset.univ.erase q,450 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l451 else 0)) =452 Equiv.Perm.sign σ •453 ((∏ l ∈ Finset.univ.erase q,454 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l) *455 if σ q = i then 0 else456 ((fderiv ℝ (fderiv ℝ H) x) (basisRow r)) (basisRow q) (σ q)) := by457 by_cases hqi : σ q = i458 · rw [if_pos hqi]459 simp only [mul_zero, smul_zero]460 apply Finset.sum_eq_zero461 intro K hK462 have hKi : K ≠ i := (Finset.mem_erase.mp hK).1463 simp only [hqi]464 rw [if_neg hKi.symm]465 simp466 · rw [if_neg hqi]467 rw [Finset.sum_eq_single (σ q)]468 · simp only [if_pos, mul_comm]469 rw [smul_mul_assoc]470 · intro K hK hKq471 simp [hKq.symm]472 · intro hmem473 exact (hmem (Finset.mem_erase.mpr ⟨hqi, Finset.mem_univ _⟩)).elim474 simp_rw [Finset.smul_sum, Finset.mul_sum]475 let T : Fin n → Fin n → Fin n → Equiv.Perm (Fin n) → ℝ :=476 fun K r q σ =>477 ((fderiv ℝ (fderiv ℝ H) x) (basisRow r)) (basisRow q) K *478 (Equiv.Perm.sign σ •479 if σ q = K then480 ∏ l ∈ Finset.univ.erase q,481 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l482 else 0)483 have hreorder :484 (∑ K ∈ Finset.univ.erase i, ∑ r, ∑ q, ∑ σ, T K r q σ) =485 ∑ r, ∑ σ, ∑ q, ∑ K ∈ Finset.univ.erase i, T K r q σ := by486 calc487 (∑ K ∈ Finset.univ.erase i, ∑ r, ∑ q, ∑ σ, T K r q σ) =488 ∑ K ∈ Finset.univ.erase i, ∑ r, ∑ σ, ∑ q, T K r q σ := by489 apply Finset.sum_congr rfl490 intro K hK491 apply Finset.sum_congr rfl492 intro r hr493 exact Finset.sum_comm494 _ = ∑ r, ∑ K ∈ Finset.univ.erase i, ∑ σ, ∑ q, T K r q σ := by495 exact Finset.sum_comm496 _ = ∑ r, ∑ σ, ∑ K ∈ Finset.univ.erase i, ∑ q, T K r q σ := by497 apply Finset.sum_congr rfl498 intro r hr499 exact Finset.sum_comm500 _ = ∑ r, ∑ σ, ∑ q, ∑ K ∈ Finset.univ.erase i, T K r q σ := by501 apply Finset.sum_congr rfl502 intro r hr503 apply Finset.sum_congr rfl504 intro σ hσ505 exact Finset.sum_comm506 change _ = ∑ K ∈ Finset.univ.erase i, ∑ r, ∑ q, ∑ σ, T K r q σ507 rw [hreorder]508 apply Finset.sum_congr rfl509 intro r hr510 apply Finset.sum_congr rfl511 intro σ hσ512 apply Finset.sum_congr rfl513 intro q hq514 change Equiv.Perm.sign σ •515 ((∏ l ∈ Finset.univ.erase q,516 (stdMatrix (fderiv ℝ H x)).updateRow i (basisRow r) (σ l) l) •517 if σ q = i then 0 else518 ((fderiv ℝ (fderiv ℝ H) x) (basisRow r)) (basisRow q) (σ q)) = _519 simpa only [smul_eq_mul] using (hsumK r q σ).symm520end Piola521end MathlibAnnex522523524noncomputable section525526open Set527open scoped BigOperators Topology528529namespace MathlibAnnex530namespace Piola531532def singleOutputPerturb {n : ℕ} (g : (Fin n → ℝ) → (Fin n → ℝ))533 (φ : (Fin n → ℝ) → ℝ) (i : Fin n) : (Fin n → ℝ) → (Fin n → ℝ) :=534 fun x => g x + φ x • basisRow i535536def componentFlux {n : ℕ} (g : (Fin n → ℝ) → (Fin n → ℝ))537 (φ : (Fin n → ℝ) → ℝ) (i : Fin n) : (Fin n → ℝ) → (Fin n → ℝ) :=538 fun x => φ x • cofactorRowField g i x539540def outputHybrid {n : ℕ} (g u : (Fin n → ℝ) → (Fin n → ℝ))541 (s : Finset (Fin n)) : (Fin n → ℝ) → (Fin n → ℝ) :=542 fun x i => g x i + if i ∈ s then u x i else 0543544@[simp] theorem outputHybrid_empty {n : ℕ} (g u : (Fin n → ℝ) → (Fin n → ℝ)) :545 outputHybrid g u ∅ = g := by546 funext x i547 simp [outputHybrid]548549@[simp] theorem outputHybrid_univ {n : ℕ} (g u : (Fin n → ℝ) → (Fin n → ℝ)) :550 outputHybrid g u Finset.univ = fun x => g x + u x := by551 funext x i552 simp [outputHybrid]553554end Piola555end MathlibAnnex556557noncomputable section558559open Set MeasureTheory Filter560open scoped BigOperators Topology561562namespace MathlibAnnex563namespace Piola564565theorem coordinateDivergence_eq_zero_of_not_mem_tsupport566 {m : ℕ} {F : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}567 {x : (Fin (m + 1) → ℝ)} (hx : x ∉ tsupport F) :568 coordinateDivergence F x = 0 := by569 have hderiv : fderiv ℝ F x = 0 :=570 fderiv_of_notMem_tsupport ℝ hx571 simp [coordinateDivergence, hderiv]572573theorem exists_open_box_containing_compact574 {m : ℕ} {K : Set ((Fin (m + 1) → ℝ))} (hK : IsCompact K) :575 ∃ R : ℝ, 0 < R ∧576 K ⊆ Set.pi Set.univ577 (fun _ : Fin (m + 1) => Set.Ioo (-R) R) := by578 rcases hK.isBounded.subset_closedBall 0 with ⟨R, hR⟩579 refine' ⟨max R 0 + 1, _, _⟩580 · have hmax0 : 0 ≤ max R 0 := le_max_right R 0581 linarith582 · intro x hx583 have hxR := hR hx584 have hnorm : ‖x‖ ≤ R := by585 simpa [Metric.mem_closedBall, dist_eq_norm] using hxR586 have hRmax : R ≤ max R 0 := le_max_left R 0587 apply Set.mem_univ_pi.mpr588 intro i589 have hcoord : |x i| ≤ ‖x‖ := by590 simpa [Real.norm_eq_abs] using norm_le_pi_norm x i591 constructor592 · have hlow : -‖x‖ ≤ x i := neg_le_of_abs_le hcoord593 linarith594 · have hupp : x i ≤ ‖x‖ :=595 le_trans (le_abs_self (x i)) hcoord596 linarith597598end Piola599end MathlibAnnex600601noncomputable section602603open Set MeasureTheory Filter604open scoped BigOperators Topology605606namespace MathlibAnnex607namespace Piola608609theorem integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport610 {m : ℕ} {F : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}611 (hF : ContDiff ℝ 1 F) (hFc : HasCompactSupport F) :612 ∫ x, coordinateDivergence F x = 0 :=613 by614 rcases exists_open_box_containing_compact hFc.isCompact with615 ⟨R, hR, hbox⟩616 let a : (Fin (m + 1) → ℝ) := fun _ => -R617 let b : (Fin (m + 1) → ℝ) := fun _ => R618 have hab : a ≤ b := by619 intro i620 dsimp [a, b]621 linarith622 have hsupp : Function.support F ⊆623 Set.pi Set.univ (fun i => Set.Ioo (a i) (b i)) := by624 intro x hx625 simpa [a, b] using hbox (subset_tsupport _ hx)626 have houtside : ∀ x ∉ Set.Icc a b, coordinateDivergence F x = 0 := by627 intro x hx628 apply coordinateDivergence_eq_zero_of_not_mem_tsupport629 intro hxt630 have hcoord : ∀ j, a j < x j ∧ x j < b j := by631 intro j632 simpa [a, b] using (Set.mem_univ_pi.mp (hbox hxt) j)633 apply hx634 exact ⟨fun j => (hcoord j).1.le, fun j => (hcoord j).2.le⟩635636 have hdivcont : Continuous (coordinateDivergence F) := by637 unfold coordinateDivergence638 fun_prop639 have hbox := integral_divergence_of_hasFDerivAt_off_countable640 a b hab F (fun x => fderiv ℝ F x) ∅ (by simp)641 hF.continuous.continuousOn642 (by643 intro x hx644 exact ((hF.differentiable (by norm_num)) x).hasFDerivAt)645 (by646 exact hdivcont.integrableOn_Icc)647 have hfront : ∀ (i : Fin (m + 1)) (y : Fin m → ℝ),648 F (i.insertNth (b i) y) i = 0 := by649 intro i y650 by_contra hne651 have hmem : i.insertNth (b i) y ∈ Function.support F := by652 intro hz653 exact hne (congrFun hz i)654 have hi := (Set.mem_univ_pi.mp (hsupp hmem)) i655 simpa using hi.2656 have hback : ∀ (i : Fin (m + 1)) (y : Fin m → ℝ),657 F (i.insertNth (a i) y) i = 0 := by658 intro i y659 by_contra hne660 have hmem : i.insertNth (a i) y ∈ Function.support F := by661 intro hz662 exact hne (congrFun hz i)663 have hi := (Set.mem_univ_pi.mp (hsupp hmem)) i664 simpa using hi.1665 have hboxzero : ∫ x in Set.Icc a b, coordinateDivergence F x = 0 := by666 simpa only [coordinateDivergence, hfront, hback, integral_zero,667 sub_self, Finset.sum_const_zero] using hbox668 calc669 (∫ x, coordinateDivergence F x) =670 ∫ x in Set.Icc a b, coordinateDivergence F x := by671 symm672 apply setIntegral_eq_integral_of_ae_compl_eq_zero673 filter_upwards with x hx674 exact houtside x hx675 _ = 0 := hboxzero676677end Piola678end MathlibAnnex679680noncomputable section681682open Set MeasureTheory Filter683open scoped BigOperators Topology684685namespace MathlibAnnex686namespace Piola687688theorem support_componentFlux_subset {n : ℕ}689 (g : (Fin n → ℝ) → (Fin n → ℝ)) (φ : (Fin n → ℝ) → ℝ) (i : Fin n) :690 Function.support (componentFlux g φ i) ⊆ Function.support φ :=691 by692 intro x hx hφ693 apply hx694 simp [componentFlux, hφ]695696theorem hasCompactSupport_componentFlux {n : ℕ}697 {g : (Fin n → ℝ) → (Fin n → ℝ)} {φ : (Fin n → ℝ) → ℝ} {i : Fin n}698 (hφc : HasCompactSupport φ) :699 HasCompactSupport (componentFlux g φ i) :=700 by701702 have hs := support_componentFlux_subset g φ i703 unfold HasCompactSupport at hφc ⊢704 exact hφc.of_isClosed_subset isClosed_closure (closure_mono hs)705706theorem divergence_componentFlux_eq_det_sub707 {n : ℕ} {g : (Fin n → ℝ) → (Fin n → ℝ)} {φ : (Fin n → ℝ) → ℝ}708 (hg : ContDiff ℝ 2 g) (hφ : ContDiff ℝ 1 φ)709 (i : Fin n) (x : (Fin n → ℝ)) :710 ∑ j, fderiv ℝ (componentFlux g φ i) x (Pi.single j 1) j =711 LinearMap.det ((fderiv ℝ (singleOutputPerturb g φ i) x).toLinearMap) -712 LinearMap.det ((fderiv ℝ g x).toLinearMap) :=713 by714 have hpiola := divergence_cofactorRowField_eq_zero hg i x715 have hcofactor := det_updateRow_eq_sum_mul_cofactorRow716 (stdMatrix (fderiv ℝ g x)) i717 (fun j => fderiv ℝ φ x (Pi.single j 1))718719 have hφd : DifferentiableAt ℝ φ x :=720 (hφ.differentiable (by norm_num)) x721 have hgd : DifferentiableAt ℝ g x :=722 (hg.differentiable (by norm_num)) x723 have hcofsmooth : ContDiff ℝ 1 (cofactorRowField g i) := by724 have hdg : ContDiff ℝ 1 (fderiv ℝ g) :=725 hg.fderiv_right (by norm_num)726 unfold cofactorRowField cofactorRow727 rw [contDiff_pi]728 intro q729 simp only [Matrix.det_apply']730 apply ContDiff.sum731 intro σ hσ732 apply contDiff_const.mul733 apply contDiff_prod734 intro k hk735 by_cases hki : σ k = i736 · simp only [Matrix.updateRow_apply, hki, if_true]737 fun_prop738 · simp only [Matrix.updateRow_apply, hki, if_false]739 unfold stdMatrix740 fun_prop741 have hcofd : DifferentiableAt ℝ (cofactorRowField g i) x :=742 (hcofsmooth.differentiable (by norm_num)) x743 have hsingle :744 fderiv ℝ (singleOutputPerturb g φ i) x =745 fderiv ℝ g x + (fderiv ℝ φ x).smulRight (basisRow i) := by746 unfold singleOutputPerturb747 exact (hgd.hasFDerivAt.add748 (hφd.hasFDerivAt.smul_const (basisRow i))).fderiv749 have hmat :750 stdMatrix (fderiv ℝ (singleOutputPerturb g φ i) x) =751 (stdMatrix (fderiv ℝ g x)).updateRow i752 ((stdMatrix (fderiv ℝ g x)) i +753 fun j => fderiv ℝ φ x (Pi.single j 1)) := by754 rw [hsingle]755 ext r c756 by_cases hri : r = i757 · subst r758 simp [stdMatrix, basisRow]759 · simp [stdMatrix, basisRow, hri]760 unfold componentFlux761 rw [fderiv_fun_smul hφd hcofd]762 change (∑ j, (φ x *763 fderiv ℝ (cofactorRowField g i) x (Pi.single j 1) j +764 fderiv ℝ φ x (Pi.single j 1) *765 cofactorRow (stdMatrix (fderiv ℝ g x)) i j)) = _766 rw [Finset.sum_add_distrib]767 rw [← Finset.mul_sum, hpiola, mul_zero, zero_add]768 rw [← LinearMap.det_toMatrix', ← LinearMap.det_toMatrix']769 change _ = (stdMatrix (fderiv ℝ (singleOutputPerturb g φ i) x)).det -770 (stdMatrix (fderiv ℝ g x)).det771 rw [hmat, Matrix.det_updateRow_add, Matrix.updateRow_eq_self, hcofactor]772 ring773774end Piola775end MathlibAnnex776777noncomputable section778779open Set MeasureTheory Filter780open scoped BigOperators Topology781782namespace MathlibAnnex783namespace Piola784785theorem integral_det_singleOutputPerturb_sub_eq_zero786 {m : ℕ} {g : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}787 {φ : (Fin (m + 1) → ℝ) → ℝ}788 (hg : ContDiff ℝ 2 g) (hφ : ContDiff ℝ 1 φ)789 (hφc : HasCompactSupport φ) (i : Fin (m + 1)) :790 ∫ x, (LinearMap.det ((fderiv ℝ (singleOutputPerturb g φ i) x).toLinearMap) -791 LinearMap.det ((fderiv ℝ g x).toLinearMap)) = 0 :=792 by793 have hfluxc : HasCompactSupport (componentFlux g φ i) :=794 hasCompactSupport_componentFlux hφc795 have hfluxsmooth : ContDiff ℝ 1 (componentFlux g φ i) := by796797 have hdg : ContDiff ℝ 1 (fderiv ℝ g) :=798 hg.fderiv_right (by norm_num)799 have hcofsmooth : ContDiff ℝ 1 (cofactorRowField g i) := by800 unfold cofactorRowField cofactorRow801 rw [contDiff_pi]802 intro q803 simp only [Matrix.det_apply']804 apply ContDiff.sum805 intro σ hσ806 apply contDiff_const.mul807 apply contDiff_prod808 intro k hk809 by_cases hki : σ k = i810 · simp only [Matrix.updateRow_apply, hki, if_true]811 fun_prop812 · simp only [Matrix.updateRow_apply, hki, if_false]813 unfold stdMatrix814 fun_prop815 unfold componentFlux816 exact hφ.smul hcofsmooth817 have hdiv :=818 integral_coordinateDivergence_eq_zero_of_contDiff_hasCompactSupport819 hfluxsmooth hfluxc820821 simpa only [coordinateDivergence,822 divergence_componentFlux_eq_det_sub hg hφ i] using hdiv823824end Piola825end MathlibAnnex826827noncomputable section828829open Set MeasureTheory Filter830open scoped BigOperators Topology831832namespace MathlibAnnex833namespace Piola834835theorem outputHybrid_insert_eq_singleOutputPerturb836 {n : ℕ} (g u : (Fin n → ℝ) → (Fin n → ℝ)) (s : Finset (Fin n))837 (i : Fin n) (hi : i ∉ s) :838 outputHybrid g u (insert i s) =839 singleOutputPerturb (outputHybrid g u s) (fun x => u x i) i :=840 by841 funext x j842 by_cases hji : j = i843 · subst j844 simp [outputHybrid, singleOutputPerturb, basisRow, hi]845 · simp [outputHybrid, singleOutputPerturb, basisRow, hji]846847theorem integral_det_fderiv_add_sub_eq_zero_of_contDiff848 {m : ℕ} {g u : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)}849 (hg : ContDiff ℝ (↑(⊤ : ℕ∞)) g) (hu : ContDiff ℝ (↑(⊤ : ℕ∞)) u)850 (huc : HasCompactSupport u) :851 ∫ x, (LinearMap.det ((fderiv ℝ (fun y => g y + u y) x).toLinearMap) -852 LinearMap.det ((fderiv ℝ g x).toLinearMap)) = 0 :=853 by854855 have hcomponent : ∀ i : Fin (m + 1),856 HasCompactSupport (fun x => u x i) := by857 intro i858859 have hs : Function.support (fun x => u x i) ⊆ Function.support u := by860 intro x hx hux861 exact hx (congrFun hux i)862 unfold HasCompactSupport at huc ⊢863 exact huc.of_isClosed_subset isClosed_closure (closure_mono hs)864 have hhybrid : ∀ s : Finset (Fin (m + 1)),865 ContDiff ℝ (↑(⊤ : ℕ∞)) (outputHybrid g u s) := by866 intro s867 unfold outputHybrid868 rw [contDiff_pi]869 intro i870 by_cases hi : i ∈ s871 · simp only [hi, if_true]872 fun_prop873 · simp only [hi, if_false, add_zero]874 fun_prop875 have hcoord : ∀ i : Fin (m + 1),876 ContDiff ℝ (↑(⊤ : ℕ∞)) (fun x => u x i) := by877 intro i878 fun_prop879 have hstepIntegrable : ∀ (G : (Fin (m + 1) → ℝ) → (Fin (m + 1) → ℝ)),880 ContDiff ℝ (↑(⊤ : ℕ∞)) G → ∀ i : Fin (m + 1),881 Integrable (fun x =>882 LinearMap.det ((fderiv ℝ (singleOutputPerturb G (fun y => u y i) i) x).toLinearMap) -883 LinearMap.det ((fderiv ℝ G x).toLinearMap)) := by884 intro G hG i885 let q := fun x =>886 LinearMap.det ((fderiv ℝ (singleOutputPerturb G (fun y => u y i) i) x).toLinearMap) -887 LinearMap.det ((fderiv ℝ G x).toLinearMap)888 have hpert : ContDiff ℝ (↑(⊤ : ℕ∞))889 (singleOutputPerturb G (fun y => u y i) i) := by890 unfold singleOutputPerturb891 fun_prop892 have hqcont : Continuous q := by893 exact (ContinuousLinearMap.continuous_det.comp894 (hpert.continuous_fderiv (by simp))).sub895 (ContinuousLinearMap.continuous_det.comp (hG.continuous_fderiv (by simp)))896 have hqsupp : Function.support q ⊆ tsupport (fun y => u y i) := by897 intro x hx898 by_contra hxout899 apply hx900 have hdu : fderiv ℝ (fun y => u y i) x = 0 :=901 fderiv_of_notMem_tsupport ℝ hxout902 have hGd : DifferentiableAt ℝ G x :=903 ((hG.differentiable (by simp)) x)904 have hud : DifferentiableAt ℝ (fun y => u y i) x :=905 ((hcoord i).differentiable (by simp)) x906 have hd :907 fderiv ℝ (singleOutputPerturb G (fun y => u y i) i) x =908 fderiv ℝ G x +909 (fderiv ℝ (fun y => u y i) x).smulRight (basisRow i) := by910 unfold singleOutputPerturb911 exact (hGd.hasFDerivAt.add912 (hud.hasFDerivAt.smul_const (basisRow i))).fderiv913 simp [q, hd, hdu]914 have hqcompact : HasCompactSupport q := by915 unfold HasCompactSupport916 exact (hcomponent i).of_isClosed_subset isClosed_closure917 (closure_minimal hqsupp isClosed_closure)918 exact hqcont.integrable_of_hasCompactSupport hqcompact919 let q := fun (s : Finset (Fin (m + 1))) x =>920 LinearMap.det ((fderiv ℝ (outputHybrid g u s) x).toLinearMap) -921 LinearMap.det ((fderiv ℝ g x).toLinearMap)922 have htel : ∀ s : Finset (Fin (m + 1)),923 Integrable (q s) ∧ ∫ x, q s x = 0 := by924 intro s925 induction s using Finset.induction_on with926 | empty =>927 simp [q]928 | @insert i s hi ih =>929 have hone := integral_det_singleOutputPerturb_sub_eq_zero930 ((hhybrid s).of_le (by931 exact WithTop.coe_le_coe.mpr932 (show (2 : ℕ∞) ≤ ⊤ from le_top)))933 ((hcoord i).of_le (by norm_num)) (hcomponent i) i934 rw [← outputHybrid_insert_eq_singleOutputPerturb g u s i hi] at hone935 have hstep := hstepIntegrable (outputHybrid g u s) (hhybrid s) i936 rw [← outputHybrid_insert_eq_singleOutputPerturb g u s i hi] at hstep937 have hsplit : q (insert i s) = fun x =>938 (LinearMap.det ((fderiv ℝ (outputHybrid g u (insert i s)) x).toLinearMap) -939 LinearMap.det ((fderiv ℝ (outputHybrid g u s) x).toLinearMap)) + q s x := by940 funext x941 simp only [q]942 ring943 rw [hsplit]944 constructor945 · exact hstep.add ih.1946 · rw [integral_add hstep ih.1, hone, ih.2, add_zero]947 simpa [q] using (htel Finset.univ).2948949end Piola950end MathlibAnnex