English
If MemLp f q μ holds and p ≤ q, then MemLp f p μ holds as well.
Русский
Если MemLp f q μ выполняется и p ≤ q, то MemLp f p μ также верно.
LaTeX
$$$MemLp f q μ \\Rightarrow p \\le q \\Rightarrow MemLp f p μ$$$
Lean4
theorem mono_exponent {p q : ℝ≥0∞} [IsFiniteMeasure μ] (hfq : MemLp f q μ) (hpq : p ≤ q) : MemLp f p μ :=
by
obtain ⟨hfq_m, hfq_lt_top⟩ := hfq
by_cases hp0 : p = 0
· rwa [hp0, memLp_zero_iff_aestronglyMeasurable]
rw [← Ne] at hp0
refine ⟨hfq_m, ?_⟩
by_cases hp_top : p = ∞
· have hq_top : q = ∞ := by rwa [hp_top, top_le_iff] at hpq
rw [hp_top]
rwa [hq_top] at hfq_lt_top
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
by_cases hq_top : q = ∞
· rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
rw [hq_top, eLpNorm_exponent_top] at hfq_lt_top
refine lt_of_le_of_lt (eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ hp_pos) ?_
refine ENNReal.mul_lt_top hfq_lt_top ?_
exact ENNReal.rpow_lt_top_of_nonneg (by simp [hp_pos.le]) (measure_ne_top μ Set.univ)
have hq0 : q ≠ 0 := by
by_contra hq_eq_zero
have hp_eq_zero : p = 0 := le_antisymm (by rwa [hq_eq_zero] at hpq) (zero_le _)
rw [hp_eq_zero, ENNReal.toReal_zero] at hp_pos
exact (lt_irrefl _) hp_pos
have hpq_real : p.toReal ≤ q.toReal := ENNReal.toReal_mono hq_top hpq
rw [eLpNorm_eq_eLpNorm' hp0 hp_top]
rw [eLpNorm_eq_eLpNorm' hq0 hq_top] at hfq_lt_top
exact eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le hfq_m hfq_lt_top hp_pos.le hpq_real
