Bilinear pairings of two directional derivatives of a compactly supported map

For a compactly supported C² map u on a finite-dimensional real space and a continuous bilinear map B, the integral of B (∂_v u) (∂_w u) against a Haar measure does not change when the two directions are exchanged. Integrating by parts in the direction w turns it into -∫ B (∂_w ∂_v u) u, and the exchanged integral into -∫ B (∂_v ∂_w u) u; the two agree because the second derivative is symmetric.

Consequently the integral vanishes whenever B is alternating. That is the vanishing of the integral over the whole space of the pullback of a constant two-form along a compactly supported map — the "null Lagrangian" phenomenon: for a map from the plane to the plane, with B the standard area form and the two coordinate directions, the integrand is the Jacobian determinant. It is what makes the energy of a compactly supported map into a symplectic vector space equal the square of the L² norm of its Cauchy--Riemann defect.

Main results

• TauCeti.integral_bilinear_fderiv_apply_comm: the integral of B (∂_v u) (∂_w u) is symmetric in the two directions, and TauCeti.integral_bilinForm_fderiv_apply_comm its form for a bilinear form on a finite-dimensional space.
• TauCeti.integral_bilinForm_fderiv_apply_eq_zero_of_isAlt: for an alternating bilinear form the integral vanishes.

References

• Sébastien Gouëzel, Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean, theorem integral_bilinear_fderiv_right_eq_neg_left_of_integrable: the integration by parts in a single direction that every proof here is built on.

theorem TauCeti.integral_bilinear_fderiv_apply_comm {E : Type u_1} {V : Type u_2} {W : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] [NormedAddCommGroup W] [NormedSpace ℝ W] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → V} (B : V →L[ℝ] V →L[ℝ] W) (hu : ContDiff ℝ 2 u) (hsupp : HasCompactSupport u) (v w : E) : ∫ (x : E), (B ((fderiv ℝ u x) v)) ((fderiv ℝ u x) w) ∂μ = ∫ (x : E), (B ((fderiv ℝ u x) w)) ((fderiv ℝ u x) v) ∂μ

Exchanging the two differentiation directions does not change the integral of a continuous bilinear pairing of two directional derivatives of a compactly supported C² map.

theorem TauCeti.integral_bilinForm_fderiv_apply_comm {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → V} [FiniteDimensional ℝ V] (b : LinearMap.BilinForm ℝ V) (hu : ContDiff ℝ 2 u) (hsupp : HasCompactSupport u) (v w : E) : ∫ (x : E), (b ((fderiv ℝ u x) v)) ((fderiv ℝ u x) w) ∂μ = ∫ (x : E), (b ((fderiv ℝ u x) w)) ((fderiv ℝ u x) v) ∂μ

Exchanging the two differentiation directions does not change the integral of a bilinear form evaluated on two directional derivatives of a compactly supported C² map into a finite-dimensional space.

theorem TauCeti.integral_bilinForm_fderiv_apply_eq_zero_of_isAlt {E : Type u_1} {V : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] [FiniteDimensional ℝ E] [NormedAddCommGroup V] [NormedSpace ℝ V] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {u : E → V} [FiniteDimensional ℝ V] {b : LinearMap.BilinForm ℝ V} (hb : LinearMap.IsAlt b) (hu : ContDiff ℝ 2 u) (hsupp : HasCompactSupport u) (v w : E) : ∫ (x : E), (b ((fderiv ℝ u x) v)) ((fderiv ℝ u x) w) ∂μ = 0

The integral of an alternating bilinear form evaluated on two directional derivatives of a compactly supported C² map vanishes: the pullback of a constant two-form along a compactly supported map integrates to zero.