Slice Selected Gradient Inputs Centred #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.Core.Step4.sourceSliceCentredMean
(x : Foundation.Parabolic.Vec3)
(ρ : ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
:
The spatial velocity mean used in the centred source at each time.
Equations
- CKN.Core.Step4.sourceSliceCentredMean x ρ u s j = ⨍ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball x ρ, u (y, s) j
Instances For
theorem
CKN.Core.Step4.centred_source_average_component_bound
{x : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(j : Fin 3)
:
‖sourceSliceCentredMean x ρ u s j‖ ≤ ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, |u (y, s) j|
The centred velocity component is bounded by its mean absolute value.
theorem
CKN.Core.Step4.sourceMorreyCutoffVCentredTensor_slice_bound_of_uncentred
{B : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.Vec3 → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3}
{c : Foundation.Parabolic.Vec3}
{i : Fin 3}
{Cη Cdη Cc : ℝ}
{KU KD Kunc Kforce : ENNReal}
(hCη : 0 ≤ Cη)
(hCdη : 0 ≤ Cdη)
(hCc : 0 ≤ Cc)
(hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B))
(hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B))
(hηbound : ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖η x‖ ≤ Cη)
(hdηbound : ∀ (j : Fin 3), ∀ᵐ (x : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖dη j x‖ ≤ Cdη)
(hc : ∀ (j : Fin 3), ‖c j‖ ≤ Cc)
(hUmeas :
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => u x i) (MeasureTheory.volume.restrict B))
(hDmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => Du x i j)
(MeasureTheory.volume.restrict B))
(hU :
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => u x i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ KU)
(hD :
∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Du x i j) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ KD)
(hunc :
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureDivergenceCutoffSource η dη u Du f x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc)
(hforce :
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => η x * f x i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ Kforce)
:
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentredTensor η dη u Du c x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc + ENNReal.ofReal Cc * ∑ _j : Fin 3, (ENNReal.ofReal Cη * KD + ENNReal.ofReal Cdη * KU) + Kforce
The force-free centred source is estimated by the full uncentred source,
the constant-mean correction, and the force term which removes −η f.
theorem
CKN.Core.Step4.sourceMorreyCutoffVCentredTensor_slice_bound_of_sourceMorrey
{B : Set Foundation.Parabolic.Vec3}
{x : Foundation.Parabolic.Vec3}
{ρ s : ℝ}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Cη Cdη : ℝ}
{KU KD Kunc : ENNReal}
{Kforce : Fin 3 → ENNReal}
(hCη : 0 ≤ Cη)
(hCdη : 0 ≤ Cdη)
(hη : MeasureTheory.AEStronglyMeasurable η (MeasureTheory.volume.restrict B))
(hdη : ∀ (j : Fin 3), MeasureTheory.AEStronglyMeasurable (dη j) (MeasureTheory.volume.restrict B))
(hηbound : ∀ᵐ (y : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖η y‖ ≤ Cη)
(hdηbound : ∀ (j : Fin 3), ∀ᵐ (y : Foundation.Parabolic.Vec3) ∂MeasureTheory.volume.restrict B, ‖dη j y‖ ≤ Cdη)
(hUmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j)
(MeasureTheory.volume.restrict B))
(hDmeas :
∀ (i j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) i j)
(MeasureTheory.volume.restrict B))
(hU :
∀ (j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => u (y, s) j) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ KU)
(hD :
∀ (i j : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => Du (y, s) i j) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ KD)
(hsourceMeas :
MeasureTheory.AEStronglyMeasurable
(fun (y : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffV η dη (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) (i j : Fin 3) => Du (y, s) i j)
(fun (y : Foundation.Parabolic.Vec3) => f (y, s)) y)
(MeasureTheory.volume.restrict B))
(hsourceBound :
MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffV η dη (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) (i j : Fin 3) => Du (y, s) i j)
(fun (y : Foundation.Parabolic.Vec3) => f (y, s)) y)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc)
(hforce :
∀ (i : Fin 3),
MeasureTheory.eLpNorm (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) i) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict B) ≤ Kforce i)
(i : Fin 3)
:
MeasureTheory.eLpNorm
(fun (y : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensor η dη (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) (i j : Fin 3) => Du (y, s) i j) (sourceSliceCentredMean x ρ u s) y i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict B) ≤ Kunc + ENNReal.ofReal
(∑ j : Fin 3, ⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x ρ, |u (y, s) j|) * ∑ _j : Fin 3, (ENNReal.ofReal Cη * KD + ENNReal.ofReal Cdη * KU) + Kforce i
Slice estimate for the force-free centred source, with the centring
constant bounded by the sum of the mean absolute velocities. The input
hsourceBound is the vector-valued uncentred estimate supplied by
sourceMorreyCutoffV_slice_bound.
theorem
CKN.Core.Step4.slice_selected_gradient_hV_of_centred_tensor_source
{J : Set ℝ}
{U : Set Foundation.Parabolic.Vec3}
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{c : ℝ → Foundation.Parabolic.Vec3}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
(hUmeas : MeasurableSet U)
(hηsupport : tsupport η ⊆ U)
(hdηsupport : ∀ (j : Fin 3), tsupport (dη j) ⊆ U)
(hUcompact : IsCompact U)
(hlocal :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensor η dη (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) (i j : Fin 3) => Du (y, s) i j) (c s) x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict U))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) => sourceMorreyCutoffVCentredTensorSpacetime η dη u Du c (x, s) i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume) ∧ ∀ (i : Fin 3),
HasCompactSupport fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensorSpacetime η dη u Du c (x, s) i
Local slice membership and the cutoff support give the global hV
predicate for the force-free centred source.
theorem
CKN.Core.Step4.slice_selected_gradient_hP78_input_of_sws_centred
{Ω : 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)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ harmonicRemainderForceBound z hρ f s
The centred-source consumer uses the force-potential input supplied by the same solution-level wrapper as the uncentred-source selector.
theorem
CKN.Core.Step4.slice_selected_gradient_of_sws_centred_source
(C₁₇ C₁₁ C₈ : ℝ)
(hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇)
(hC₈ : sliceForceGradientConstant ≤ C₈)
{E : ℝ → ℝ}
{Ω : 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)
(hC₁₁ : 0 ≤ C₁₁)
(hE : ∀ (s : ℝ), 0 ≤ E s)
(hCZ_p1 :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm
(pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s)
(ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E s ^ (2 / 3))
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
{U : Set Foundation.Parabolic.Vec3}
(hUmeas : MeasurableSet U)
(hηsupport : tsupport η ⊆ U)
(hdηsupport : ∀ (j : Fin 3), tsupport (dη j) ⊆ U)
(hUcompact : IsCompact U)
(hlocal :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensor η dη (fun (y : Foundation.Parabolic.Vec3) => u (y, s))
(fun (y : Foundation.Parabolic.Vec3) (i j : Fin 3) => Du (y, s) i j) (sourceSliceCentredMean z.1 ρ u s) x i)
(ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict U))
(hVpair :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
∑ i : Fin 3,
∫ (x : Foundation.Parabolic.Vec3), sourceMorreyCutoffVCentredTensorSpacetime η dη u Du (sourceSliceCentredMean z.1 ρ u) (x, s) i * spatialDeriv ψ i x = pressureSecondPairing
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
ψ)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
(∀ (k : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2))
MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ (∀ (k : Fin 3),
HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) =>
D x k) ∧ ∀ (k : Fin 3),
MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k) (ENNReal.ofReal (6 / 5))
(MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal Foundation.Euclidean.czGradientOperatorConstant * ∑ i : Fin 3,
MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensorSpacetime η dη u Du (sourceSliceCentredMean z.1 ρ u) (x, s) i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal
(C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + harmonicRemainderForceBound z hρ f s) * ρ ^ (-1 / 2)) + ENNReal.ofReal (sliceForceGradientBound Foundation.Euclidean.czGradientOperatorConstant C₈ z.1 hρ f s)
The unconditional slice selector consumes the force-free centred source and its tested pairing.