English
If for every nonzero y the preimage μ(f^{-1}({y})) is finite, then MemLp f p μ.
Русский
Если для каждого y ≠ 0 мера множества f^{-1}({y}) конечна, то f ∈ L^p.
LaTeX
$$$(\\forall y\\, (y\\neq 0) \\Rightarrow \\mu(f^{-1}(\\{y\\}))<\\infty) \\Rightarrow \\mathrm{MemLp}(f,p,\\mu)$$$
Lean4
theorem memLp_of_finite_measure_preimage (p : ℝ≥0∞) {f : α →ₛ E} (hf : ∀ y, y ≠ 0 → μ (f ⁻¹' { y }) < ∞) :
MemLp f p μ := by
by_cases hp0 : p = 0
· rw [hp0, memLp_zero_iff_aestronglyMeasurable]; exact f.aestronglyMeasurable
by_cases hp_top : p = ∞
· rw [hp_top]; exact memLp_top f μ
refine ⟨f.aestronglyMeasurable, ?_⟩
rw [eLpNorm_eq_eLpNorm' hp0 hp_top, f.eLpNorm'_eq]
refine ENNReal.rpow_lt_top_of_nonneg (by simp) (ENNReal.sum_lt_top.mpr fun y _ => ?_).ne
by_cases hy0 : y = 0
· simp [hy0, ENNReal.toReal_pos hp0 hp_top]
· refine ENNReal.mul_lt_top ?_ (hf y hy0)
exact ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top
