eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le

English

If eLpNorm' f q μ < ∞ for some q, and 0 ≤ p ≤ q, then eLpNorm' f p μ < ∞.

Русский

Если eLpNorm' f q μ < ∞ и 0 ≤ p ≤ q, то eLpNorm' f p μ < ∞.

LaTeX

$$$[0 \\le p] \land p \\le q \\land eLpNorm' f q μ < ∞ \\Rightarrow eLpNorm' f p μ < ∞$$$

Lean4

theorem eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le {p q : ℝ} [IsFiniteMeasure μ] (hf : AEStronglyMeasurable f μ)
    (hfq_lt_top : eLpNorm' f q μ < ∞) (hp_nonneg : 0 ≤ p) (hpq : p ≤ q) : eLpNorm' f p μ < ∞ :=
  by
  rcases le_or_gt p 0 with hp_nonpos | hp_pos
  · rw [le_antisymm hp_nonpos hp_nonneg]
    simp
  have hq_pos : 0 < q := lt_of_lt_of_le hp_pos hpq
  calc
    eLpNorm' f p μ ≤ eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q) :=
      eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ hp_pos hpq hf
    _ < ∞ := by
      rw [ENNReal.mul_lt_top_iff]
      refine Or.inl ⟨hfq_lt_top, ENNReal.rpow_lt_top_of_nonneg ?_ (measure_ne_top μ Set.univ)⟩
      rwa [le_sub_comm, sub_zero, one_div, one_div, inv_le_inv₀ hq_pos hp_pos]

Похожие утверждения