Integrability of the applied derivative and of derivative energy densities

The derivative of a C¹ function with compact support is continuous and compactly supported, hence bounded. So along a strongly measurable family of points G, the derivative applied to an integrable family of vectors Z is integrable: it is dominated by a constant times ‖Z‖. No finiteness of the measure is needed.

Over any nontrivially normed field, squared norms of the derivative of a C¹ map in two given directions, and cutoff-weighted versions of them, are integrable when the map or the cutoff has compact support. A weighted squared defect c z * ‖fderiv w z e₁ + A z (fderiv w z e₂)‖ ^ 2 is integrable when it vanishes off a compact set on which c and A are continuous, so they need not be continuous elsewhere.

On a Euclidean product ℝ × V, the derivative of such a function in a fixed direction is also integrable on the product of a half-line with V.

Main results

• TauCeti.integrable_fderiv_apply: for f of class C¹ with compact support, an a.e. strongly measurable G and an integrable Z, the map x ↦ fderiv 𝕜 f (G x) (Z x) is integrable.
• TauCeti.integrable_fderiv_apply_of_tsupport_subset: the same when Z is only integrable after cutting off to the points x with G x in a set K containing the topological support of f.
• TauCeti.integrable_cutoff_fderiv_sq_mul_norm_sq, TauCeti.integrable_norm_fderiv_sq_add, TauCeti.integrable_cutoff_sq_mul_norm_fderiv_sq, TauCeti.integrable_mul_norm_defect_sq: integrability of the derivative energy densities in two directions.
• TauCeti.integrable_fderiv_apply_prod: the directional derivative of a compactly supported C¹ function on ℝ × V is integrable on the product of Ioi a with V.

theorem TauCeti.integrable_fderiv_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : E → F} (hf : ContDiff 𝕜 1 f) (hfc : HasCompactSupport f) {G : α → E} (hG : MeasureTheory.AEStronglyMeasurable G μ) {Z : α → E} (hZ : MeasureTheory.Integrable Z μ) : MeasureTheory.Integrable (fun (x : α) => (fderiv 𝕜 f (G x)) (Z x)) μ

The derivative of a C¹ compactly supported function, evaluated along an a.e. strongly measurable family of points G and applied to an integrable family of vectors Z, is integrable: it is bounded by a constant times ‖Z‖.

theorem TauCeti.integrable_fderiv_apply_of_tsupport_subset {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : E → F} (hf : ContDiff 𝕜 1 f) (hfc : HasCompactSupport f) {K : Set E} (hfK : tsupport f ⊆ K) {G : α → E} (hG : MeasureTheory.AEStronglyMeasurable G μ) {Z : α → E} (hZ : MeasureTheory.Integrable ({x : α | G x ∈ K}.indicator Z) μ) : MeasureTheory.Integrable (fun (x : α) => (fderiv 𝕜 f (G x)) (Z x)) μ

The derivative of a C¹ compactly supported function f, evaluated along an a.e. strongly measurable family of points G and applied to a family of vectors Z, is integrable as soon as Z is integrable after cutting off to the points x with G x ∈ K, for a set K containing the topological support of f: off K the derivative vanishes.

theorem TauCeti.integrable_cutoff_fderiv_sq_mul_norm_sq {E : Type u_2} [NormedAddCommGroup E] {F : Type u_3} [NormedAddCommGroup F] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] [NormedSpace ℝ E] {u : E → F} {χ : E → ℝ} (hu : Continuous u) (hχ : ContDiff ℝ 1 χ) (hc : HasCompactSupport χ) (e₁ e₂ : E) : MeasureTheory.Integrable (fun (z : E) => ((fderiv ℝ χ z) e₁ ^ 2 + (fderiv ℝ χ z) e₂ ^ 2) * ‖u z‖ ^ 2) μ

The cutoff-derivative error density of a C¹ cutoff with compact support is integrable against the squared norm of a continuous map.

theorem TauCeti.integrable_norm_fderiv_sq_add {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {w : E → F} (hw : ContDiff 𝕜 1 w) (hc : HasCompactSupport w) (e₁ e₂ : E) : MeasureTheory.Integrable (fun (z : E) => ‖(fderiv 𝕜 w z) e₁‖ ^ 2 + ‖(fderiv 𝕜 w z) e₂‖ ^ 2) μ

The derivative energy of a compactly supported C¹ map is integrable, in two directions.

theorem TauCeti.integrable_cutoff_sq_mul_norm_fderiv_sq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] {u : E → F} {χ : E → ℝ} (hu : ContDiff 𝕜 1 u) (hχ : Continuous χ) (hc : HasCompactSupport χ) (e₁ e₂ : E) : MeasureTheory.Integrable (fun (z : E) => χ z ^ 2 * (‖(fderiv 𝕜 u z) e₁‖ ^ 2 + ‖(fderiv 𝕜 u z) e₂‖ ^ 2)) μ

A cutoff-weighted derivative energy density of a C¹ map is integrable when the weight has compact support.

theorem TauCeti.integrable_mul_norm_defect_sq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [OpensMeasurableSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasureOnCompacts μ] (e₁ e₂ : E) {w : E → F} {c : E → ℝ} {A : E → F →L[𝕜] F} {S : Set E} (hw : ContDiff 𝕜 1 w) (hc : ContinuousOn c S) (hS : IsCompact S) (hA : ContinuousOn A S) (hsub : (Function.support fun (z : E) => c z * ‖(fderiv 𝕜 w z) e₁ + (A z) ((fderiv 𝕜 w z) e₂)‖ ^ 2) ⊆ S) : MeasureTheory.Integrable (fun (z : E) => c z * ‖(fderiv 𝕜 w z) e₁ + (A z) ((fderiv 𝕜 w z) e₂)‖ ^ 2) μ

A weighted squared defect c z * ‖fderiv 𝕜 w z e₁ + A z (fderiv 𝕜 w z e₂)‖ ^ 2 of a C¹ map is integrable once it vanishes off a compact set on which the coefficients are continuous.

theorem TauCeti.integrable_fderiv_apply_prod {V : Type u_4} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] [MeasurableSpace V] [BorelSpace V] {g : WithLp 2 (ℝ × V) → ℝ} (hg : ContDiff ℝ 1 g) (hgc : HasCompactSupport g) (a : ℝ) (d : WithLp 2 (ℝ × V)) : MeasureTheory.Integrable (fun (z : ℝ × V) => (fderiv ℝ g (WithLp.toLp 2 z)) d) ((MeasureTheory.volume.restrict (Set.Ioi a)).prod MeasureTheory.volume)

The directional derivative of a compactly supported C¹ function is integrable on the product of Ioi a with V.