continuous_integral_comp_L1 — Mathlib

English

The integral mapping φ ↦ ∫ φ is continuous when viewed as a function into Lp spaces.

Русский

Отображение интеграла непрерывно относително φ в пространства Lp.

LaTeX

$$Continuous$$

Lean4

theorem continuous_integral_comp_L1 (L : E →SL[σ] F) : Continuous fun φ : X →₁[μ] E => ∫ x : X, L (φ x) ∂μ := by
  rw [← funext L.integral_compLp]; exact continuous_integral.comp (L.compLpL 1 μ).continuous

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