English
For any P, P' finite measures and any ε > 0, bounds hold so that integrals of ε.mulExpNegMulSq with bounded continuous functions agree if their integrals agree for all bounded continuous functions in a subalgebra.
Русский
При конечных мерах P, P' и любом ε > 0 интегралы ε⋅mulExpNegMulSq от ограниченно непрерывных функций совпадают при условии равенства интегралов для всех таких функций в подалгебре.
LaTeX
$$$\\forall (P, P')\\text{ finite measures}, \\forall ε>0, \\forall A\\le (bounded\\;continuous\\;functions),\\; \\text{Eq} (\\int mulExpNegMulSq(ε, g)) (\\int mulExpNegMulSq(ε, g))$$$
Lean4
theorem integral_mulExpNegMulSq_comp_eq {P' : Measure E} [IsFiniteMeasure P'] {A : Subalgebra ℝ (E →ᵇ ℝ)} (hε : 0 < ε)
(heq : ∀ g ∈ A, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P') {g : E →ᵇ ℝ} (hgA : g ∈ A) :
∫ x, mulExpNegMulSq ε (g x) ∂P = ∫ x, mulExpNegMulSq ε (g x) ∂P' :=
by
have one_add_inv_mul_mem (n : ℕ) : g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n ∈ A :=
by
apply Subalgebra.mul_mem A hgA (Subalgebra.pow_mem A _ n)
apply Subalgebra.add_mem A (Subalgebra.one_mem A) (Subalgebra.smul_mem A _ n⁻¹)
exact Subalgebra.neg_mem A (Subalgebra.mul_mem A (Subalgebra.smul_mem A hgA ε) hgA)
have limP :
Tendsto (fun n : ℕ => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
(𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P')) :=
by
rw [funext fun n => heq _ (one_add_inv_mul_mem n)]
exact tendsto_integral_mul_one_add_inv_smul_sq_pow g hε
exact tendsto_nhds_unique (tendsto_integral_mul_one_add_inv_smul_sq_pow g hε) limP
