integral_continuousLinearMap_prod'

English

If id maps are integrable with μ and ν, then L is integrable on μ×ν.

Русский

Если интегрируемы функции единицы по μ и ν, то L интегрируемо по произведению.

LaTeX

$$$$\\text{Integrable } L \\ (μ×ν)$$$$

Lean4

theorem integral_continuousLinearMap_prod' (hLμ : Integrable (L.comp (.inl ℝ E F)) μ)
    (hLν : Integrable (L.comp (.inr ℝ E F)) ν) :
    ∫ p, L p ∂(μ.prod ν) = ∫ x, L.comp (.inl ℝ E F) x ∂μ + ∫ y, L.comp (.inr ℝ E F) y ∂ν :=
  by
  simp_rw [← L.comp_inl_add_comp_inr]
  replace hLμ := ((memLp_one_iff_integrable.mpr hLμ).comp_fst ν).integrable le_rfl
  replace hLν := ((memLp_one_iff_integrable.mpr hLν).comp_snd μ).integrable le_rfl
  rw [integral_add hLμ hLν, integral_prod _ hLμ, integral_prod _ hLν]
  simp

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