The scale cost of measuring the one-sided constant at the margin

The one-sided transfer constant oneSidedMorreyBound is built from a small-cell bound and a whole-carrier integral bound. This file isolates the exact cost of measuring the meeting point of the two regimes at the margin scale ρ₀ rather than at the carrier radius ρ₁: the small-cell constant A is untouched, while the whole-carrier constant B carries the explicit scale ratio (ρ₁ / ρ₀) ^ (5 * (1 - P / τ)). The second statement is the form in which a comparison against an explicit majorant stated at the carrier radius is transported down to the margin scale.

theorem CKN.Core.Step4.oneSidedMorreyBound_scale_eq {P τ ρ₀ ρ₁ : ℝ} {A B : ENNReal} (hP : 0 < P) (hρ₀ : 0 < ρ₀) (hρ₁ : 0 < ρ₁) : Endgame.oneSidedMorreyBound P τ ρ₀ A B = Endgame.oneSidedMorreyBound P τ ρ₁ A (B * ENNReal.ofReal ((ρ₁ / ρ₀) ^ (5 * (1 - P / τ))))

Measuring the one-sided transfer constant at a smaller scale ρ₀ is exactly the same as measuring it at ρ₁ with the whole-carrier constant B inflated by the explicit ratio (ρ₁ / ρ₀) ^ (5 * (1 - P / τ)); the small-cell constant is untouched.

theorem CKN.Core.Step4.oneSidedMorreyBound_margin_le_of_scaled {P τ ρ₀ ρ₁ : ℝ} {A B K : ENNReal} (hP : 0 < P) (hρ₀ : 0 < ρ₀) (hρ₁ : 0 < ρ₁) (h : Endgame.oneSidedMorreyBound P τ ρ₁ A (B * ENNReal.ofReal ((ρ₁ / ρ₀) ^ (5 * (1 - P / τ)))) ≤ K) : Endgame.oneSidedMorreyBound P τ ρ₀ A B ≤ K

Transport to the margin scale of a comparison against an explicit majorant stated at the carrier radius: a bound on the constant measured at ρ₁ with the inflated whole-carrier constant also bounds the constant measured at ρ₀.