Pushforward of compactly supported currents along smooth maps

Let Ω ⊆ E and Ω' ⊆ E' be open subsets of real normed spaces, with E finite-dimensional, and let T be a current on Ω: a continuous linear map on test k-forms. Pushing T forward along a map Φ : E → E' by Φ_# T = T ∘ Φ^* needs the pullback Φ^* ω of a test form on Ω' to be a test form on Ω, which holds when Φ is proper from Ω to Ω' (TestFunction.pullbackCLM). When the support of T is a compact subset of Ω, properness is not needed: choose a test function χ on Ω equal to one near the support of T (TestFunction.exists_eventually_eq_one) and put

Φ_# T = T ∘ (χ Φ^*),

where χ Φ^* is the pullback with cutoff TestFunction.cutoffPullbackCLM, defined for every map Φ smooth on Ω. This file proves:

• Φ_# T does not depend on the cutoff: only the germ of χ along the support of T matters;
• when Φ is proper, Φ_# T is the pushforward T ∘ Φ^*;
• ∂ (Φ_# T) = Φ_# (∂ T), where ∂ T = T ∘ d;
• the support of Φ_# T lies in the image under Φ of the support of T;
• if |χ| ≤ 1 and ‖DΦ‖ ≤ L on the support of χ, then M(Φ_# T) ≤ L ^ k M(T);
• functoriality: (Ψ ∘ Φ)_# T = Ψ_# (Φ_# T).

Main declarations

• ContinuousLinearMap.comp_cutoffPullbackCLM_congr: independence of the cutoff.
• ContinuousLinearMap.comp_cutoffPullbackCLM_eq_comp_pullbackCLM: agreement with the pushforward along a proper map.
• ContinuousLinearMap.comp_cutoffPullbackCLM_comp_extDerivCLM: ∂ (Φ_# T) = Φ_# (∂ T).
• ContinuousLinearMap.comp_cutoffPullbackCLM_comp_cutoffPullbackCLM: functoriality.
• Distribution.dsupport_comp_cutoffPullbackCLM_subset: spt (Φ_# T) ⊆ Φ (tsupport χ ∩ spt T).
• Distribution.mass_comp_cutoffPullbackCLM_le: M(Φ_# T) ≤ L ^ k M(T).

References

• H. Federer, Geometric Measure Theory, §4.1.7 (the pushforward of a current whose support is compact, defined with a cutoff).
• L. Simon, Introduction to Geometric Measure Theory, Chapter 6, §2.

theorem ContinuousLinearMap.comp_cutoffPullbackCLM_congr {E : Type u_1} {E' : Type u_2} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Φ : E → E'} {k : ℕ} {χ₁ χ₂ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} (T : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤ →L[ℝ] G) (h : ⇑χ₁ =ᶠ[nhdsSet (Distribution.dsupport ⇑T)] ⇑χ₂) : T ∘SL χ₁.cutoffPullbackCLM Φ hΦ = T ∘SL χ₂.cutoffPullbackCLM Φ hΦ

Independence of the cutoff: the pushforward T ∘ (χ Φ^*) of a current T depends only on the germ of χ along the support of T.

theorem ContinuousLinearMap.comp_cutoffPullbackCLM_eq_comp_pullbackCLM {E : Type u_1} {E' : Type u_2} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Φ : E → E'} {k : ℕ} {χ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} (T : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤ →L[ℝ] G) (hχ : ∀ᶠ (x : E) in nhdsSet (Distribution.dsupport ⇑T), χ x = 1) (hΦp : ∀ (K : Set E'), IsCompact K → K ⊆ ↑Ω' → IsCompact (↑Ω ∩ Φ ⁻¹' K)) : T ∘SL χ.cutoffPullbackCLM Φ hΦ = T ∘SL TestFunction.pullbackCLM Φ hΦ hΦp

Agreement with the proper pushforward: if Φ is proper from Ω to Ω' and χ is equal to one near the support of T, then T ∘ (χ Φ^*) = T ∘ Φ^*.

theorem ContinuousLinearMap.comp_cutoffPullbackCLM_comp_extDerivCLM {E : Type u_1} {E' : Type u_2} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Φ : E → E'} {k : ℕ} {χ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} (T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤ →L[ℝ] G) (hχ : ∀ᶠ (x : E) in nhdsSet (Distribution.dsupport ⇑T), χ x = 1) : (T ∘SL χ.cutoffPullbackCLM Φ hΦ) ∘SL TestFunction.extDerivCLM = (T ∘SL TestFunction.extDerivCLM) ∘SL χ.cutoffPullbackCLM Φ hΦ

The pushforward commutes with the boundary: if χ is equal to one near the support of a current T on test (k + 1)-forms, then ∂ (T ∘ (χ Φ^*)) = (∂ T) ∘ (χ Φ^*), where ∂ T = T ∘ d. The support of ∂ T lies in that of T, so the right-hand side is the pushforward of ∂ T.

theorem ContinuousLinearMap.comp_cutoffPullbackCLM_comp_cutoffPullbackCLM {E : Type u_1} {E' : Type u_2} {E'' : Type u_3} {F : Type u_4} {G : Type u_5} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup E''] [NormedSpace ℝ E''] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Ω'' : TopologicalSpace.Opens E''} {Φ : E → E'} {k : ℕ} {χ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} (T : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤ →L[ℝ] G) {Ψ : E' → E''} {χ' : TestFunction Ω' ℝ ⊤} {hΨ : ContDiffOn ℝ (↑⊤) Ψ ↑Ω'} {hΨΦ : ContDiffOn ℝ (↑⊤) (Ψ ∘ Φ) ↑Ω} (hχ : ∀ᶠ (x : E) in nhdsSet (Distribution.dsupport ⇑T), χ x = 1) (hχ' : ∀ᶠ (y : E') in nhdsSet (Φ '' Distribution.dsupport ⇑T), χ' y = 1) : (T ∘SL χ.cutoffPullbackCLM Φ hΦ) ∘SL χ'.cutoffPullbackCLM Ψ hΨ = T ∘SL χ.cutoffPullbackCLM (Ψ ∘ Φ) hΨΦ

Functoriality of the pushforward: (Ψ ∘ Φ)_# T = Ψ_# (Φ_# T), when χ is equal to one near the support of T and χ' is equal to one near its image under Φ.

theorem Distribution.dsupport_comp_cutoffPullbackCLM_subset {E : Type u_1} {E' : Type u_2} {F : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Φ : E → E'} {k : ℕ} {χ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} {𝓕 : Type u_5} [FiniteDimensional ℝ E] [AddCommMonoid V] [FunLike 𝓕 (TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) V] [AddMonoidHomClass 𝓕 (TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) V] (T : 𝓕) : dsupport (⇑T ∘ ⇑(χ.cutoffPullbackCLM Φ hΦ)) ⊆ Φ '' (tsupport ⇑χ ∩ dsupport ⇑T)

The support of a pushforward: the support of T ∘ (χ Φ^*) lies in the image under Φ of the part of the support of T in the support of χ. In particular it is compact, and when χ is equal to one near the support of T, it lies in the image of the support of T.

theorem Distribution.mass_comp_cutoffPullbackCLM_le {E : Type u_1} {E' : Type u_2} {F : Type u_3} {V : Type u_4} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup E'] [NormedSpace ℝ E'] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {Ω' : TopologicalSpace.Opens E'} {Φ : E → E'} {k : ℕ} {χ : TestFunction Ω ℝ ⊤} {hΦ : ContDiffOn ℝ (↑⊤) Φ ↑Ω} {𝓕 : Type u_5} [NormedAddCommGroup V] [NormedSpace ℝ V] [FunLike 𝓕 (TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) V] [LinearMapClass 𝓕 ℝ (TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) V] (T : 𝓕) (hχ : ∀ (x : E), |χ x| ≤ 1) {L : NNReal} (hL : ∀ x ∈ tsupport ⇑χ, ‖fderiv ℝ Φ x‖ ≤ ↑L) : mass (⇑T ∘ ⇑(χ.cutoffPullbackCLM Φ hΦ)) ≤ ↑L ^ k * mass ⇑T

The mass of a pushforward: if |χ| ≤ 1 and ‖DΦ‖ ≤ L on the support of χ, then the pushforward T ∘ (χ Φ^*) of a k-current T has mass at most L ^ k times the mass of T.