One Sided Morrey Monotone

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step4.oneSidedMorreyBound_mono {P τ ρ₀ : ℝ} {A₁ A₂ B₁ B₂ : ENNReal} (hP : 0 < P) (hA : A₁ ≤ A₂) (hB : B₁ ≤ B₂) : Endgame.oneSidedMorreyBound P τ ρ₀ A₁ B₁ ≤ Endgame.oneSidedMorreyBound P τ ρ₀ A₂ B₂

The one-sided Morrey transfer constant is monotone in both integral arguments A and B.

theorem CKN.Core.Step4.oneSidedMorreyBound_mono_left {P τ ρ₀ : ℝ} {A₁ A₂ B : ENNReal} (hP : 0 < P) (hA : A₁ ≤ A₂) : Endgame.oneSidedMorreyBound P τ ρ₀ A₁ B ≤ Endgame.oneSidedMorreyBound P τ ρ₀ A₂ B

The one-sided Morrey transfer constant is monotone in A alone.

theorem CKN.Core.Step4.oneSidedMorreyBound_mono_right {P τ ρ₀ : ℝ} {A B₁ B₂ : ENNReal} (hP : 0 < P) (hB : B₁ ≤ B₂) : Endgame.oneSidedMorreyBound P τ ρ₀ A B₁ ≤ Endgame.oneSidedMorreyBound P τ ρ₀ A B₂

The one-sided Morrey transfer constant is monotone in B alone.