Smooth multiplication of test forms and the Leibniz rule for currents

For an open set Ω of a real normed space E, a smooth function f : E → ℝ acts on test functions on Ω by pointwise multiplication, and a smooth covector field α : E → E →L[ℝ] ℝ acts on test k-forms by the wedge product ω ↦ α ∧ ω, with values in test (k + 1)-forms. Both are continuous linear maps for the LF topology, built from Mathlib's TestFunction.bilinLeftCLM. They do not enlarge supports and commute with extension of test functions to a larger open set.

The exterior derivative satisfies the Leibniz rule d (f ω) = df ∧ ω + f dω on test forms. Transposing, for a current T (a continuous linear functional on test (k + 1)-forms), the current fT = T ∘ (f ·) has boundary ∂(fT) = f ∂T - T ⌞ df, where ∂T = T ∘ d and (T ⌞ df) ω = T (df ∧ ω).

The wedge α ∧ ω with a one-form is the alternatization of v ↦ α v • ω, the operation through which Mathlib's extDeriv is defined, so that it lands in degree k + 1 like the exterior derivative. ContinuousAlternatingMap.alternatizeUncurryFin_smulRight_apply identifies it with the paired wedge ContinuousAlternatingMap.pairedWedge of the one-form α with ω.

Main declarations

• TestFunction.smulLeftCLM: multiplication φ ↦ f φ of test functions by a smooth function.
• TestFunction.exists_coe_eq_clm_apply_of_tsupport_inter_subset: the pairing x ↦ A x (φ x) of a test function on Ω' with a smooth operator field is a test function on any open Ω containing tsupport A ∩ Ω'.
• TestFunction.oneFormWedgeCLM: the wedge ω ↦ α ∧ ω of test forms with a smooth one-form.
• TestFunction.norm_oneFormWedgeCLM_apply_le: the pointwise bound ‖(α ∧ ω) x‖ ≤ (k + 1) ‖α x‖ ‖ω x‖, with its extended-norm form TestFunction.enorm_oneFormWedgeCLM_apply_le.
• TestFunction.extDerivCLM_smulLeftCLM: the Leibniz rule d (f ω) = df ∧ ω + f dω.
• ContinuousLinearMap.comp_smulLeftCLM_comp_extDerivCLM: the boundary of a smooth multiple of a current, ∂(fT) = f ∂T - T ⌞ df.
• ContDiffMapSupportedIn.seminorm_bilinLeftCLM_mul_le: the Leibniz bound N_i(χ g) ≤ 2 ^ k N_k(χ) M for the product of a complex smooth function χ supported in a compact set with a smooth function g whose derivatives of order at most k are bounded by M.

References

• H. Federer, Geometric Measure Theory, §4.1.7.
• L. Simon, Introduction to Geometric Measure Theory, Chapter 6.

noncomputable def TestFunction.smulLeftCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ (↑n) f) : TestFunction Ω F n →L[ℝ] TestFunction Ω F n

Multiplication of test functions on Ω by a C^n real function f, as a continuous linear map φ ↦ f φ.

@[simp]

theorem TestFunction.smulLeftCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ (↑n) f) (φ : TestFunction Ω F n) (x : E) : ((smulLeftCLM hf) φ) x = f x • φ x

theorem TestFunction.coe_smulLeftCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ (↑n) f) (φ : TestFunction Ω F n) : ⇑((smulLeftCLM hf) φ) = f • ⇑φ

A smooth multiple of a test function, as a function, is the pointwise product.

theorem TestFunction.tsupport_smulLeftCLM_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ (↑n) f) (φ : TestFunction Ω F n) : tsupport ⇑((smulLeftCLM hf) φ) ⊆ tsupport f ∩ tsupport ⇑φ

Multiplying by a smooth function does not enlarge the support of a test function.

@[simp]

theorem TestFunction.smulLeftCLM_smulLeftCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {f g : E → ℝ} (hf : ContDiff ℝ (↑n) f) (hg : ContDiff ℝ (↑n) g) (φ : TestFunction Ω F n) : (smulLeftCLM hf) ((smulLeftCLM hg) φ) = (smulLeftCLM ⋯) φ

Multiplying by two smooth functions in turn is multiplying by their product.

@[simp]

theorem TestFunction.smulLeftCLM_monoCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω Ω' : TopologicalSpace.Opens E} {n : ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ (↑n) f) (φ : TestFunction Ω' F n) : (smulLeftCLM hf) ((monoCLM ℝ) φ) = (monoCLM ℝ) ((smulLeftCLM hf) φ)

Multiplication by a smooth function commutes with extending test functions from Ω' to Ω.

theorem TestFunction.exists_coe_eq_clm_apply_of_tsupport_inter_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω Ω' : TopologicalSpace.Opens E} {n : ℕ∞} {G : Type u_3} [NormedAddCommGroup G] [NormedSpace ℝ G] {A : E → F →L[ℝ] G} (hA : ContDiff ℝ (↑n) A) (h : tsupport A ∩ ↑Ω' ⊆ ↑Ω) (φ : TestFunction Ω' F n) : ∃ (ψ : TestFunction Ω G n), ⇑ψ = fun (x : E) => (A x) (φ x)

Pairing a test function with a C^n operator field from a smaller open set. If A : E → F →L[ℝ] G is C^n with tsupport A ∩ Ω' ⊆ Ω and φ is a C^n test function on Ω', then x ↦ A x (φ x) is a C^n test function on Ω, whether or not Ω' ≤ Ω. This covers a scalar multiple f φ (take A x = f x • id) and the pairing Df φ with a derivative.

noncomputable def TestFunction.oneFormWedgeCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) n →L[ℝ] TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) n

The wedge α ∧ ω of a test k-form ω on Ω with a C^n one-form α, as a continuous linear map into test (k + 1)-forms. Pointwise, α ∧ ω is the alternatization of v ↦ α v • ω, see TestFunction.oneFormWedgeCLM_apply.

@[simp]

theorem TestFunction.oneFormWedgeCLM_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) n) (x : E) : ((oneFormWedgeCLM hα) ω) x = ContinuousAlternatingMap.alternatizeUncurryFin ((α x).smulRight (ω x))

theorem TestFunction.norm_oneFormWedgeCLM_apply_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) n) (x : E) : ‖((oneFormWedgeCLM hα) ω) x‖ ≤ (↑k + 1) * ‖α x‖ * ‖ω x‖

Pointwise, the wedge α ∧ ω is bounded in operator norm by (k + 1) ‖α x‖ ‖ω x‖.

theorem TestFunction.enorm_oneFormWedgeCLM_apply_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) n) (x : E) : ‖((oneFormWedgeCLM hα) ω) x‖ₑ ≤ (↑k + 1) * ‖α x‖ₑ * ‖ω x‖ₑ

The pointwise bound ‖(α ∧ ω) x‖ₑ ≤ (k + 1) ‖α x‖ₑ ‖ω x‖ₑ in extended norms.

theorem TestFunction.tsupport_oneFormWedgeCLM_subset {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) n) : tsupport ⇑((oneFormWedgeCLM hα) ω) ⊆ tsupport α ∩ tsupport ⇑ω

The wedge with a smooth one-form does not enlarge the support of a test form.

@[simp]

theorem TestFunction.oneFormWedgeCLM_monoCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω Ω' : TopologicalSpace.Opens E} {n : ℕ∞} {k : ℕ} {α : E → E →L[ℝ] ℝ} (hα : ContDiff ℝ (↑n) α) (ω : TestFunction Ω' (E [⋀^Fin k]→L[ℝ] F) n) : (oneFormWedgeCLM hα) ((monoCLM ℝ) ω) = (monoCLM ℝ) ((oneFormWedgeCLM hα) ω)

The wedge with a smooth one-form commutes with extending test forms from Ω' to Ω.

theorem TestFunction.extDerivCLM_smulLeftCLM {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} {k : ℕ} {f : E → ℝ} (hf : ContDiff ℝ (↑⊤) f) (ω : TestFunction Ω (E [⋀^Fin k]→L[ℝ] F) ⊤) : extDerivCLM ((smulLeftCLM hf) ω) = (oneFormWedgeCLM ⋯) ω + (smulLeftCLM hf) (extDerivCLM ω)

The Leibniz rule for test forms: d (f ω) = df ∧ ω + f dω for a smooth function f.

theorem ContinuousLinearMap.comp_smulLeftCLM_comp_extDerivCLM {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [AddCommGroup G] [Module ℝ G] [TopologicalSpace G] [IsTopologicalAddGroup G] {Ω : TopologicalSpace.Opens E} {k : ℕ} {f : E → ℝ} (T : TestFunction Ω (E [⋀^Fin (k + 1)]→L[ℝ] F) ⊤ →L[ℝ] G) (hf : ContDiff ℝ (↑⊤) f) : (T ∘SL TestFunction.smulLeftCLM hf) ∘SL TestFunction.extDerivCLM = (T ∘SL TestFunction.extDerivCLM) ∘SL TestFunction.smulLeftCLM hf - T ∘SL TestFunction.oneFormWedgeCLM ⋯

The boundary of a smooth multiple of a current: for a continuous linear functional T on test (k + 1)-forms and a smooth function f, ∂(fT) = f ∂T - T ⌞ df. Here fT = T ∘ (f ·), the boundary is ∂T = T ∘ d, and (T ⌞ df) ω = T (df ∧ ω).

theorem ContDiffMapSupportedIn.seminorm_bilinLeftCLM_mul_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {K : TopologicalSpace.Compacts E} (χ : ContDiffMapSupportedIn E ℂ ⊤ K) {g : E → ℂ} (hg : ContDiff ℝ (↑⊤) g) {k : ℕ} {M : ℝ} (hM : ∀ j ≤ k, ∀ (x : E), ‖iteratedFDeriv ℝ j g x‖ ≤ M) {i : ℕ} (hi : i ≤ k) : (ContDiffMapSupportedIn.seminorm ℂ E ℂ ⊤ K i) ((bilinLeftCLM (ContinuousLinearMap.mul ℂ ℂ) hg) χ) ≤ 2 ^ k * (ContDiffMapSupportedIn.supSeminorm ℂ E ℂ ⊤ K k) χ * M

The C^i seminorms, i ≤ k, of χ g are bounded by 2 ^ k N_k(χ) M when M bounds the derivatives of g of order at most k.