integrable_comp_eval — Mathlib

English

For finite index, the integral of the product equals the product of the integrals of f_i with respect to μ_i, raised to the cardinality of ι.

Русский

Для конечного индекса ∫ произведение равно произведению интегралов f_i, возведенным в card(ι).

LaTeX

$$$$\\int x:ι\\to E,\\; \\prod_i f_i(x_i)\\,d(\\pi\\mu)=\\prod_i\\int x, f_i(x)\\,d(\\mu_i).$$$$

Lean4

theorem integrable_comp_eval [∀ i, IsFiniteMeasure (μ i)] {i : ι} {f : X i → E} (hf : Integrable f (μ i)) :
    Integrable (fun x ↦ f (x i)) (Measure.pi μ) :=
  by
  refine Integrable.comp_measurable ?_ (by fun_prop)
  classical
  rw [Measure.pi_map_eval]
  exact hf.smul_measure <| ENNReal.prod_ne_top (by finiteness)

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