Restriction of indicated Morrey data

Smaller carriers retain the same numerical Morrey bound. Joint measurability on a spatial-time strip gives globally measurable past-cylinder indications.

theorem CKN.Core.Endgame.morreyNorm_indicator_mono_set {P τ : ℝ} (hP : 0 ≤ P) {S T : Set Foundation.Parabolic.ParabolicPoint} (hST : S ⊆ T) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : Foundation.Parabolic.Morrey.morreyNorm P τ (S.indicator f) ≤ Foundation.Parabolic.Morrey.morreyNorm P τ (T.indicator f)

Restricting an indicated source cannot increase its Morrey norm.

theorem CKN.Core.Endgame.morreyVecMem_mono_carrier {P τ : ℝ} (hP : 0 ≤ P) {S T : Set Foundation.Parabolic.ParabolicPoint} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hST : S ⊆ T) (hu : morreyVecMem P τ T u) : morreyVecMem P τ S u

Componentwise ball-Morrey membership restricts to any smaller carrier.