The divergence theorem on affine parallelepipeds

Let L be a real continuous linear automorphism of ι → ℝ, let p : ι → ℝ and write A u = p + L u, so that A maps the unit cube [0, 1]^ι onto a parallelepiped. A flux field F : ι → (ι → ℝ) → E (component i of the field is F i) is transported to the unit cube by the cofactor pullback

H j u = det L • ∑ i, (L⁻¹)ⱼᵢ • F i (A u),

where (L⁻¹)ⱼᵢ = L.symm (Pi.single i 1) j is the (j, i) entry of the matrix of L⁻¹. The matrix det L • L⁻¹ is the adjugate of L. The field H is the contravariant Piola transform of F along A: it is the coordinate expression of the pullback along A of the flux form ∑ i, (-1)^i F i dx₀ ∧ ⋯ ∧ dxₙ (with dxᵢ omitted from the i-th product). Its divergence is the signed determinant times the divergence of F:

∑ j, ∂ⱼ H j (u) = det L • ∑ i, ∂ᵢ F i (A u),

whenever every F i is differentiable at A u, because the coefficient of ∂ₖ F i is det L • ∑ j, (L⁻¹)ⱼᵢ Lₖⱼ = det L • δₖᵢ (ContinuousLinearEquiv.sum_cofactor_comp_apply_single). Unlike the absolute value in the change of variables formula, the determinant here is signed.

Applying Mathlib's divergence theorem on the unit cube, MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable', to H gives the divergence theorem on the parallelepiped A '' [0, 1]^ι, with the boundary integrals of H over the faces of the unit cube on one side. As in Mathlib, only continuity on the closed parallelepiped, differentiability at the interior points off a countable set and integrability of the divergence are assumed; no continuity of the derivative is needed.

Main declarations

• ContinuousLinearEquiv.affineFluxPullback: the cofactor pullback H of a flux field.
• ContinuousLinearEquiv.hasFDerivAt_affineFluxPullback: the derivative of H j at u.
• ContinuousLinearEquiv.sum_fderiv_affineFluxPullback: the divergence of H at u is det L times the divergence of F at A u.
• ContinuousLinearEquiv.integral_divergence_affineFluxPullback: the divergence theorem on an affine parallelepiped, in cofactor form on the unit cube.

References

• P. G. Ciarlet, Mathematical Elasticity, Vol. I: Three-Dimensional Elasticity, North-Holland (1988), §1.7, for the Piola transform and the Piola identity, of which the cofactor pullback and its divergence formula are the affine case.

noncomputable def ContinuousLinearEquiv.affineFluxPullback {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : (ι → ℝ) ≃L[ℝ] ι → ℝ) (p : ι → ℝ) (F : ι → (ι → ℝ) → E) (j : ι) (u : ι → ℝ) : E

The cofactor pullback of a flux field F along the affine map u ↦ p + L u: H j u = det L • ∑ i, (L⁻¹)ⱼᵢ • F i (p + L u), where (L⁻¹)ⱼᵢ = L.symm (Pi.single i 1) j. When every F i is differentiable at p + L u, its divergence at u is det L times the divergence of F at p + L u (ContinuousLinearEquiv.sum_fderiv_affineFluxPullback).

theorem ContinuousLinearEquiv.affineFluxPullback_apply {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : (ι → ℝ) ≃L[ℝ] ι → ℝ) (p : ι → ℝ) (F : ι → (ι → ℝ) → E) (j : ι) (u : ι → ℝ) : L.affineFluxPullback p F j u = LinearMap.det ↑↑L • ∑ i : ι, L.symm (Pi.single i 1) j • F i (p + L u)

@[simp]

theorem ContinuousLinearEquiv.affineFluxPullback_refl {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ι → ℝ) (F : ι → (ι → ℝ) → E) (j : ι) (u : ι → ℝ) : (ContinuousLinearEquiv.refl ℝ (ι → ℝ)).affineFluxPullback p F j u = F j (p + u)

For L the identity the cofactor pullback is the translated field u ↦ F j (p + u).

theorem ContinuousLinearEquiv.continuousOn_affineFluxPullback {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : (ι → ℝ) ≃L[ℝ] ι → ℝ) (p : ι → ℝ) (F : ι → (ι → ℝ) → E) {s : Set (ι → ℝ)} (hF : ∀ (i : ι), ContinuousOn (F i) ((fun (u : ι → ℝ) => p + L u) '' s)) (j : ι) : ContinuousOn (L.affineFluxPullback p F j) s

The cofactor pullback of a field continuous on the parallelepiped A '' s is continuous on s, where A u = p + L u.

theorem ContinuousLinearEquiv.hasFDerivAt_affineFluxPullback {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : (ι → ℝ) ≃L[ℝ] ι → ℝ) (p : ι → ℝ) (F : ι → (ι → ℝ) → E) {F' : ι → (ι → ℝ) →L[ℝ] E} {u : ι → ℝ} (hF : ∀ (i : ι), HasFDerivAt (F i) (F' i) (p + L u)) (j : ι) : HasFDerivAt (L.affineFluxPullback p F j) (LinearMap.det ↑↑L • ∑ i : ι, L.symm (Pi.single i 1) j • F' i ∘SL ↑L) u

The derivative of a component of the cofactor pullback: if each F i has derivative F' i at p + L u, then H j has derivative det L • ∑ i, (L⁻¹)ⱼᵢ • (F' i ∘ L) at u.

theorem ContinuousLinearEquiv.sum_fderiv_affineFluxPullback {ι : Type u_1} {E : Type u_2} [Fintype ι] [DecidableEq ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (L : (ι → ℝ) ≃L[ℝ] ι → ℝ) (p : ι → ℝ) (F : ι → (ι → ℝ) → E) {u : ι → ℝ} (hF : ∀ (i : ι), DifferentiableAt ℝ (F i) (p + L u)) : ∑ j : ι, (fderiv ℝ (L.affineFluxPullback p F j) u) (Pi.single j 1) = LinearMap.det ↑↑L • ∑ i : ι, (fderiv ℝ (F i) (p + L u)) (Pi.single i 1)

The divergence of the cofactor pullback. If every component of the field F is differentiable at p + L u, then the divergence of the cofactor pullback at u is det L times the divergence of F at p + L u.

theorem ContinuousLinearEquiv.integral_divergence_affineFluxPullback {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {n : ℕ} (L : (Fin (n + 1) → ℝ) ≃L[ℝ] Fin (n + 1) → ℝ) (p : Fin (n + 1) → ℝ) (F : Fin (n + 1) → (Fin (n + 1) → ℝ) → E) (F' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable) (Hc : ∀ (i : Fin (n + 1)), ContinuousOn (F i) ((fun (u : Fin (n + 1) → ℝ) => p + L u) '' Set.Icc 0 1)) (Hd : ∀ u ∈ (Set.univ.pi fun (x : Fin (n + 1)) => Set.Ioo 0 1) \ s, ∀ (i : Fin (n + 1)), HasFDerivAt (F i) (F' i (p + L u)) (p + L u)) (Hi : MeasureTheory.IntegrableOn (fun (u : Fin (n + 1) → ℝ) => ∑ i : Fin (n + 1), (F' i (p + L u)) (Pi.single i 1)) (Set.Icc 0 1) MeasureTheory.volume) : LinearMap.det ↑↑L • ∫ (u : Fin (n + 1) → ℝ) in Set.Icc 0 1, ∑ i : Fin (n + 1), (F' i (p + L u)) (Pi.single i 1) = ∑ j : Fin (n + 1), ((∫ (x : Fin n → ℝ) in Set.Icc 0 1, L.affineFluxPullback p F j (j.insertNth 1 x)) - ∫ (x : Fin n → ℝ) in Set.Icc 0 1, L.affineFluxPullback p F j (j.insertNth 0 x))

The divergence theorem on an affine parallelepiped. Let A u = p + L u and let F be a flux field continuous on the parallelepiped A '' [0, 1]ⁿ⁺¹, differentiable with derivatives F' i at A u for every interior point u of the unit cube off a countable set, and with u ↦ div F (A u) integrable on the unit cube. Then det L times the integral of div F ∘ A over the unit cube is the boundary sum of the cofactor pullback H = L.affineFluxPullback p F: the sum over j of the integral of H j over the front face u j = 1 minus that over the back face u j = 0. The determinant is signed.