English
Let s be a measurable set and c a vector in E. For any p ∈ ℝ≥0∞, the function x ↦ c on s and 0 outside s belongs to L^p(μ) provided either c = 0 or μ(s) < ∞. In particular, the indicator of s with constant value c lies in L^p(μ) under this finiteness condition.
Русский
Пусть s — измеримое множество, c — вектор из E. Для любого p ∈ ℝ≥0∞ функция x ↦ c при x ∈ s и 0 иначе принадлежит L^p(μ), если выполняется либо c = 0, либо μ(s) < ∞. В частности, индикатор множества s, умноженный на константу c, принадлежит L^p(μ) при этом условии конечности.
LaTeX
$$$(\\chi_s \\cdot c) \\in L^p(\\mu) \\quad \\text{provided} \\quad c = 0 \\lor \\mu(s) < \\infty.$$$
Lean4
theorem memLp_indicator_const (p : ℝ≥0∞) (hs : MeasurableSet s) (c : E) (hμsc : c = 0 ∨ μ s ≠ ∞) :
MemLp (s.indicator fun _ => c) p μ :=
by
rw [memLp_indicator_iff_restrict hs]
obtain rfl | hμ := hμsc
· exact MemLp.zero
· have := Fact.mk hμ.lt_top
apply memLp_const
