Morrey bounds from carrier-local representatives

Almost-everywhere equality on a measurable carrier transfers global bounds of a representative to the indicated original function. The representative need not vanish outside the carrier.

theorem CKN.Core.Endgame.morreyNorm_eq_of_ae_eq {P τ : ℝ} {f g : Foundation.Parabolic.ParabolicPoint → ℝ} (hfg : f =ᵐ[MeasureTheory.volume] g) : Foundation.Parabolic.Morrey.morreyNorm P τ f = Foundation.Parabolic.Morrey.morreyNorm P τ g

Almost-everywhere equal scalar functions have the same cylinder Morrey norm.

theorem CKN.Core.Endgame.morreyNorm_indicator_le_of_ae_eq_restrict {P τ : ℝ} (hP : 0 ≤ P) {Q : Set Foundation.Parabolic.ParabolicPoint} (hQ : MeasurableSet Q) {u v : Foundation.Parabolic.ParabolicPoint → ℝ} (huv : u =ᵐ[MeasureTheory.volume.restrict Q] v) : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator u) ≤ Foundation.Parabolic.Morrey.morreyNorm P τ v

A carrier-local representative bounds the indicated scalar Morrey norm.

theorem CKN.Core.Endgame.morreyNorm_component_indicator_le_of_ae_eq_restrict {P τ : ℝ} (hP : 0 ≤ P) {Q : Set Foundation.Parabolic.ParabolicPoint} (hQ : MeasurableSet Q) {u v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (huv : u =ᵐ[MeasureTheory.volume.restrict Q] v) (i : Fin 3) : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => v z i

Component bounds transfer without imposing global equality to the representative.

theorem CKN.Core.Endgame.morreyNorm_component_indicator_le_norm_of_ae_eq_restrict {P τ : ℝ} (hP : 0 ≤ P) {Q : Set Foundation.Parabolic.ParabolicPoint} (hQ : MeasurableSet Q) {u v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (huv : u =ᵐ[MeasureTheory.volume.restrict Q] v) (i : Fin 3) : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator fun (z : Foundation.Parabolic.ParabolicPoint) => u z i) ≤ Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (v z)

A global Euclidean-norm bound controls every indicated component.

theorem CKN.Core.Endgame.morreyVecMem_of_ae_eq_restrict {P τ : ℝ} (hP : 1 ≤ P) (hPτ : P ≤ τ) {Q : Set Foundation.Parabolic.ParabolicPoint} (hQ : MeasurableSet Q) {u v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (huv : u =ᵐ[MeasureTheory.volume.restrict Q] v) (hv : ∀ (i : Fin 3), (Foundation.Parabolic.Morrey.morreyNorm P τ fun (z : Foundation.Parabolic.ParabolicPoint) => v z i) < ⊤) : morreyVecMem P τ Q u

Finite global component norms give carrier-local vector Morrey membership.

theorem CKN.Core.Endgame.morreyVecMem_three_twentyFive_of_ae_eq_restrict {Q : Set Foundation.Parabolic.ParabolicPoint} (hQ : MeasurableSet Q) {u v : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (huv : u =ᵐ[MeasureTheory.volume.restrict Q] v) (hv : (Foundation.Parabolic.Morrey.morreyNorm 3 25 fun (z : Foundation.Parabolic.ParabolicPoint) => Foundation.Parabolic.vec3EuclideanNorm (v z)) < ⊤) : morreyVecMem 3 25 Q u

A finite global Euclidean-norm Morrey bound gives membership at exponents 3 and 25.