The actual pressure mass from measurable envelopes #
Harmonic and force slice masses are dominated by measurable envelopes. Only the final centred-source correction needs a mass bound without any joint measurability assumption.
The absolute coefficients of the far-force increment #
On a clipped cell the prescribed spatial pressure gradient of prop:bootstrap
splits into a Riesz field driven by the localized divergence source, the
gradient of the harmonic pressure part, the gradient of the second force
potential p₈ of eq:pk, and a Riesz field driven by the centred source
correction. This file fixes the absolute coefficients that the third summand
costs.
Display (3.5) bounds the classical gradient of p₈,η on the inner ball of a
collar of radius ρ by the L¹ size of the force on that collar, with the
coefficient 400·c·cutoffGradientConstant·ρ⁻³, in which the numeral
400 = (3/20)⁻² is the separation of lem:cutoff. At the collar radii
(R₀ − R₁)/2 of the two parameter triples of prop:bootstrap the scale
factor ρ⁻³ is at most 128³, and the cell volume contributes one further
factor 4π/3 ≤ 5. The three constants recorded here are the scale-free part
of that coefficient, its collar-uniform value, and the Calderón–Zygmund
threshold at which the affine slot pays for the increment.
The absolute coefficients #
The scale-free part of the far-force gradient coefficient of display (3.5):
the numeral 400 = (3/20)⁻² of the separation of lem:cutoff, the order-one
constant of eq:har-Ck, and the cutoff gradient constant.
Equations
Instances For
The far-force gradient coefficient at collar radii at least 1/128, where
the scale factor ρ⁻³ of display (3.5) is at most 128³.
Equations
Instances For
The absolute Calderón–Zygmund threshold at which the affine slot pays for
the far-force increment: the coefficient of display (3.5) times the cell-volume
factor 4π/3 ≤ 5.
Equations
Instances For
Measurable harmonic and force envelopes at the prescribed collars #
theorem
CKN.Core.Step4.exists_gap_force_affine_envelope_instances
(q ε C_CZ τ R₀ R₁ r : ℝ)
(KU KD : ENNReal)
(hC : gapForceIncrementThreshold ≤ C_CZ)
(hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32)
{Ω : 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)
(hsmall :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
(hr : 0 < r)
(hcell : r ≤ (R₀ - R₁) / 4)
(i : Fin 3)
:
have hρ := ⋯;
∃ (M : ℝ → ENNReal),
AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0)) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0), MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => gapForceIncrement z hρ u p f i (y, s))
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ M s) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, M s ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The prescribed half-gap collar admits a measurable mass envelope within the affine slot.
theorem
CKN.Core.Step4.exists_gap_harmonic_affine_envelope_instances
(q ε C_CZ τ R₀ R₁ r : ℝ)
(KU KD : ENNReal)
(hC : gapHarmonicEnvelopeThreshold ≤ C_CZ)
(hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32)
{Ω : 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)
(hsmall :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
(hr : 0 < r)
(hcell : r ≤ (R₀ - R₁) / 4)
(i : Fin 3)
:
have hρ := ⋯;
∃ (M : ℝ → ENNReal),
AEMeasurable M (MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0)) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0), MeasureTheory.eLpNorm
(fun (y : Vec 3) =>
classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u) p
s)
y i)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict
(Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ M s) ∧ ∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, M s ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The prescribed half-gap collar admits a measurable mass envelope within the affine slot.
theorem
CKN.Core.Step4.actual_pressure_four_term_affine_instances
(q ε C_CZ τ R₀ R₁ r : ℝ)
(Cbase : ℝ → ℝ)
(KU KD : ENNReal)
(hthreshold : fourTermAffineThreshold (Cbase q) ≤ C_CZ)
(hforce : originASlotForceIncrementThreshold ≤ Cbase q)
(hharmonic : gapHarmonicEnvelopeThreshold ≤ Cbase q)
(hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32)
{Ω : 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 Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hsmall :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(hDp :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) =>
Dp (y, s) i)
(T : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ)
(hTm : ∀ (j i : Fin 3), Measurable (T j i))
(hT :
∀ (j i : Fin 3),
∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j i (y, s)) =ᵐ[MeasureTheory.volume]
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
fun (y : Foundation.Parabolic.Vec3) =>
(Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
(fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ k : Fin 3, Du w j k * u w k - f w j) (y, s))
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
(hr : 0 < r)
(hcell : r ≤ 1 / 256)
(i : Fin 3)
(hraw :
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => ∑ j : Fin 3, T j i (y, s)) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q (Cbase q) ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
(hcorrection :
have hρ := ⋯;
have η := mollifiedBallCutoff z.1 hρ;
have c := sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u;
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η (spatialDeriv η)
(fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) j)
x)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q (Cbase q) ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
:
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
The exact four-term decomposition gives the affine bound on every common thin cell. The first three time masses have measurable representatives or envelopes supplied by suitability; the correction needs only its mass bound.
theorem
CKN.Core.Step4.actual_pressure_four_term_affine_of_sws
(q ε C_CZ τ R₀ R₁ r : ℝ)
(Cbase : ℝ → ℝ)
(KU KD : ENNReal)
(hthreshold : fourTermAffineThreshold (Cbase q) ≤ C_CZ)
(hriesz : rieszSourceThresholdA ≤ Cbase q)
(hforce : originASlotForceIncrementThreshold ≤ Cbase q)
(hharmonic : gapHarmonicEnvelopeThreshold ≤ Cbase q)
(hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32)
{Ω : 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 Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hKU : KU < ⊤)
(hKD : KD < ⊤)
(hU :
∀ (k : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w k) ≤ KU)
(hD :
∀ (j k : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w j k) ≤ KD)
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I)
(hsmall :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u w)) ^ 3 + ENNReal.ofReal |p w| ^ (3 / 2) + ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(hDp :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) =>
Dp (y, s) i)
(z : Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
(hr : 0 < r)
(hcell : r ≤ 1 / 256)
(i : Fin 3)
(hcorrection :
have hρ := ⋯;
have η := mollifiedBallCutoff z.1 hρ;
have c := sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u;
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η (spatialDeriv η)
(fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) j)
x)
(ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q (Cbase q) ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
:
∫⁻ (s : ℝ) in Set.Ioc (z.2 - r ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0, MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)) ^ (6 / 5) ≤ originKPAffineASlot q C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q)))
Suitability supplies the selected raw Riesz field and both measurable envelopes. Only the centred-source correction mass remains to be supplied.