Morrey bounds under parabolic changes of variables

The numerical pressure and bootstrap bounds use unit cylinders. A positive parabolic dilation transports their Morrey norms with the explicit factor a ^ (-5 / τ). The estimate below takes the supremum over every centre and radius and does not impose integrability assumptions on the source.

theorem CKN.Core.Endgame.force_slot_scaling_injective {a : ℝ} (ha : 0 < a) (z₀ : Foundation.Parabolic.ParabolicPoint) : Function.Injective (scalingParabolic a z₀)

A positive parabolic dilation is injective.

theorem CKN.Core.Endgame.force_slot_cylinder_image {a : ℝ} (ha : 0 < a) (z₀ z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) : scalingParabolic a z₀ '' Foundation.Parabolic.parabolicCylinder z.1 z.2 r = Foundation.Parabolic.parabolicCylinder (scalingParabolic a z₀ z).1 (scalingParabolic a z₀ z).2 (a * r)

A positive dilation maps each cylinder to the cylinder with scaled radius.

theorem CKN.Core.Endgame.force_slot_integral_scaling {a : ℝ} (ha : 0 < a) (z₀ : Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : ∫ (w : Foundation.Parabolic.ParabolicPoint), f (scalingParabolic a z₀ w) = a⁻¹ ^ 5 * ∫ (w : Foundation.Parabolic.ParabolicPoint), f w

Real integrals transform by the parabolic Jacobian, without additional measurability or integrability assumptions.

theorem CKN.Core.Endgame.force_slot_lintegral_scaling {a : ℝ} (ha : 0 < a) (z₀ z : Foundation.Parabolic.ParabolicPoint) (r : ℝ) (f : Foundation.Parabolic.ParabolicPoint → ENNReal) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, f (scalingParabolic a z₀ w) = ENNReal.ofReal (a⁻¹ ^ 5) * ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder (scalingParabolic a z₀ z).1 (scalingParabolic a z₀ z).2 (a * r), f w

A nonnegative cylinder integral transforms by the parabolic Jacobian.

theorem CKN.Core.Endgame.force_slot_power_integral_scaling {a : ℝ} (ha : 0 < a) (z₀ z : Foundation.Parabolic.ParabolicPoint) (r P : ℝ) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : Foundation.Parabolic.Morrey.cylinderPowerIntegral P (fun (w : Foundation.Parabolic.ParabolicPoint) => f (scalingParabolic a z₀ w)) z r = ENNReal.ofReal (a⁻¹ ^ 5) * Foundation.Parabolic.Morrey.cylinderPowerIntegral P f (scalingParabolic a z₀ z) (a * r)

The integral in every Morrey cell transforms by the parabolic Jacobian.

theorem CKN.Core.Endgame.force_slot_morrey_scaling_le {a P τ : ℝ} (ha : 0 < a) (hP : 0 < P) (z₀ : Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : (Foundation.Parabolic.Morrey.morreyNorm P τ fun (w : Foundation.Parabolic.ParabolicPoint) => f (scalingParabolic a z₀ w)) ≤ ENNReal.ofReal a ^ (-5 / τ) * Foundation.Parabolic.Morrey.morreyNorm P τ f

A positive parabolic dilation gives the all-centre numerical Morrey bound.

theorem CKN.Core.Endgame.force_slot_indicator_scaling_le (a c P τ : ℝ) (K : ENNReal) (ha : 0 < a) (hP : 0 < P) (z₀ : Foundation.Parabolic.ParabolicPoint) (Q : Set Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator f) ≤ K) : Foundation.Parabolic.Morrey.morreyNorm P τ ((scalingParabolic a z₀ ⁻¹' Q).indicator fun (w : Foundation.Parabolic.ParabolicPoint) => c * f (scalingParabolic a z₀ w)) ≤ ENNReal.ofReal |c| * (ENNReal.ofReal a ^ (-5 / τ) * K)

A numerical bound for an indicated source transports with both the field amplitude and the parabolic Morrey scaling factor retained.

theorem CKN.Core.Endgame.force_slot_scaling_bound_lt_top (a c τ : ℝ) {K : ENNReal} (ha : 0 < a) (hK : K < ⊤) : ENNReal.ofReal |c| * (ENNReal.ofReal a ^ (-5 / τ) * K) < ⊤

Finite data remain finite under every positive parabolic rescaling.

theorem CKN.Core.Endgame.force_slot_morrey_unscaling_le {a P τ : ℝ} (ha : 0 < a) (hP : 0 < P) (z₀ : Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) : Foundation.Parabolic.Morrey.morreyNorm P τ f ≤ ENNReal.ofReal a ^ (5 / τ) * Foundation.Parabolic.Morrey.morreyNorm P τ fun (w : Foundation.Parabolic.ParabolicPoint) => f (scalingParabolic a z₀ w)

The reverse change of variables recovers a bound on the original field from a bound in normalized coordinates.

theorem CKN.Core.Endgame.force_slot_subcarrier_scaling_le (a c P τ : ℝ) (K : ENNReal) (ha : 0 < a) (hP : 0 < P) (z₀ : Foundation.Parabolic.ParabolicPoint) (Q B : Set Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) (hQB : scalingParabolic a z₀ '' Q ⊆ B) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ (B.indicator f) ≤ K) : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => c * f (scalingParabolic a z₀ w)) ≤ ENNReal.ofReal |c| * (ENNReal.ofReal a ^ (-5 / τ) * K)

A normalized subcarrier inherits the explicit scaled bound on its original carrier.

theorem CKN.Core.Endgame.force_slot_subcarrier_unscaling_le (a c P τ : ℝ) (K : ENNReal) (ha : 0 < a) (hc : c ≠ 0) (hP : 0 < P) (z₀ : Foundation.Parabolic.ParabolicPoint) (Q B : Set Foundation.Parabolic.ParabolicPoint) (f : Foundation.Parabolic.ParabolicPoint → ℝ) (hBQ : scalingParabolic a z₀ ⁻¹' B ⊆ Q) (hN : Foundation.Parabolic.Morrey.morreyNorm P τ (Q.indicator fun (w : Foundation.Parabolic.ParabolicPoint) => c * f (scalingParabolic a z₀ w)) ≤ K) : Foundation.Parabolic.Morrey.morreyNorm P τ (B.indicator f) ≤ ENNReal.ofReal a ^ (5 / τ) * (ENNReal.ofReal |c⁻¹| * K)

A nonzero field amplitude can be removed from a normalized Morrey bound, retaining the inverse amplitude and dilation factors.