English
Let t ⊆ X be measurable, hμt ≠ ∞, and e ∈ E. Then the integral of indicatorConstLp(p ht hμt e) over the whole space equals μ.real t times e.
Русский
Пусть t ⊆ X измеримо, μ t ≠ ∞, и e ∈ E. Тогда интеграл indicatorConstLp(p ht hμt e) по всей области равен μ.real t умножить на e.
LaTeX
$$$$ \\int_X \\mathrm{indicatorConstLp}(p, ht, h\\mu t, e)(x) \\, d\\mu(x) = \\mu_{\\mathbb{R}}(t) \\; e $$$$
Lean4
theorem integral_indicatorConstLp [CompleteSpace E] {p : ℝ≥0∞} (ht : MeasurableSet t) (hμt : μ t ≠ ∞) (e : E) :
∫ x, indicatorConstLp p ht hμt e x ∂μ = μ.real t • e :=
calc
∫ x, indicatorConstLp p ht hμt e x ∂μ = ∫ x in univ, indicatorConstLp p ht hμt e x ∂μ := by rw [setIntegral_univ]
_ = μ.real (t ∩ univ) • e := (setIntegral_indicatorConstLp MeasurableSet.univ ht hμt e)
_ = μ.real t • e := by rw [inter_univ]
