Exact source: MathlibAnnex/Analysis/Distribution/Divergence.lean
Pinned GitHub source · Raw UTF-8 source
Back to Vanishing weak gradient tested by divergence
1import MathlibAnnex.Analysis.Distribution.TestField2import Mathlib.LinearAlgebra.Trace3import Mathlib.Analysis.Calculus.FDeriv.Mul4import Mathlib.Analysis.Calculus.FDeriv.Add56/-! Basis-free divergence and common test-field identities. -/7noncomputable section8open Set9open scoped BigOperators1011namespace MathlibAnnex12variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]1314/-- Divergence is the trace of the Fréchet derivative on a finite-dimensional15real normed space. The instance is part of the public declaration type. -/16def divergence [FiniteDimensional ℝ E] (W : E → E) (x : E) : ℝ :=17 LinearMap.trace ℝ E (fderiv ℝ W x).toLinearMap1819section FiniteDimensional20variable [FiniteDimensional ℝ E]2122/-- Rank-one trace identity in the continuous-linear-map representation. -/23theorem trace_smulRight (L : E →L[ℝ] ℝ) (v : E) :24 LinearMap.trace ℝ E (L.smulRight v).toLinearMap = L v := by25 change LinearMap.trace ℝ E (L.toLinearMap.smulRight v) = L v26 exact LinearMap.trace_smulRight _ _2728/-- The minus sign is the chain-rule contribution of translation followed by negation. -/29theorem divergence_sub_smul {φ : E → ℝ} (y z v : E)30 (hφ : DifferentiableAt ℝ φ (y - z)) :31 divergence (fun w => φ (y - w) • v) z = - fderiv ℝ φ (y - z) v := by32 have hsub := (hasFDerivAt_id (𝕜 := ℝ) z).const_sub y33 have hscalar := hφ.hasFDerivAt.comp z hsub34 have hfield := (hscalar.smul_const v).fderiv35 have hfd : fderiv ℝ (fun w : E => φ (y - w) • v) z =36 ((fderiv ℝ φ (y - z)).comp (-(ContinuousLinearMap.id ℝ E))).smulRight v := by37 simpa only [Function.comp_apply, id_eq] using hfield38 rw [divergence, hfd, trace_smulRight]39 simp4041namespace CompactC1VectorField4243theorem divergence_eq_zero_of_not_mem_carrier (W : CompactC1VectorField E)44 {x : E} (hx : x ∉ W.carrier) : divergence W x = 0 := by45 simp [divergence, W.fderiv_eq_zero_of_not_mem_carrier hx]4647theorem support_divergence_subset (W : CompactC1VectorField E) :48 Function.support (divergence W) ⊆ W.carrier := by49 intro x hx50 by_contra h51 exact hx (W.divergence_eq_zero_of_not_mem_carrier h)5253end CompactC1VectorField5455/-- Coordinate realization, including the empty index type. The ambient norm56is the standard Pi norm; no identification with `EuclideanSpace` is implicit. -/57theorem divergence_pi {ι : Type*} [Fintype ι] [DecidableEq ι]58 (W : (ι → ℝ) → (ι → ℝ)) (x : ι → ℝ) :59 divergence W x = ∑ i : ι, (fderiv ℝ W x (Pi.single i 1)) i := by60 rw [divergence, LinearMap.trace_eq_matrix_trace ℝ (Pi.basisFun ℝ ι)]61 simp [Matrix.trace, LinearMap.toMatrix_apply]6263end FiniteDimensional64end MathlibAnnex