Data for the centred source correction on the half-gap collar #
Joint measurability of the velocity, its gradient, the force and the spatial slice mean; the divergence source's Morrey budget on any carrier inside the outer cylinder; and the gradient-shaped budget for the mean-free velocity.
theorem
CKN.Core.Step4.originASlot_unit_box_data
{Ω : Set Foundation.Parabolic.Vec3}
{I : 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)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
{S : Set Foundation.Parabolic.ParabolicPoint}
(hS : S ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1)
:
(∀ (i : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => u w i) (MeasureTheory.volume.restrict S)) ∧ (∀ (i j : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Du w i j) (MeasureTheory.volume.restrict S)) ∧ ∀ (i : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => f w i) (MeasureTheory.volume.restrict S)
Component measurability of the data on any subset of the unit cylinder.
theorem
CKN.Core.Step4.originASlot_slice_mean_aemeasurable
{Ω : Set Foundation.Parabolic.Vec3}
{I : 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)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(A : Set Foundation.Parabolic.Vec3)
(i : Fin 3)
:
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => sourceSliceCentredMean z.1 ρ u w.2 i)
(MeasureTheory.volume.restrict (A ×ˢ Set.Ioc (z.2 - ρ ^ 2) z.2))
The slice mean is jointly measurable on every product carrier over the collar time window.
theorem
CKN.Core.Step4.morreyNorm_indicator_component_le_vector
{p κ : ℝ}
(hp : 0 ≤ p)
(S : Set Foundation.Parabolic.ParabolicPoint)
(G : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(j : Fin 3)
:
Foundation.Parabolic.Morrey.morreyNorm p κ (S.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => G w j) ≤ Foundation.Parabolic.Morrey.morreyNorm p κ fun (w : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (S.indicator G w)
A component of an indicator vector field is below the indicator norm.
theorem
CKN.Core.Step4.originASlot_divergence_source_morreyNorm_le
(q τ R₀ ε : ℝ)
(KU KD : ENNReal)
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hR₀ : 0 < R₀)
(hR₀le : R₀ ≤ 1)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{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)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hU :
∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i) ≤ KU)
(hD :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
Du z i j) ≤ KD)
(hsize :
∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z)) ^ 3 + ENNReal.ofReal |p z| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z)) ^ q ≤ ENNReal.ofReal ε)
{S : Set Foundation.Parabolic.ParabolicPoint}
(hS : S ⊆ Foundation.Parabolic.parabolicCylinder 0 0 R₀)
(j : Fin 3)
:
The divergence source on any carrier inside the outer cylinder has the established affine Morrey budget.
theorem
CKN.Core.Step4.originASlot_gradient_mass_le
{R₀ ρ : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(hρ : 0 < ρ)
{KD : ENNReal}
(k : Fin 3)
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hcyl : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 R₀)
(hDm :
∀ (l : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w k l)
MeasureTheory.volume)
(hD :
∀ (l : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w k l) ≤ KD)
:
Foundation.Parabolic.Morrey.cylinderPowerIntegral 2 (fun (w : Foundation.Parabolic.ParabolicPoint) => ‖Du w k‖) z ρ ≤ ENNReal.ofReal ρ ^ (5 * (1 - 2 / (25 / 8))) * (3 * KD) ^ 2
The collar gradient mass is controlled by the gradient Morrey budget.
theorem
CKN.Core.Step4.originASlot_meanFree_morreyNorm_le_gradient_budget
{R₀ ρ : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(hρ : 0 < ρ)
(hρ1 : ρ ≤ 1)
{KD : ENNReal}
(k : Fin 3)
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hpoin :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j - sourceSliceCentredMean z.1 ρ u s j) 6
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)) ≤ sobolevPoincareL6Constant * MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) j) 2
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hmeas :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable
(fun (y : Foundation.Parabolic.Vec3) => u (y, s) k - sourceSliceCentredMean z.1 ρ u s k)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hGm :
AEMeasurable
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w k - sourceSliceCentredMean z.1 ρ u w.2 k)
MeasureTheory.volume)
(hDnorm :
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => ‖Du w k‖)
(MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ)))
(hDsl :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => Du (y, t) k)
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 ρ)))
(hcyl : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 R₀)
(hDm :
∀ (l : Fin 3),
AEMeasurable
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w k l)
MeasureTheory.volume)
(hD :
∀ (l : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w k l) ≤ KD)
:
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w k - sourceSliceCentredMean z.1 ρ u w.2 k) ≤ ENNReal.ofReal (Real.pi * 4 / 3) ^ (1 / 3) * sobolevPoincareL6Constant * (3 * KD)
The mean-free factor carries the gradient budget, with an absolute coefficient.
theorem
CKN.Core.Step4.originASlot_correction_aemeasurable
{R₀ ρ : ℝ}
{z : Foundation.Parabolic.ParabolicPoint}
(hρ : 0 < ρ)
{S : Set Foundation.Parabolic.ParabolicPoint}
{u f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hSm : MeasurableSet S)
(hu :
∀ (i : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => u w i) (MeasureTheory.volume.restrict S))
(hDu :
∀ (i j : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => Du w i j) (MeasureTheory.volume.restrict S))
(hf :
∀ (i : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => f w i) (MeasureTheory.volume.restrict S))
(hc :
∀ (i : Fin 3),
AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => sourceSliceCentredMean z.1 ρ u w.2 i)
(MeasureTheory.volume.restrict S))
(j : Fin 3)
:
AEMeasurable
(S.indicator fun (v : Foundation.Parabolic.ParabolicPoint) =>
centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) (fun (y : Foundation.Parabolic.Vec3) => u (y, v.2))
(fun (y : Foundation.Parabolic.Vec3) => f (y, v.2)) (fun (y : Foundation.Parabolic.Vec3) => Du (y, v.2))
(sourceSliceCentredMean z.1 ρ u v.2) j v.1)
MeasureTheory.volume
The carrier-restricted centred correction is jointly measurable.