Morrey membership of the force-free centred tensor source #
The convection term uses the product exponents 2 and 3. The cutoff
term uses two velocity factors. Bounded cutoff coefficients and the
bounded source carrier preserve finiteness at the target exponent.
theorem
CKN.Core.Step4.pressure_source_bounded_multiplier_morrey_lt_top
{P κ C : ℝ}
(hP : 0 < P)
{a g : Foundation.Parabolic.ParabolicPoint → ℝ}
(ha : ∀ᵐ (z : Foundation.Parabolic.ParabolicPoint), |a z| ≤ |C|)
(hg : Foundation.Parabolic.Morrey.morreyNorm P κ g < ⊤)
:
(Foundation.Parabolic.Morrey.morreyNorm P κ fun (z : Foundation.Parabolic.ParabolicPoint) => a z * g z) < ⊤
An almost-everywhere bounded scalar multiplier preserves finite Morrey seminorm.
theorem
CKN.Core.Step4.pressure_source_lower_integrability_morrey_lt_top
{P P₀ κ : ℝ}
(hP : 1 ≤ P)
(hPP₀ : P ≤ P₀)
(hP₀κ : P₀ ≤ κ)
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hg : AEMeasurable g MeasureTheory.volume)
(hN : Foundation.Parabolic.Morrey.morreyNorm P₀ κ g < ⊤)
:
Lowering the integrability exponent preserves finite Morrey seminorm.
theorem
CKN.Core.Step4.pressure_source_lower_exponent_morrey_lt_top
{P κ κ₀ R : ℝ}
(hP : 1 ≤ P)
(hPκ : P ≤ κ)
(hκκ₀ : κ ≤ κ₀)
{g : Foundation.Parabolic.ParabolicPoint → ℝ}
{z₀ : Foundation.Parabolic.ParabolicPoint}
(hR : 0 < R)
(hsupport : ∀ z ∉ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R, g z = 0)
(hN : Foundation.Parabolic.Morrey.morreyNorm P κ₀ g < ⊤)
:
Lowering the Morrey exponent on a bounded carrier preserves finiteness.
theorem
CKN.Core.Step4.pressure_centred_tensor_source_morrey_lt_top
{τ κ R Cη Cdη : ℝ}
(hτ : 25 / 3 ≤ τ)
(hκ : 6 / 5 ≤ κ)
(hκhi : κ ≤ 25 / 9)
(hκτ : κ ≤ (1 / τ + 8 / 25)⁻¹)
{S : Set Foundation.Parabolic.ParabolicPoint}
{z₀ : Foundation.Parabolic.ParabolicPoint}
(hR : 0 < R)
(hS : S ⊆ Foundation.Parabolic.parabolicCylinder z₀.1 z₀.2 R)
{η : Foundation.Parabolic.Vec3 → ℝ}
{dη : Fin 3 → Foundation.Parabolic.Vec3 → ℝ}
(hη : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => η z.1) MeasureTheory.volume)
(hdη : ∀ (j : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => dη j z.1) MeasureTheory.volume)
(hηbound : ∀ (x : Foundation.Parabolic.Vec3), |η x| ≤ |Cη|)
(hdηbound : ∀ (j : Fin 3) (x : Foundation.Parabolic.Vec3), |dη j x| ≤ |Cdη|)
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{c : ℝ → Foundation.Parabolic.Vec3}
(hUa :
∀ (j : Fin 3), AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) MeasureTheory.volume)
(hWa :
∀ (j : Fin 3),
AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j - c z.2 j) MeasureTheory.volume)
(hDa :
∀ (i j : Fin 3),
AEMeasurable (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) MeasureTheory.volume)
(hU :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ (S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j) < ⊤)
(hW :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z j - c z.2 j) < ⊤)
(hD :
∀ (i j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j) < ⊤)
(i : Fin 3)
:
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ
(S.indicator fun (z : Foundation.Parabolic.ParabolicPoint) =>
sourceMorreyCutoffVCentredTensorSpacetime η dη u Du c z i) < ⊤
The centred force-free source is in the target Morrey class from the velocity, centred velocity, and weak-gradient Morrey data.