setIntegral_tsupport — Mathlib

English

When integrating a Bochner function over the tsupport of the function, the integral equals the integral over the whole domain.

Русский

При интегрировании по tsupport функции Боchner интеграл по tsupport равен интегралу по всей области.

LaTeX

$$$$\\int_{x \\in tsupport F} F(x)\\,d\\nu = \\int_X F(x)\\,d\\nu.$$$$

Lean4

theorem setIntegral_tsupport [TopologicalSpace X] : ∫ x in tsupport F, F x ∂ν = ∫ x, F x ∂ν :=
  by
  nth_rw 2 [← setIntegral_univ]
  rw [setIntegral_eq_of_subset_of_forall_diff_eq_zero MeasurableSet.univ (subset_univ (tsupport F))]
  exact fun _ hx => image_eq_zero_of_notMem_tsupport <| notMem_of_mem_diff hx

Похожие утверждения