Homogeneous time mass of the annular force increment #
Spatial boundedness on the half-collar and Holder's inequality in space and time retain the force data power without an additive constant.
Four-term pressure mass and affine absorption #
theorem
CKN.Core.Step4.four_term_slice_mass_le
{μ : MeasureTheory.Measure Foundation.Parabolic.Vec3}
{D A B C E : Foundation.Parabolic.Vec3 → ℝ}
(hid : D =ᵐ[μ] fun (x : Foundation.Parabolic.Vec3) => -A x + B x + C x - E x)
:
MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) μ ^ (6 / 5) ≤ 16 * (MeasureTheory.eLpNorm A (ENNReal.ofReal (6 / 5)) μ ^ (6 / 5) + MeasureTheory.eLpNorm B (ENNReal.ofReal (6 / 5)) μ ^ (6 / 5) + MeasureTheory.eLpNorm C (ENNReal.ofReal (6 / 5)) μ ^ (6 / 5) + MeasureTheory.eLpNorm E (ENNReal.ofReal (6 / 5)) μ ^ (6 / 5))
The signed four-term identity controls each spatial slice norm.
The absolute enlargement pays the triangle cost and all four component budgets.
Instances For
theorem
CKN.Core.Step4.four_term_affine_cost_absorbed
{q ε Cbase C_CZ : ℝ}
{KU KD : ENNReal}
(hthreshold : fourTermAffineThreshold Cbase ≤ C_CZ)
:
Four component bounds at the base constant fit the enlarged affine slot.
theorem
CKN.Core.Step4.four_term_time_mass_le
{ν : MeasureTheory.Measure ℝ}
{D A B C E : ℝ → ENNReal}
(hA : AEMeasurable A ν)
(hB : AEMeasurable B ν)
(hC : AEMeasurable C ν)
(hbound : ∀ᵐ (s : ℝ) ∂ν, D s ≤ 16 * (A s + B s + C s + E s))
:
Integration preserves the four-term cost for measurable slice masses.
theorem
CKN.Core.Step4.four_term_time_mass_affine
{ν : MeasureTheory.Measure ℝ}
{D A B C E : ℝ → ENNReal}
{q ε Cbase C_CZ : ℝ}
{KU KD L : ENNReal}
(hthreshold : fourTermAffineThreshold Cbase ≤ C_CZ)
(hA : AEMeasurable A ν)
(hB : AEMeasurable B ν)
(hC : AEMeasurable C ν)
(hbound : ∀ᵐ (s : ℝ) ∂ν, D s ≤ 16 * (A s + B s + C s + E s))
(hAm : ∫⁻ (s : ℝ), A s ∂ν ≤ originKPAffineASlot q Cbase ε KU KD * L)
(hBm : ∫⁻ (s : ℝ), B s ∂ν ≤ originKPAffineASlot q Cbase ε KU KD * L)
(hCm : ∫⁻ (s : ℝ), C s ∂ν ≤ originKPAffineASlot q Cbase ε KU KD * L)
(hEm : ∫⁻ (s : ℝ), E s ∂ν ≤ originKPAffineASlot q Cbase ε KU KD * L)
:
Four slice-mass budgets combine into one enlarged affine budget.
An absolute affine threshold for the force-potential increment #
An explicit absolute threshold for the force-potential increment.
Equations
Instances For
theorem
CKN.Core.Step4.exists_gap_force_mass_envelope_of_sws
(ε R₁ r : ℝ)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hlo : 1 / 128 ≤ ρ)
(hhi : ρ ≤ 1 / 2)
(hr : 0 < r)
(hrρ : r ≤ ρ / 2)
{Ω : 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)
(hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1)
(hforce :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(i : Fin 3)
:
∃ (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 ≤ MeasureTheory.volume (Foundation.Parabolic.vec3Ball z.1 r ∩ Foundation.Parabolic.vec3Ball 0 R₁) * ENNReal.ofReal gapForceIncrementCoefficient ^ (6 / 5) * ENNReal.ofReal (r ^ 2) ^ (1 - 6 / (5 * q)) * ENNReal.ofReal ε ^ (6 / (5 * q))
The clipped mass of the actual force increment has the homogeneous force power and the spatial cell volume, on every interior half-collar.
theorem
CKN.Core.Step4.exists_gap_force_affine_envelope_of_sws
(ε C_CZ τ R₁ r : ℝ)
(KU KD : ENNReal)
(hC : gapForceIncrementThreshold ≤ C_CZ)
(hτ : 25 / 3 ≤ τ)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hlo : 1 / 128 ≤ ρ)
(hhi : ρ ≤ 1 / 2)
(hr : 0 < r)
(hrρ : r ≤ ρ / 2)
{Ω : 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)
(hQ : Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ ⊆ Foundation.Parabolic.parabolicCylinder 0 0 1)
(hforce :
∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder 0 0 1, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f w)) ^ q ≤ ENNReal.ofReal ε)
(i : Fin 3)
:
∃ (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 force increment has a measurable mass envelope within the affine slot.