English
Let s, t be measurable sets, deterministic p ∈ ENNReal, and e ∈ E. If hμt ≠ ∞ and h t is measurable, then the integral of the p-indicatorConstLp function over s equals μ.real(t ∩ s) times e.
Русский
Пусть s, t — измеримые множества, p ∈ ENNReal и e ∈ E. При условии hμt ≠ ∞ и ht измеримо, интеграл от функции indicatorConstLp(p, ht, hμt, e) по s равен μ.real(t ∩ s)·e.
LaTeX
$$$$ \\int_X \\mathrm{indicatorConstLp}(p, ht, h\\mu t, e)(x) \\, d\\mu(x) = \\mu_{\\mathbb{R}}(t \\cap s) \\; e $$$$
Lean4
theorem setIntegral_indicatorConstLp [CompleteSpace E] {p : ℝ≥0∞} (hs : MeasurableSet s) (ht : MeasurableSet t)
(hμt : μ t ≠ ∞) (e : E) : ∫ x in s, indicatorConstLp p ht hμt e x ∂μ = μ.real (t ∩ s) • e :=
calc
∫ x in s, indicatorConstLp p ht hμt e x ∂μ = ∫ x in s, t.indicator (fun _ => e) x ∂μ := by
rw [setIntegral_congr_ae hs (indicatorConstLp_coeFn.mono fun x hx _ => hx)]
_ = (μ.real (t ∩ s)) • e := by rw [integral_indicator_const _ ht, measureReal_restrict_apply ht]
