The A slot from its homogeneous centred-source correction #
The other three terms, their measurable envelopes, and the finite-cell transfer are supplied internally. Only the displayed correction estimate remains as the analytic input of this reduction.
The instance A-slot interface with exponent-dependent thresholds #
The base threshold may depend on the force exponent alone. The analytic estimate is restricted to the common half-collar radius. The finite cover restores the exact cell range of the pressure adapter.
theorem
CKN.Core.Step4.theoremA_aSlot_integral_instances_of_thin_cells_q
(Cbase : ℝ → ℝ)
(hCbase : ∀ (q : ℝ), 0 ≤ Cbase q)
(hmargin :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
Cbase q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (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) →
∀ (i : Fin 3),
∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁),
∀ (r : ℝ),
0 < r →
r ≤ 1 / 256 →
∫⁻ (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))))
(q τ C_CZ R₀ R₁ ε : ℝ)
(KU KD : ENNReal)
:
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
originASlotThinCellThreshold (Cbase q) ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (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) →
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
∫⁻ (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)))
Thin-cell bounds at the two prescribed triples imply the full A-slot integral estimate with one absolute increase of the coefficient.
The triangle cost followed by one finite-cover cost.
Equations
Instances For
theorem
CKN.Core.Step4.theoremA_aSlot_integral_of_source_correction
(CM2 : ℝ → ℝ)
(hM2 :
∀ (q τ C_CZ R₀ R₁ ε : ℝ) (KU KD : ENNReal),
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
CM2 q ≤ C_CZ →
∀ (hinstances : τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32),
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∀ (i : Fin 3),
∀ z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁),
∀ (r : ℝ),
0 < r →
r ≤ 1 / 256 →
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 C_CZ ε KU KD * ENNReal.ofReal (r ^ (5 * (1 - 6 / 5 / min (1 / τ + 8 / 25)⁻¹ q))))
(q τ C_CZ R₀ R₁ ε : ℝ)
(KU KD : ENNReal)
:
5 / 2 < q →
25 / 3 ≤ τ →
τ ≤ 25 →
0 ≤ C_CZ →
originASlotCorrectionThreshold CM2 q ≤ C_CZ →
τ = 25 / 3 ∧ R₀ = 11 / 16 ∧ R₁ = 43 / 64 ∨ τ = 25 ∧ R₀ = 5 / 8 ∧ R₁ = 19 / 32 →
0 < R₁ →
R₁ < R₀ →
R₀ < 3 / 4 →
0 ≤ ε →
KU < ⊤ →
KD < ⊤ →
∀ {Ω : 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},
IsSuitableWeakSolutionIntegrable Ω I q u Du p f →
closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I →
(∀ (i : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder 0 0 R₀).indicator
fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ KU) →
(∀ (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) →
∫⁻ (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 ε →
∀ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3),
Measurable Dp →
(∀ᵐ (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) →
∀ (i : Fin 3),
∀ z ∈ Foundation.Parabolic.parabolicCylinder 0 0 (3 / 4),
∀ (r : ℝ),
0 < r →
r ≤ R₁ →
∫⁻ (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 homogeneous correction bound on the common half-collar scale implies the exact exponent-dependent A-slot integral binder.