Compactly supported exact top forms on a vector space

A compactly supported C1 form has an integrable exterior derivative whose top-degree coefficient integrates to zero against the Haar measure of any basis. The coordinate proof uses the compact-support specialization of Mathlib's MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable, exported as MeasureTheory.integral_divergence_eq_zero: a bounding box contains the support, and compact support eliminates all its boundary faces.

Applied to a wedge φ ∧ ψ of real-valued forms, together with the Leibniz rule d (φ ∧ ψ) = dφ ∧ ψ + (-1) ^ k φ ∧ dψ, this is integration by parts for forms: when ψ has compact support, ∫ dφ ∧ ψ = -(-1) ^ k ∫ φ ∧ dψ (Module.Basis.integral_extDeriv_wedge_eq_integral_wedge_extDeriv).

The integral of a wedge ω ∧ η with η vanishing outside a set K is bounded by a constant depending only on the basis times sup ‖η‖ ∫_K ‖ω‖ (Module.Basis.exists_abs_integral_wedge_le).

theorem Module.Basis.integral_extDeriv_eq_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {n : ℕ} (b : Basis (Fin (n + 1)) ℝ E) {ω : E → E [⋀^Fin n]→L[ℝ] ℝ} (hω : ContDiff ℝ 1 ω) (hc : HasCompactSupport ω) : MeasureTheory.Integrable (fun (x : E) => (extDeriv ω x) ⇑b) b.addHaar ∧ ∫ (x : E), (extDeriv ω x) ⇑b ∂b.addHaar = 0

A compactly supported C1 form has an integrable exterior derivative, and the top-degree coefficient integrates to zero for every basis and its normalized Haar measure.

theorem Module.Basis.integral_extDeriv_wedge_eq_integral_wedge_extDeriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {k l N : ℕ} (b : Basis (Fin N) ℝ E) (hN : k + l + 1 = N) {φ : E → E [⋀^Fin k]→L[ℝ] ℝ} {ψ : E → E [⋀^Fin l]→L[ℝ] ℝ} (hφ : ContDiff ℝ 1 φ) (hψ : ContDiff ℝ 1 ψ) (hc : HasCompactSupport ψ) : ∫ (x : E), ((extDeriv φ x).wedge (ψ x)) (⇑b ∘ Fin.cast ⋯) ∂b.addHaar = -(-1) ^ k * ∫ (x : E), ((φ x).wedge (extDeriv ψ x)) (⇑b ∘ Fin.cast hN) ∂b.addHaar

Integration by parts for differential forms. For C1 real-valued forms φ of degree k and ψ of degree l on a space of dimension N = k + l + 1, with ψ compactly supported, ∫ dφ ∧ ψ = -(-1) ^ k ∫ φ ∧ dψ. The top-degree coefficients are taken on a basis b and integrated against its Haar measure; the degrees k + 1 + l and k + (l + 1) of the two wedges are identified with N by Fin.cast.

theorem Module.Basis.exists_abs_integral_wedge_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] {k l : ℕ} (b : Basis (Fin (k + l)) ℝ E) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ ⦃ω : E → E [⋀^Fin k]→L[ℝ] ℝ⦄ ⦃η : E → E [⋀^Fin l]→L[ℝ] ℝ⦄ ⦃K : Set E⦄ ⦃G : E → ℝ⦄ ⦃A : ℝ⦄, MeasurableSet K → (∀ x ∉ K, η x = 0) → MeasureTheory.IntegrableOn G K b.addHaar → (∀ x ∈ K, ‖ω x‖ ≤ G x) → (∀ (x : E), ‖η x‖ ≤ A) → |∫ (x : E), ((ω x).wedge (η x)) ⇑b ∂b.addHaar| ≤ C * (A * ∫ (x : E) in K, G x ∂b.addHaar)

The integral of the wedge of a form ω with a form η vanishing outside a set K is at most a constant depending only on the basis b times A ∫_K G, when ‖ω‖ ≤ G on K and ‖η‖ ≤ A.