English
A bounded measurable function with compact support lies in Lp provided a bound on its norm holds almost everywhere.
Русский
Функция с компактной областью поддержки и ограниченной нормой принадлежит Lp, если выполняются условия измеримости.
LaTeX
$$HasCompactSupport.memLp_of_bound {f} (hf : HasCompactSupport f) (h2f : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : MemLp f p μ$$
Lean4
/-- A bounded measurable function with compact support is in L^p. -/
theorem _root_.HasCompactSupport.memLp_of_bound {f : X → E} (hf : HasCompactSupport f) (h2f : AEStronglyMeasurable f μ)
(C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : MemLp f p μ :=
by
have := memLp_top_of_bound h2f C hfC
exact
this.mono_exponent_of_measure_support_ne_top (fun x ↦ image_eq_zero_of_notMem_tsupport) (hf.measure_lt_top.ne)
le_top
