fst_integral_withLp — Mathlib

English

If f ∈ L^1 with values in WithLp q (E × F), then the second coordinate of the integral equals the integral of the second coordinate function.

Русский

Если f ∈ L^1 для WithLp q (E × F), то вторая компонента интеграла равна интегралу второй координаты.

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\Rightarrow \\Bigl(\\int x\\, f(x)\\,d\\mu\\Bigr)_{\\mathrm{snd}} = \\int x\\, (f(x))_{\\mathrm{snd}}\\,d\\mu.$$$$

Lean4

theorem fst_integral_withLp [CompleteSpace F] (hf : Integrable f μ) : (∫ x, f x ∂μ).fst = ∫ x, (f x).fst ∂μ :=
  by
  rw [← WithLp.ofLp_fst]
  conv => enter [1, 1]; change WithLp.prodContinuousLinearEquiv q ℝ E F _
  rw [← ContinuousLinearEquiv.integral_comp_comm, fst_integral]
  · rfl
  · exact (ContinuousLinearEquiv.integrable_comp_iff _).2 hf

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