continuous_setIntegral — Mathlib

English

The a.e. value of the restricting CLM coincides with the restricted function almost everywhere.

Русский

Значение а.e. ограничивающего CLM совпадает почти повсюду с ограниченной функцией.

LaTeX

$$$$\\text{ae}_{μ|_s}(\\text{CLM}(f)) = f|_s$$$$

Lean4

@[continuity]
theorem continuous_setIntegral [NormedSpace ℝ E] (s : Set X) : Continuous fun f : X →₁[μ] E => ∫ x in s, f x ∂μ :=
  by
  haveI : Fact ((1 : ℝ≥0∞) ≤ 1) := ⟨le_rfl⟩
  have h_comp :
    (fun f : X →₁[μ] E => ∫ x in s, f x ∂μ) = integral (μ.restrict s) ∘ fun f => LpToLpRestrictCLM X E ℝ μ 1 s f :=
    by
    ext1 f
    rw [Function.comp_apply, integral_congr_ae (LpToLpRestrictCLM_coeFn ℝ s f)]
  rw [h_comp]
  exact continuous_integral.comp (LpToLpRestrictCLM X E ℝ μ 1 s).continuous

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