Properties of the integral of mulExpNegMulSq

The mapping mulExpNegMulSq can be used to transform a function g : E → ℝ into a bounded function mulExpNegMulSq ε ∘ g : E → ℝ = fun x => g x * Real.exp (-ε * g x * g x). This file contains results on the integral of mulExpNegMulSq g ε with respect to a finite measure P.

Lemmas

• tendsto_integral_mulExpNegMulSq_comp: By the dominated convergence theorem and mulExpNegMulSq_abs_le_norm, the integral of mulExpNegMulSq ε ∘ g with respect to a finite measure P converges to the integral of g, as ε → 0;
• tendsto_integral_mul_one_add_inv_smul_sq_pow: 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, fun x => (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x. This allows to transfer properties of a subalgebra of functions containing g to the function mulExpNegMulSq ε ∘ g, see e.g. integral_mulExpNegMulSq_comp_eq.

Main Result

dist_integral_mulExpNegMulSq_comp_le: For a subalgebra of functions A, if for any g ∈ A the integral 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 * √ε. This is a key ingredient in the proof of theorem ext_of_forall_mem_subalgebra_integral_eq, where it is shown that a subalgebra of functions that separates points separates finite measures.

theorem integrable_mulExpNegMulSq_comp {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (f : C(E, ℝ)) (hε : 0 < ε) : MeasureTheory.Integrable (fun (x : E) => ε.mulExpNegMulSq (f x)) P

theorem integrable_mulExpNegMulSq_comp_restrict_of_isCompact {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {K : Set E} (hK : IsCompact K) (hKmeas : MeasurableSet K) (g : C(E, ℝ)) : MeasureTheory.Integrable (fun (x : E) => ε.mulExpNegMulSq (g x)) (P.restrict K)

theorem tendsto_integral_mulExpNegMulSq_comp {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] (g : BoundedContinuousFunction E ℝ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P) (nhdsWithin 0 (Set.Ioi 0)) (nhds (∫ (x : E), g x ∂P))

The integral of mulExpNegMulSq ε ∘ g with respect to a finite measure P converges to the integral of g, as ε → 0 from above.

theorem tendsto_integral_mul_one_add_inv_smul_sq_pow {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (g : BoundedContinuousFunction E ℝ) (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) Filter.atTop (nhds (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P))

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.

@[deprecated tendsto_integral_mul_one_add_inv_smul_sq_pow (since := "2025-05-22")]

theorem tendsto_integral_mul_one_plus_inv_smul_sq_pow {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (g : BoundedContinuousFunction E ℝ) (hε : 0 < ε) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : E), (g * (1 + (↑n)⁻¹ • -(ε • g * g)) ^ n) x ∂P) Filter.atTop (nhds (∫ (x : E), ε.mulExpNegMulSq (g x) ∂P))

Alias of tendsto_integral_mul_one_add_inv_smul_sq_pow.

---

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 integral_mulExpNegMulSq_comp_eq {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P'] {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)} (hε : 0 < ε) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') {g : BoundedContinuousFunction E ℝ} (hgA : g ∈ A) : ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P = ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P'

theorem abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} (f : C(E, ℝ)) {K : Set E} (hK : MeasurableSet K) (hε : 0 < ε) (hKP : P Kᶜ < ↑ε.toNNReal) : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε

theorem abs_setIntegral_mulExpNegMulSq_comp_sub_le_mul_measure {E : Type u_1} [TopologicalSpace E] [MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {K : Set E} (hK : IsCompact K) (hKmeas : MeasurableSet K) (f g : C(E, ℝ)) {δ : ℝ} (hε : 0 < ε) (hfg : ∀ x ∈ K, |g x - f x| < δ) : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| ≤ δ * (P K).toReal

theorem dist_integral_mulExpNegMulSq_comp_le {ε : ℝ} {E : Type u_2} [MeasurableSpace E] [PseudoEMetricSpace E] [BorelSpace E] [CompleteSpace E] [SecondCountableTopology E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P] [MeasureTheory.IsFiniteMeasure P'] (f : BoundedContinuousFunction E ℝ) {A : Subalgebra ℝ (BoundedContinuousFunction E ℝ)} (hA : (Subalgebra.map (BoundedContinuousFunction.toContinuousMapₐ ℝ) A).SeparatesPoints) (heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') (hε : 0 < ε) : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

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 * √ε.