Weak derivatives and space-time mollification

The distributional identities in def:sws commute with local space-time mollification on compact subsets of the domain.

theorem CKN.instIsAddHaarMeasureProdVec3RealVolume_1 : MeasureTheory.volume.IsAddHaarMeasure

theorem CKN.spaceTimeMollify_fderiv_eq_of_local_weak {U : Set (Foundation.Parabolic.Vec3 × ℝ)} {u g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {v : Foundation.Parabolic.Vec3 × ℝ} (hU : IsOpen U) (hu : MeasureTheory.LocallyIntegrableOn u U MeasureTheory.volume) (hg : MeasureTheory.LocallyIntegrableOn g U MeasureTheory.volume) {δ : ℝ} (hδ : 0 < δ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall z (3 * δ) ⊆ U) (hweak : ∀ (φ : Foundation.Parabolic.Vec3 × ℝ → ℝ), ContDiff ℝ (↑⊤) φ → HasCompactSupport φ → tsupport φ ⊆ Metric.closedBall z (3 * δ) → ∫ (y : Foundation.Parabolic.Vec3 × ℝ) in U, u y * (fderiv ℝ φ y) v = -∫ (y : Foundation.Parabolic.Vec3 × ℝ) in U, g y * φ y) : HasFDerivAt (spaceTimeMollify u δ hδ) (fderiv ℝ (spaceTimeMollify u δ hδ) z) z ∧ (fderiv ℝ (spaceTimeMollify u δ hδ) z) v = spaceTimeMollify g δ hδ z

A local weak derivative identity determines the derivative of a mollification at points whose kernel support stays inside the domain. This is used for the local energy identity in lem:caccioppoli.

theorem CKN.continuous_hasCompactSupport_nnnorm_bound {X : Type u_1} [PseudoMetricSpace X] [Nonempty X] {f : X → ℝ} (hf : Continuous f) (hfc : HasCompactSupport f) : ∃ (C : NNReal), ∀ (x : X), ‖f x‖₊ ≤ C

A continuous compactly supported real function is bounded. This supplies bounded weights for the weighted pairing limits in lem:caccioppoli.

theorem CKN.memLp_mul_left_of_nnnorm_bound {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {f g : X → ℝ} {C : NNReal} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.MemLp g 2 μ) (hC : ∀ᵐ (x : X) ∂μ, ‖f x‖₊ ≤ C) : MeasureTheory.MemLp (fun (x : X) => f x * g x) 2 μ

Multiplication by a bounded measurable scalar preserves L² membership.

theorem CKN.tendsto_toLp_mul_left_of_nnnorm_bound {X : Type u_1} [MeasurableSpace X] {μ : MeasureTheory.Measure X} {φ : X → ℝ} {f : ℕ → X → ℝ} {g : X → ℝ} {C : NNReal} (hφ : MeasureTheory.AEStronglyMeasurable φ μ) (hC : ∀ (x : X), ‖φ x‖₊ ≤ C) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (x : X) => φ x * f n x) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (fun (x : X) => φ x * g x) ⋯))

Multiplication by a bounded measurable scalar preserves strong L² convergence. This is used to pass weighted energy pairings to the limit in lem:caccioppoli.

theorem CKN.spaceTimeMollify_weak_derivatives {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) {δ : ℝ} (hδ : 0 < δ) {z : Foundation.Parabolic.Vec3 × ℝ} (hz : Metric.closedBall z (4 * δ) ⊆ Ω ×ˢ I) : (∀ (i j : Fin 3), spatialPartial (have this := fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q; this) j z = spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => Dw (Foundation.Parabolic.parabolicHomeomorph.symm y) i j) δ hδ z) ∧ (∀ (i j k : Fin 3), spatialSecondPartial (have this := fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q; this) j k z = spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => D2w (Foundation.Parabolic.parabolicHomeomorph.symm y) i j k) δ hδ z) ∧ ∀ (i : Fin 3), timePartial (have this := fun (q : Foundation.Parabolic.ParabolicPoint) => spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => w (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ q; this) z = spaceTimeMollify (fun (y : Foundation.Parabolic.Vec3 × ℝ) => Dtw (Foundation.Parabolic.parabolicHomeomorph.symm y) i) δ hδ z

Mollification commutes componentwise with the spatial, second spatial, and time weak derivatives on compact subsets of an open space-time domain (manuscript def:sws).

theorem CKN.weak_time_derivative_sq {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) (hI : IsOpen I) {w : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Dw : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {D2w : Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → Foundation.Parabolic.Vec3} {Dtw : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hderiv : HasSpaceTimeWeakDerivs Ω I w Dw D2w Dtw) (hL2w : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (q : Foundation.Parabolic.Vec3 × ℝ) => (spaceTimeSet Ω I).indicator w (Foundation.Parabolic.parabolicHomeomorph.symm q) i) 2 MeasureTheory.volume) (hL2time : ∀ (i : Fin 3), MeasureTheory.MemLp (fun (q : Foundation.Parabolic.Vec3 × ℝ) => (spaceTimeSet Ω I).indicator Dtw (Foundation.Parabolic.parabolicHomeomorph.symm q) i) 2 MeasureTheory.volume) {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) {δ₀ : ℝ} (hδ₀ : 0 < δ₀) (hbuffer : ∀ q ∈ tsupport φ, Metric.closedBall q (4 * δ₀) ⊆ Ω ×ˢ I) : ∑ i : Fin 3, ∫ (q : Foundation.Parabolic.Vec3 × ℝ), (spaceTimeSet Ω I).indicator w (Foundation.Parabolic.parabolicHomeomorph.symm q) i ^ 2 * (fderiv ℝ φ q) (0, 1) = -(2 * ∑ i : Fin 3, ∫ (q : Foundation.Parabolic.Vec3 × ℝ), (spaceTimeSet Ω I).indicator w (Foundation.Parabolic.parabolicHomeomorph.symm q) i * (spaceTimeSet Ω I).indicator Dtw (Foundation.Parabolic.parabolicHomeomorph.symm q) i * φ q)

The square of a locally square-integrable weak solution has the expected weak time derivative on compactly supported tests (manuscript def:sws). The formula is written as the finite sum of scalar pairings; u and g are the zero extensions of w and Dtw. The buffer condition keeps every mollification kernel inside the weak-derivative domain.