Component bounds for Euclidean vector-source Morrey norms #
The Euclidean norm is bounded by the sum of the three absolute coordinate values. The scalar triangle inequality transfers this comparison to the Morrey norm without changing either exponent.
theorem
CKN.Core.Endgame.morrey_norm_add_le
{P τ : ℝ}
(hP : 1 ≤ P)
{f g : Foundation.Parabolic.ParabolicPoint → ℝ}
(hf : AEMeasurable f MeasureTheory.volume)
(hg : AEMeasurable g MeasureTheory.volume)
:
(Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => f z + g z) ≤ Foundation.Parabolic.Morrey.morreyNorm P τ f + Foundation.Parabolic.Morrey.morreyNorm P τ g
The scalar Morrey triangle inequality for any integrability exponent at least one. No restriction on the outer exponent is needed.
theorem
CKN.Core.Endgame.morrey_norm_euclidean_le_sum_components
{P τ : ℝ}
(hP : 1 ≤ P)
{g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume)
:
(Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (g z)) ≤ ∑ i : Fin 3, Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => g z i
The Euclidean norm of a three-component source is bounded in Morrey norm by the sum of its component Morrey norms, with constant one.
theorem
CKN.Core.Endgame.morrey_norm_euclidean_lt_top_of_components
{P τ : ℝ}
(hP : 1 ≤ P)
{g : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hg : ∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) MeasureTheory.volume)
(hN :
∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => g z i) < ⊤)
:
(Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) =>
Foundation.Parabolic.vec3EuclideanNorm (g z)) < ⊤
Finite component Morrey norms give a finite Euclidean norm-source Morrey norm at the same exponents.