Definition of mulExpNegMulSq and properties

mulExpNegMulSq is the mapping fun (ε : ℝ) (x : ℝ) => x * Real.exp (- (ε * x * x)). By composition, it 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) with useful boundedness and convergence properties.

Main Properties

• abs_mulExpNegMulSq_le: For fixed ε > 0, the mapping x ↦ mulExpNegMulSq ε x is bounded by Real.sqrt ε⁻¹;
• tendsto_mulExpNegMulSq: For fixed x : ℝ, the mapping mulExpNegMulSq ε x converges pointwise to x as ε → 0;
• lipschitzWith_one_mulExpNegMulSq: For fixed ε > 0, the mapping mulExpNegMulSq ε is Lipschitz with constant 1;
• abs_mulExpNegMulSq_comp_le_norm: For a fixed bounded continuous function g, the mapping mulExpNegMulSq ε ∘ g is bounded by norm g, uniformly in ε ≥ 0;

Definition and properties of fun x => x * Real.exp (- (ε * x * x))

noncomputable def Real.mulExpNegMulSq (ε x : ℝ) : ℝ

Mapping fun ε x => x * Real.exp (- (ε * x * x)). By composition, it can be used to transform functions into bounded functions.

theorem Real.mulExpNegSq_apply (ε x : ℝ) : ε.mulExpNegMulSq x = x * exp (-(ε * x * x))

theorem Real.neg_mulExpNegMulSq_neg (ε x : ℝ) : -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x

theorem Real.mulExpNegMulSq_one_le_one (x : ℝ) : mulExpNegMulSq 1 x ≤ 1

theorem Real.neg_one_le_mulExpNegMulSq_one (x : ℝ) : -1 ≤ mulExpNegMulSq 1 x

theorem Real.abs_mulExpNegMulSq_one_le_one (x : ℝ) : |mulExpNegMulSq 1 x| ≤ 1

theorem Real.continuous_mulExpNegMulSq {ε : ℝ} : Continuous fun (x : ℝ) => ε.mulExpNegMulSq x

theorem Continuous.mulExpNegMulSq {ε : ℝ} {α : Type u_1} [TopologicalSpace α] {f : α → ℝ} (hf : Continuous f) : Continuous fun (x : α) => ε.mulExpNegMulSq (f x)

theorem Real.differentiableAt_mulExpNegMulSq {ε : ℝ} (y : ℝ) : DifferentiableAt ℝ ε.mulExpNegMulSq y

theorem Real.differentiable_mulExpNegMulSq {ε : ℝ} : Differentiable ℝ ε.mulExpNegMulSq

theorem Real.hasDerivAt_mulExpNegMulSq {ε : ℝ} (y : ℝ) : HasDerivAt ε.mulExpNegMulSq (exp (-(ε * y * y)) + y * (exp (-(ε * y * y)) * (-2 * ε * y))) y

theorem Real.deriv_mulExpNegMulSq {ε : ℝ} (y : ℝ) : deriv ε.mulExpNegMulSq y = exp (-(ε * y * y)) + y * (exp (-(ε * y * y)) * (-2 * ε * y))

theorem Real.norm_deriv_mulExpNegMulSq_le_one {ε : ℝ} (hε : 0 < ε) (x : ℝ) : ‖deriv ε.mulExpNegMulSq x‖ ≤ 1

theorem Real.nnnorm_deriv_mulExpNegMulSq_le_one {ε : ℝ} (hε : 0 < ε) (x : ℝ) : ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

theorem Real.lipschitzWith_one_mulExpNegMulSq {ε : ℝ} (hε : 0 < ε) : LipschitzWith 1 ε.mulExpNegMulSq

For fixed ε > 0, the mapping mulExpNegMulSq ε is Lipschitz with constant 1

theorem Real.mulExpNegMulSq_eq_sqrt_mul_mulExpNegMulSq_one {ε : ℝ} (hε : 0 < ε) (x : ℝ) : ε.mulExpNegMulSq x = (√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)

theorem Real.abs_mulExpNegMulSq_le {ε : ℝ} (hε : 0 < ε) {x : ℝ} : |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

For fixed ε > 0, the mapping x ↦ mulExpNegMulSq ε x is bounded by `(√ε)⁻¹

theorem Real.dist_mulExpNegMulSq_le_two_mul_sqrt {ε : ℝ} (hε : 0 < ε) (x y : ℝ) : dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

theorem Real.dist_mulExpNegMulSq_le_dist {ε : ℝ} (hε : 0 < ε) {x y : ℝ} : dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

theorem Real.tendsto_mulExpNegMulSq {x : ℝ} : Filter.Tendsto (fun (ε : ℝ) => ε.mulExpNegMulSq x) (nhds 0) (nhds x)

For fixed x : ℝ, the mapping mulExpNegMulSq ε x converges pointwise to x as ε → 0

theorem Real.abs_mulExpNegMulSq_comp_le_norm {ε : ℝ} {E : Type u_1} [TopologicalSpace E] {x : E} (g : BoundedContinuousFunction E ℝ) (hε : 0 ≤ ε) : |(ε.mulExpNegMulSq ∘ ⇑g) x| ≤ ‖g‖

For a fixed bounded function g, mulExpNegMulSq ε ∘ g is bounded by norm g, uniformly in ε ≥ 0.