eval_integral_piLp — Mathlib

English

A simplified equivalence for integrability of PiLp-valued functions and their coordinates.

Русский

Упрощённое равносильное условие интегрируемости для функций с значением в PiLp и их координат.

LaTeX

$$$$\\text{Integrable}(f,\\mu) \\iff \\forall i, \\text{Integrable}(f\\cdot i,\\mu).$$$$

Lean4

theorem eval_integral_piLp (hf : ∀ i, Integrable (f · i) μ) (i : ι) : (∫ x, f x ∂μ) i = ∫ x, f x i ∂μ :=
  by
  rw [← PiLp.proj_apply (𝕜 := ℝ) q E i (∫ x, f x ∂μ), ← ContinuousLinearMap.integral_comp_comm]
  · simp
  exact Integrable.of_eval_piLp hf

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