Measurability of time-dependent force potentials

Spatial integration against a measurable kernel preserves measurability of the potential norm in time. This applies to the force-growth constants in eq:pressure-gradient-morrey without assuming temporal regularity.

The harmonic force bound on interior time boxes

The force term in eq:pressure-gradient-morrey is controlled almost everywhere by its measurable fixed-radius envelope on any local time box.

Time integrability of the harmonic force envelope

The fixed-radius force contribution in eq:pressure-gradient-morrey has a measurable, finite, locally time-integrable norm envelope from def:sws.

theorem CKN.Core.Step4.origin_newtonian_coefficients_lt_top {R : ℝ} (hR : 0 < R) : originNewtonianCoefficient R < ⊤ ∧ ∀ (i : Fin 3), originNewtonianDerivativeCoefficient R i < ⊤

The fixed-radius Newtonian coefficients are finite.

theorem CKN.Core.Step4.origin_force_envelope_obligations_on_local_box {Ω : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} {q R : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hR : 0 < R) (hbox : localBox Ω I (Foundation.Parabolic.vec3Ball 0 R) J) : AEMeasurable (originForceGrowthEnvelope R f) (MeasureTheory.volume.restrict J) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, originForceGrowthEnvelope R f s ≠ ⊤) ∧ MeasureTheory.Integrable (fun (s : ℝ) => (originForceGrowthEnvelope R f s).toReal) (MeasureTheory.volume.restrict J)

Suitability gives the force envelope's measurability, a.e. finiteness, and time integrability on any interior origin ball-times-window box.

theorem CKN.Core.Step4.origin_force_components_memLp_ae_on_local_box {Ω B : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hbox : localBox Ω I B J) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (j : Fin 3), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B)

The force components lie in spatial L^{6/5} almost everywhere on an arbitrary suitable-solution local box.

theorem CKN.Core.Step4.origin_harmonic_force_le_envelope_on_local_box {Ω : Set Foundation.Parabolic.Vec3} {I J : Set ℝ} {q R : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hR : 0 < R) (hbox : localBox Ω I (Foundation.Parabolic.vec3Ball 0 R) J) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ENNReal.ofReal (harmonicRemainderForceBound (0, 0) hR f s) ≤ originForceGrowthEnvelope R f s

The actual harmonic force constant is bounded a.e. by the force envelope on any interior origin ball-times-window box.

theorem CKN.Core.Step4.origin_convolution_norm_time_aemeasurable {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {J : Set ℝ} {k : Foundation.Parabolic.Vec3 → ℝ} (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))) (hk : Measurable k) {P : ℝ} (hP : 0 < P) (B : Set Foundation.Parabolic.Vec3) : AEMeasurable (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => ∫ (y : Foundation.Parabolic.Vec3), k (x - y) * G (y, s)) (ENNReal.ofReal P) (MeasureTheory.volume.restrict B)) (MeasureTheory.volume.restrict J)

The spatial norm of a time-dependent convolution is measurable in time.

theorem CKN.Core.Step4.origin_force_growth_constants_time_aemeasurable {G : Foundation.Parabolic.Vec3 × ℝ → ℝ} {J : Set ℝ} (hG : MeasureTheory.AEStronglyMeasurable G (MeasureTheory.volume.prod (MeasureTheory.volume.restrict J))) (R : ℝ) : AEMeasurable (fun (s : ℝ) => Foundation.Euclidean.newtonianPotentialGrowthConstant (fun (y : Foundation.Parabolic.Vec3) => G (y, s)) R) (MeasureTheory.volume.restrict J) ∧ ∀ (i : Fin 3), AEMeasurable (fun (s : ℝ) => Foundation.Euclidean.newtonianDerivativePotentialGrowthConstant i (fun (y : Foundation.Parabolic.Vec3) => G (y, s)) R) (MeasureTheory.volume.restrict J)

Both Newtonian force-growth constants are measurable functions of time for a jointly measurable source supported on the full spatial space.