English
Let f be a bounded continuous function on E. Suppose a separating subalgebra A of bounded continuous functions exists such that integrals ∫ f dP and ∫ f dP′ coincide for all g ∈ A, and let ε > 0. Then the difference |∫ mulExpNegMulSq(ε, f) dP − ∫ mulExpNegMulSq(ε, f) dP′| is bounded by 6√ε.
Русский
Пусть f - ограниченная непрерывная функция на E. Пусть существует разделяющая подалгебра A из BAB функций; если для всех g ∈ A интегралы ∫ g dP совпадают с ∫ g dP′, и ε > 0, то разность интегралов с mulExpNegMulSq(ε, f) по P и P′ не превосходит 6√ε.
LaTeX
$$$\\left| \\int_E mulExpNegMulSq(\\varepsilon, f(x)) \\, dP - \\int_E mulExpNegMulSq(\\varepsilon, f(x)) \\, dP' \\right| \\le 6 \\sqrt{\\varepsilon}$$$
Lean4
/-- If for any `g ∈ A` the integrals with respect to two finite measures `P, P'` coincide, then the
difference of the integrals of `mulExpNegMulSq ε ∘ g` with respect to `P, P'` is bounded by
`6 * √ε`. -/
theorem dist_integral_mulExpNegMulSq_comp_le (f : E →ᵇ ℝ) {A : Subalgebra ℝ (E →ᵇ ℝ)}
(hA : (A.map (toContinuousMapₐ ℝ)).SeparatesPoints) (heq : ∀ g ∈ A, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P')
(hε : 0 < ε) : |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x, mulExpNegMulSq ε (f x) ∂P'| ≤ 6 * √ε := by
-- if both measures are zero, the result is trivial
by_cases hPP' : P = 0 ∧ P' = 0
·
simp only [hPP', integral_zero_measure, sub_self, abs_zero, Nat.ofNat_pos, mul_nonneg_iff_of_pos_left,
(le_of_lt (sqrt_pos_of_pos hε))]
let const : ℝ := (max (P.real Set.univ) (P'.real Set.univ))
have pos_of_measure : 0 < const := by
rw [not_and_or] at hPP'
rcases hPP' with hP0 | hP'0
· exact lt_max_of_lt_left (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP0) (measure_ne_top P Set.univ))
·
exact
lt_max_of_lt_right
(toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (measure_ne_top P' Set.univ))
-- obtain K, a compact and closed set, which covers E up to a small area of measure at most ε
-- w.r.t. both P and P'
obtain ⟨KP, _, hKPco, hKPcl, hKP⟩ :=
MeasurableSet.exists_isCompact_isClosed_diff_lt (MeasurableSet.univ) (measure_ne_top P Set.univ)
(ne_of_gt (ofReal_pos.mpr hε))
obtain ⟨KP', _, hKP'co, hKP'cl, hKP'⟩ :=
MeasurableSet.exists_isCompact_isClosed_diff_lt (MeasurableSet.univ) (measure_ne_top P' Set.univ)
(ne_of_gt (ofReal_pos.mpr hε))
let K := KP ∪ KP'
have hKco := IsCompact.union hKPco hKP'co
have hKcl := IsClosed.union hKPcl hKP'cl
simp only [← Set.compl_eq_univ_diff] at hKP hKP'
have hKPbound : P (KP ∪ KP')ᶜ < ε.toNNReal :=
lt_of_le_of_lt (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_left))) hKP
have hKP'bound : P' (KP ∪ KP')ᶜ < ε.toNNReal :=
lt_of_le_of_lt (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_right))) hKP'
obtain ⟨g', hg'A, hg'approx⟩ :=
ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints hA f hKco
(Left.mul_pos (sqrt_pos_of_pos hε) (inv_pos_of_pos pos_of_measure))
simp only [Subalgebra.mem_map] at hg'A
let g := hg'A.choose
have hgA : g ∈ A := hg'A.choose_spec.1
have hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹ :=
by
rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]
exact hg'approx
have line1 : |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| < √ε :=
abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt f (IsClosed.measurableSet hKcl) hε hKPbound
have line3 : |∫ x in K, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P| < √ε :=
by
rw [abs_sub_comm]
exact (abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt g (IsClosed.measurableSet hKcl) hε hKPbound)
have line5 : |∫ x, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (g x) ∂P'| < √ε :=
(abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt g (IsClosed.measurableSet hKcl) hε hKP'bound)
have line7 : |∫ x in K, mulExpNegMulSq ε (f x) ∂P' - ∫ x, mulExpNegMulSq ε (f x) ∂P'| < √ε :=
by
rw [abs_sub_comm]
exact (abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt f (IsClosed.measurableSet hKcl) hε hKP'bound)
have line2 : |∫ x in K, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (g x) ∂P| ≤ √ε :=
by
rw [abs_sub_comm]
apply
le_trans
(abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure hKco (IsClosed.measurableSet hKcl) f g hε hgapprox)
rw [mul_assoc]
apply mul_le_of_le_one_right (le_of_lt (sqrt_pos_of_pos hε))
apply inv_mul_le_one_of_le₀ (le_max_of_le_left _) (le_of_lt pos_of_measure)
exact (toReal_le_toReal (measure_ne_top P _) (measure_ne_top P _)).mpr (measure_mono (Set.subset_univ _))
have line6 : |∫ x in K, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (f x) ∂P'| ≤ √ε :=
by
apply
le_trans
(abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure hKco (IsClosed.measurableSet hKcl) f g hε hgapprox)
rw [mul_assoc]
apply mul_le_of_le_one_right (le_of_lt (sqrt_pos_of_pos hε))
apply inv_mul_le_one_of_le₀ (le_max_of_le_right _) (le_of_lt pos_of_measure)
exact (toReal_le_toReal (measure_ne_top P' _) (measure_ne_top P' _)).mpr (measure_mono (Set.subset_univ _))
have line4 : |∫ x, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P'| = 0 :=
by
rw [abs_eq_zero, sub_eq_zero]
exact integral_mulExpNegMulSq_comp_eq hε heq hgA
calc
|∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x, mulExpNegMulSq ε (f x) ∂P'| ≤
|∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| +
|∫ x in K, mulExpNegMulSq ε (f x) ∂P - ∫ x in K, mulExpNegMulSq ε (g x) ∂P| +
|∫ x in K, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P| +
|∫ x, mulExpNegMulSq ε (g x) ∂P - ∫ x, mulExpNegMulSq ε (g x) ∂P'| +
|∫ x, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (g x) ∂P'| +
|∫ x in K, mulExpNegMulSq ε (g x) ∂P' - ∫ x in K, mulExpNegMulSq ε (f x) ∂P'| +
|∫ x in K, mulExpNegMulSq ε (f x) ∂P' - ∫ x, mulExpNegMulSq ε (f x) ∂P'| :=
@dist_triangle8 ℝ _ _ _ _ _ _ _ _ _
_ ≤ 6 * √ε := by linarith
