Physlib.Mathematics.InnerProductSpace.Gaussian

Imports

/-
Copyright (c) 2026 Gregory J. Loges. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gregory J. Loges
-/
module

public import Mathlib.Analysis.Calculus.ContDiff.Bounds
public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
public import Mathlib.Analysis.InnerProductSpace.Calculus
public import Mathlib.Analysis.SpecialFunctions.ExpDeriv
public import Physlib.Meta.TODO.Basic

Gaussians in inner product spaces

i. Overview

In this module we define Gaussians as Schwartz maps in general inner product spaces.

The most general Gaussian constructed is exp (-2⁻¹ * ‖B⁻¹ (x - x₀)‖ ^ 2) (mean x₀ and covariance BᵀB) as a Schwartz map 𝓢(E, 𝕜), where B : D ≃L[ℝ] E is a linear equivalence of inner product spaces. This is accomplished by first constructing the Gaussian exp (-2⁻¹ * ‖x‖ ^ 2) as a Schwartz map 𝓢(E, ℝ) using explicit bounds on the derivatives of ‖x‖ ^ 2 = innerSL ℝ x x and limiting properties of the real exponential, then composing with an invertible affine transformation.

The Gaussians are left unnormalized since the appropriate condition will depend on context and whether E is finite- or infinite-dimensional. For example, the normalization conditions when interpreted as a probability density function vs. as a quantum state require different pre-factors.

For some relevant Gaussian integrals see Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.

ii. Key results

gaussian 𝕜 B x₀ : Given a linear equivalence B : D ≃L[ℝ] E and mean x₀ : E, the Gaussian exp (-2⁻¹ * ‖B⁻¹ (x - x₀)‖ ^ 2) centered on x₀ as a Schwartz map 𝓢(E, 𝕜).

gaussian₀ 𝕜 B : Given a linear equivalence B : D ≃L[ℝ] E of inner product spaces, the Gaussian exp (-2⁻¹ * ‖B⁻¹ x‖ ^ 2) centered on the origin as a Schwartz map 𝓢(E, 𝕜).

stdGaussian E 𝕜 : The standard Gaussian exp (-2⁻¹ * ‖x‖ ^ 2) as a Schwartz map 𝓢(E, 𝕜).

iii. Table of contents

A. Standard, real-valued

B. General, RCLike-valued

iv. References

@[expose] public section

TODO "Provide functionality for multiplying by exponential functions like `exp ⟪v, x⟫`
  (which does not have temperate growth) to obtain another Schwartz map (smulLeftExp?)
  and prove that this is equal to a shifted/rescaled Gaussian with the same covariance."

A. Standard, real-valued

Crude bounds on the norms of iterated Fréchet derivatives of innerSL ℝ in the form required by norm_iteratedFDeriv_comp_le.


private lemma norm_iteratedFDeriv_innerSL_le_pow {n : ℕ} (hn : 1 ≤ n) :
    ‖iteratedFDeriv ℝ n (fun x : E ↦ innerSL ℝ x x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n := byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ n⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
  have h_id₁ : ‖iteratedFDeriv ℝ 1 id x‖ ≤ 1 := by simp [norm_id_le]E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ nE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
  have h_id : ∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0 := by
    intro k hkE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ ‖iteratedFDeriv ℝ k id x‖ = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
    rw [show k = k - 2 + 2 byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ n⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ nE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ iteratedFDeriv ℝ (k - 2 + 2) id x = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n omegaAll goals completed! 🐙E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ iteratedFDeriv ℝ (k - 2 + 2) id x = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n, norm_eq_zeroE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ iteratedFDeriv ℝ (k - 2 + 2) id x = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ iteratedFDeriv ℝ (k - 2 + 2) id x = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n]E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2⊢ iteratedFDeriv ℝ (k - 2 + 2) id x = 0E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
    extE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1k:ℕhk:k ≥ 2x✝:Fin (k - 2 + 2) → E⊢ (iteratedFDeriv ℝ (k - 2 + 2) id x) x✝ = 0 x✝E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
    simp [iteratedFDeriv_succ_apply_right]E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ nE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n
  calc
    _ ≤ ∑ k ∈ Finset.range (n + 1),
        n.choose k * ‖iteratedFDeriv ℝ k id x‖ * ‖iteratedFDeriv ℝ (n - k) id x‖ :=
      (innerSL ℝ).norm_iteratedFDeriv_le_of_bilinear_of_le_one
        contDiff_id contDiff_id x (Nat.cast_le.mpr n.le_succ) (norm_innerSL_le ℝ)
    _ = n.choose 0 * ‖iteratedFDeriv ℝ 0 id x‖ * ‖iteratedFDeriv ℝ (n - 0) id x‖ +
        n.choose 1 * ‖iteratedFDeriv ℝ 1 id x‖ * ‖iteratedFDeriv ℝ (n - 1) id x‖ := byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ∑ k ∈ Finset.range (n + 1), ↑(n.choose k) * ‖iteratedFDeriv ℝ k id x‖ * ‖iteratedFDeriv ℝ (n - k) id x‖ =
  ↑(n.choose 0) * ‖iteratedFDeriv ℝ 0 id x‖ * ‖iteratedFDeriv ℝ (n - 0) id x‖ +
    ↑(n.choose 1) * ‖iteratedFDeriv ℝ 1 id x‖ * ‖iteratedFDeriv ℝ (n - 1) id x‖
      refine Finset.sum_eq_add_of_mem 0 1 ?_ ?_ zero_ne_one fun k hk hk₀₁ ↦ ?_refine_1E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ 0 ∈ Finset.range (n + 1)refine_2E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ 1 ∈ Finset.range (n + 1)refine_3E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0k:ℕhk:k ∈ Finset.range (n + 1)hk₀₁:k ≠ 0 ∧ k ≠ 1⊢ ↑(n.choose k) * ‖iteratedFDeriv ℝ k id x‖ * ‖iteratedFDeriv ℝ (n - k) id x‖ = 0
      ·refine_1E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ 0 ∈ Finset.range (n + 1) simpAll goals completed! 🐙
      ·refine_2E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ 1 ∈ Finset.range (n + 1) simp [Nat.zero_lt_of_lt hn]All goals completed! 🐙
      ·refine_3E:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0k:ℕhk:k ∈ Finset.range (n + 1)hk₀₁:k ≠ 0 ∧ k ≠ 1⊢ ↑(n.choose k) * ‖iteratedFDeriv ℝ k id x‖ * ‖iteratedFDeriv ℝ (n - k) id x‖ = 0 simp [h_id, hk₀₁, Nat.two_le_iff]All goals completed! 🐙
    _ ≤ ‖x‖ * ‖iteratedFDeriv ℝ n id x‖ + n.choose 1 * ‖iteratedFDeriv ℝ (n - 1) id x‖ := byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0⊢ ↑(n.choose 0) * ‖iteratedFDeriv ℝ 0 id x‖ * ‖iteratedFDeriv ℝ (n - 0) id x‖ +
    ↑(n.choose 1) * ‖iteratedFDeriv ℝ 1 id x‖ * ‖iteratedFDeriv ℝ (n - 1) id x‖ ≤
  ‖x‖ * ‖iteratedFDeriv ℝ n id x‖ + ↑(n.choose 1) * ‖iteratedFDeriv ℝ (n - 1) id x‖ boundAll goals completed! 🐙
  rcases (show n = 1 ∨ n = 2 ∨ 2 < n byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ n⊢ ‖iteratedFDeriv ℝ n (fun x => ((innerSL ℝ) x) x) x‖ ≤ (2 + ‖x‖ ^ 2) ^ n omegaAll goals completed! 🐙) with rfl | rfl | hn'
  ·calc.step.inlE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:Eh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn:1 ≤ 1⊢ ‖x‖ * ‖iteratedFDeriv ℝ 1 id x‖ + ↑(Nat.choose 1 1) * ‖iteratedFDeriv ℝ (1 - 1) id x‖ ≤ (2 + ‖x‖ ^ 2) ^ 1 refine le_trans (b := 2 * ‖x‖) ?_ (byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:Eh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn:1 ≤ 1⊢ 2 * ‖x‖ ≤ (2 + ‖x‖ ^ 2) ^ 1 nlinarithAll goals completed! 🐙)
    simp [← le_sub_iff_add_le, two_mul, mul_le_of_le_one_right, norm_id_le]All goals completed! 🐙
  ·calc.step.inr.inlE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:Eh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn:1 ≤ 2⊢ ‖x‖ * ‖iteratedFDeriv ℝ 2 id x‖ + ↑(Nat.choose 2 1) * ‖iteratedFDeriv ℝ (2 - 1) id x‖ ≤ (2 + ‖x‖ ^ 2) ^ 2 refine le_trans ?_ (le_trans (le_self_pow₀ one_le_two two_ne_zero) (byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:Eh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn:1 ≤ 2⊢ 2 ^ 2 ≤ (2 + ‖x‖ ^ 2) ^ 2 boundAll goals completed! 🐙))
    simp [h_id, norm_id_le]All goals completed! 🐙
  ·calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ ‖x‖ * ‖iteratedFDeriv ℝ n id x‖ + ↑(n.choose 1) * ‖iteratedFDeriv ℝ (n - 1) id x‖ ≤ (2 + ‖x‖ ^ 2) ^ n rw [h_id n (byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ n ≥ 2calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n omegaAll goals completed! 🐙calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n), h_id (n - 1) (byE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ n - 1 ≥ 2calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n omegaAll goals completed! 🐙calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n), mul_zero,calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 + ↑(n.choose 1) * 0 ≤ (2 + ‖x‖ ^ 2) ^ ncalc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n mul_zero,calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 + 0 ≤ (2 + ‖x‖ ^ 2) ^ ncalc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n add_zerocalc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ ncalc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n]calc.step.inr.inrE:Type u_2inst✝¹:NormedAddCommGroup Einst✝:InnerProductSpace ℝ Ex:En:ℕhn:1 ≤ nh_id₁:‖iteratedFDeriv ℝ 1 id x‖ ≤ 1h_id:∀ k ≥ 2, ‖iteratedFDeriv ℝ k id x‖ = 0hn':2 < n⊢ 0 ≤ (2 + ‖x‖ ^ 2) ^ n
    positivityAll goals completed! 🐙



private lemma pow_mul_exp_bddAbove {s : ℝ} (hs : 0 ≤ s) (n : ℕ) :
    ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C := bys:ℝhs:0 ≤ sn:ℕ⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  let b : ℝ → ℝ := fun x ↦ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  have hb : Continuous b := by fun_props:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous b⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ Cs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous b⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  have htop : Tendsto b atTop (nhds 0) := by
    let g : ℝ → ℝ := fun x : ℝ ↦ x ^ (s + n) * rexp (-2⁻¹ * x)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)⊢ Tendsto b atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
    let g' : ℝ → ℝ := fun x ↦ 2 + xs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto b atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
    refine tendsto_of_tendsto_of_tendsto_of_le_of_le' (g := 0) (h := exp 1 • g ∘ g') ?_ ?_ ?_ ?_refine_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto 0 atTop (nhds 0)refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (rexp 1 • g ∘ g') atTop (nhds 0)refine_3s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ ∀ᶠ (b_1 : ℝ) in atTop, 0 b_1 ≤ b b_1refine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ ∀ᶠ (b_1 : ℝ) in atTop, b b_1 ≤ (rexp 1 • g ∘ g') b_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
    ·refine_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto 0 atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C exact tendsto_const_nhdsAll goals completed! 🐙s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
    ·refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (rexp 1 • g ∘ g') atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C rw [← smul_zero (exp 1)refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (rexp 1 • g ∘ g') atTop (nhds (rexp 1 • 0))refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (rexp 1 • g ∘ g') atTop (nhds (rexp 1 • 0))s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C]refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (rexp 1 • g ∘ g') atTop (nhds (rexp 1 • 0))s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      refine Tendsto.const_smul ?_ _refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto (g ∘ g') atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      refine Tendsto.comp (y := atTop) ?_ ?_refine_2.refine_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto g atTop (nhds 0)refine_2.refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto g' atTop atTops:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      ·refine_2.refine_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto g atTop (nhds 0)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C exact tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero (s + n) 2⁻¹ (bys:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ 0 < 2⁻¹s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C norm_numAll goals completed! 🐙s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C)
      ·refine_2.refine_2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ Tendsto g' atTop atTops:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C exact tendsto_atTop_atTop.mpr fun x ↦ ⟨x - 2, bys:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝ⊢ ∀ (a : ℝ), x - 2 ≤ a → x ≤ g' as:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C simp [g', add_comm]All goals completed! 🐙s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C⟩
    ·refine_3s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ ∀ᶠ (b_1 : ℝ) in atTop, 0 b_1 ≤ b b_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C exact eventually_atTop.mpr ⟨0, fun _ _ ↦ bys:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx✝¹:ℝx✝:0 ≤ x✝¹⊢ 0 x✝¹ ≤ b x✝¹s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C positivityAll goals completed! 🐙s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C⟩
    ·refine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + x⊢ ∀ᶠ (b_1 : ℝ) in atTop, b b_1 ≤ (rexp 1 • g ∘ g') b_1s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C refine eventually_atTop.mpr ⟨0, fun x hx ↦ ?_⟩refine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ b x ≤ (rexp 1 • g ∘ g') xs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      simp only [b, g, g', Function.comp_def, Pi.smul_def, mul_add, exp_add, smul_eq_mul]refine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ rexp 1 * ((2 + x) ^ (s + ↑n) * (rexp (-2⁻¹ * 2) * rexp (-2⁻¹ * x)))s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      field_simprefine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ x ^ s * (2 + x) ^ n ≤ rexp 1 * (2 + x) ^ (s + ↑n) * rexp (-1)s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      simp only [exp_neg, rpow_add (show 0 < 2 + x by linarith), rpow_natCast]refine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ x ^ s * (2 + x) ^ n ≤ rexp 1 * ((2 + x) ^ s * (2 + x) ^ n) * (rexp 1)⁻¹s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      field_simprefine_4s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ x ^ s ≤ (2 + x) ^ ss:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
      exact rpow_le_rpow hx (bys:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bg:ℝ → ℝ := fun x => x ^ (s + ↑n) * rexp (-2⁻¹ * x)g':ℝ → ℝ := fun x => 2 + xx:ℝhx:0 ≤ x⊢ x ≤ 2 + xs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C linarithAll goals completed! 🐙s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C) hss:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  have htail : ∀ᶠ x in atTop, b x < 1 :=
    (htop.eventually <| isOpen_Ioo.mem_nhds ⟨neg_one_lt_zero, zero_lt_one⟩).mono fun _ h ↦ h.2s:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  obtain ⟨M, hgM⟩ := eventually_atTop.mp htails:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  obtain ⟨x₀, hx₀, hx₀'⟩ :=
    isCompact_Icc.exists_isMaxOn ⟨0, Set.left_mem_Icc.mpr (abs_nonneg M)⟩ hb.continuousOns:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀⊢ ∃ C > 0, ∀ x ≥ 0, x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ C
  refine ⟨max (b x₀) 1, bys:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀⊢ max (b x₀) 1 > 0 simpAll goals completed! 🐙, fun x hx ↦ ?_⟩
  by_cases hxM : x ≤ |M|poss:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀x:ℝhx:x ≥ 0hxM:x ≤ |M|⊢ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ max (b x₀) 1negs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀x:ℝhx:x ≥ 0hxM:¬x ≤ |M|⊢ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ max (b x₀) 1
  ·poss:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀x:ℝhx:x ≥ 0hxM:x ≤ |M|⊢ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ max (b x₀) 1 exact le_max_of_le_left (hx₀' ⟨hx, hxM⟩)All goals completed! 🐙
  ·negs:ℝhs:0 ≤ sn:ℕb:ℝ → ℝ := fun x => x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x)hb:Continuous bhtop:Tendsto b atTop (nhds 0)htail:∀ᶠ (x : ℝ) in atTop, b x < 1M:ℝhgM:∀ (b_1 : ℝ), M ≤ b_1 → b b_1 < 1x₀:ℝhx₀:x₀ ∈ Set.Icc 0 |M|hx₀':IsMaxOn b (Set.Icc 0 |M|) x₀x:ℝhx:x ≥ 0hxM:¬x ≤ |M|⊢ x ^ s * (2 + x) ^ n * rexp (-2⁻¹ * x) ≤ max (b x₀) 1 exact le_max_of_le_right (hgM x <| (le_abs_self _).trans (Std.le_of_not_ge hxM)).leAll goals completed! 🐙

B. General, RCLike-valued

The (unnormalized) 𝕜-valued Gaussian exp (-2⁻¹ * ‖B⁻¹ (x - x₀)‖ ^ 2) as a Schwartz map.

def gaussian : 𝓢(E, 𝕜) :=
  compSubConstCLM 𝕜 x₀
    (((realStdGaussian D).postcompCLM ofRealCLM).compCLMOfContinuousLinearEquiv 𝕜 B.symm)

@[simp]
lemma gaussian_apply : gaussian 𝕜 B x₀ x = ofReal (rexp (-2⁻¹ * ‖B.symm (x - x₀)‖ ^ 2)) := rfl

The (unnormalized) 𝕜-valued Gaussian exp (-2⁻¹ * ‖B⁻¹ x‖ ^ 2) as a Schwartz map.

abbrev gaussian₀ : 𝓢(E, 𝕜) := gaussian 𝕜 B 0