tendsto_integral_mul_one_add_inv_smul_sq_pow

English

Let g be a bounded measurable map; as ε → 0+, certain adjusted integrals with powers converge to the integral of ε.mulExpNegMulSq(g).

Русский

Пусть g — ограниченная плавная функция. Тогда соответствующие интегралы с модификациями экспоненты сходятся к интегралу ε⋅mulExpNegMulSq(g).

LaTeX

$$$\\text{Tendsto}\\bigl(\\lambda \\varepsilon. \\int_E g(x) \\bigl(1 + (n^{−1}) \\cdot (-(\\varepsilon) g(x)^2)\\bigr)^n \\, dP\\bigr)_{n\\to\\infty} \\to \\int_E (\\varepsilon \\ mulExpNegMulSq (g(x)))\\, dP$$$

Lean4

/-- The integral of `mulExpNegMulSq ε ∘ g` with respect to a finite measure `P` can be
approximated by the integral of the sequence approximating the exponential function. -/
theorem tendsto_integral_mul_one_add_inv_smul_sq_pow (g : E →ᵇ ℝ) (hε : 0 < ε) :
    Tendsto (fun (n : ℕ) => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
      (𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P)) :=
  by
  apply tendsto_integral_filter_of_norm_le_const ?h_meas ?h_bound ?h_lim
  · apply Eventually.of_forall
    exact fun n =>
      StronglyMeasurable.aestronglyMeasurable
        (Continuous.stronglyMeasurable (Continuous.mul g.continuous ((1 + ((n : ℝ)⁻¹ • -(ε • g * g))) ^ n).continuous))
  · obtain ⟨N, hgN⟩ := exists_nat_gt (ε * (norm g * norm g))
    use norm g
    rw [eventually_atTop]
    use N
    intro n hn
    have hnpos : 0 < (n : ℝ) :=
      by
      apply lt_of_lt_of_le (lt_of_le_of_lt _ hgN) (Nat.cast_le.mpr hn)
      exact (mul_nonneg (le_of_lt hε) (mul_self_nonneg (norm g)))
    apply Eventually.of_forall
    intro x
    simp only [smul_neg, BoundedContinuousFunction.coe_mul, Pi.mul_apply, pow_apply, BoundedContinuousFunction.coe_add,
      BoundedContinuousFunction.coe_one, coe_neg, BoundedContinuousFunction.coe_smul, smul_eq_mul, Pi.add_apply,
      Pi.one_apply, Pi.neg_apply, norm_mul, norm_eq_abs, norm_pow]
    refine
      (mul_le_mul_of_nonneg_right (norm_coe_le_norm g x) (pow_nonneg (abs_nonneg _) n)).trans <|
        mul_le_of_le_one_right (norm_nonneg _) ?_
    apply pow_le_one₀ (abs_nonneg _)
    rw [mul_assoc, inv_mul_eq_div, abs_le]
    refine
      ⟨?_,
        (add_le_iff_nonpos_right 1).mpr
          (Left.neg_nonpos_iff.mpr (div_nonneg (mul_nonneg (le_of_lt hε) (mul_self_nonneg (g x))) (le_of_lt hnpos)))⟩
    apply le_trans (by linarith) (sub_nonneg_of_le ((div_le_one hnpos).mpr _))
    apply le_trans (le_trans _ (le_of_lt hgN)) (Nat.cast_le.mpr hn)
    apply mul_le_mul (Preorder.le_refl ε) _ (mul_self_nonneg (g x)) (le_of_lt hε)
    rw [← abs_le_iff_mul_self_le, abs_norm]
    exact norm_coe_le_norm g x
  · apply Eventually.of_forall
    intro x
    apply Tendsto.const_mul (g x)
    simpa [mul_assoc, inv_mul_eq_div, ← neg_div] using tendsto_one_add_div_pow_exp (-(ε * (g x * g x)))

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