English
The integral is invariant under commutative transformations of Lp spaces with appropriate maps.
Русский
Интеграл сохраняется при совместном преобразовании пространств Lp.
LaTeX
$$$\\int L(φ(x)) dμ = L(\\int φ(x) dμ)$$$
Lean4
theorem integral_trim (hm : m ≤ m0) {f : β → G} (hf : StronglyMeasurable[m] f) : ∫ x, f x ∂μ = ∫ x, f x ∂μ.trim hm :=
by
by_cases hG : CompleteSpace G; swap
· simp [integral, hG]
borelize G
by_cases hf_int : Integrable f μ
swap
· have hf_int_m : ¬Integrable f (μ.trim hm) := fun hf_int_m => hf_int (integrable_of_integrable_trim hm hf_int_m)
rw [integral_undef hf_int, integral_undef hf_int_m]
haveI : SeparableSpace (range f ∪ {0} : Set G) := hf.separableSpace_range_union_singleton
let f_seq := @SimpleFunc.approxOn G β _ _ _ m _ hf.measurable (range f ∪ {0}) 0 (by simp) _
have hf_seq_meas : ∀ n, StronglyMeasurable[m] (f_seq n) := fun n => @SimpleFunc.stronglyMeasurable β G m _ (f_seq n)
have hf_seq_int : ∀ n, Integrable (f_seq n) μ := SimpleFunc.integrable_approxOn_range (hf.mono hm).measurable hf_int
have hf_seq_int_m : ∀ n, Integrable (f_seq n) (μ.trim hm) := fun n => (hf_seq_int n).trim hm (hf_seq_meas n)
have hf_seq_eq : ∀ n, ∫ x, f_seq n x ∂μ = ∫ x, f_seq n x ∂μ.trim hm := fun n =>
integral_trim_simpleFunc hm (f_seq n) (hf_seq_int n)
have h_lim_1 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ)) :=
by
refine tendsto_integral_of_L1 f hf_int (Eventually.of_forall hf_seq_int) ?_
exact SimpleFunc.tendsto_approxOn_range_L1_enorm (hf.mono hm).measurable hf_int
have h_lim_2 : atTop.Tendsto (fun n => ∫ x, f_seq n x ∂μ) (𝓝 (∫ x, f x ∂μ.trim hm)) :=
by
simp_rw [hf_seq_eq]
refine
@tendsto_integral_of_L1 β G _ _ m (μ.trim hm) _ f (hf_int.trim hm hf) _ _ (Eventually.of_forall hf_seq_int_m) ?_
exact @SimpleFunc.tendsto_approxOn_range_L1_enorm β G m _ _ _ f _ _ hf.measurable (hf_int.trim hm hf)
exact tendsto_nhds_unique h_lim_1 h_lim_2
