English
If L is a linear operator and φ lies in Lp, then ∫ x (L ∘ φ) = ∫ x L(φ(x)).
Русский
Если L линейный орт, то интеграл от L ∘ φ равен интегралу от L(φ(x)).
LaTeX
$$$\\int (L(φ(x))) dμ = \\int L(φ(x)) dμ$$$
Lean4
theorem integral_comp_commSL [CompleteSpace E] (hσ : ∀ (r : ℝ) (x : 𝕜), σ (r • x) = r • σ x) (L : E →SL[σ] F)
{φ : X → E} (φ_int : Integrable φ μ) : ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ) :=
by
apply φ_int.induction (P := fun φ => ∫ x, L (φ x) ∂μ = L (∫ x, φ x ∂μ))
· intro e s s_meas _
rw [integral_indicator_const e s_meas, ← @smul_one_smul E ℝ 𝕜 _ _ _ _ _ (μ.real s) e,
ContinuousLinearMap.map_smulₛₗ, hσ, map_one, smul_assoc, one_smul, ← integral_indicator_const (L e) s_meas]
congr 1 with a
rw [← Function.comp_def L, Set.indicator_comp_of_zero L.map_zero, Function.comp_apply]
· intro f g _ f_int g_int hf hg
simp [L.map_add, integral_add (μ := μ) f_int g_int,
integral_add (μ := μ) (L.integrable_comp f_int) (L.integrable_comp g_int), hf, hg]
· exact isClosed_eq L.continuous_integral_comp_L1 (L.continuous.comp continuous_integral)
· intro f g hfg _ hf
convert hf using 1 <;> clear hf
· exact integral_congr_ae (hfg.fun_comp L).symm
· rw [integral_congr_ae hfg.symm]
