of_measure_le_smul — Mathlib

English

If f ∈ Lp(μ) and c ≠ ∞, then f ∈ Lp(c·μ).

Русский

Если f ∈ Lp(μ) и c ≠ ∞, то f ∈ Lp(c·μ).

LaTeX

$${f} {p} {μ} MemLp f p μ → {c} {hc} Ne c top → MemLp f p (c • μ).$$

Lean4

theorem of_measure_le_smul {μ' : Measure α} {c : ℝ≥0∞} (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ) {f : α → ε}
    (hf : MemLp f p μ) : MemLp f p μ' :=
  by
  refine ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), ?_⟩
  refine (eLpNorm_mono_measure f hμ'_le).trans_lt ?_
  by_cases hc0 : c = 0
  · simp [hc0]
  rw [eLpNorm_smul_measure_of_ne_zero hc0, smul_eq_mul]
  refine ENNReal.mul_lt_top (Ne.lt_top ?_) hf.2
  simp [hc, hc0]

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