Gaussian.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.AsymptoticallyMinimalLittlewood.integral_schwartz_mul_gaussian line 11

theorem OAI.AsymptoticallyMinimalLittlewood.norm_damped_quadratic_le_one line 39

Source documentation

The damping kernel has modulus at most one on the closed right half-plane.

theorem norm_damped_quadratic_le_one {b : ℂ} (hb : 0 ≤ b.re) (u x : ℝ) :
    ‖Complex.exp (-Real.pi * b * (x : ℂ) ^ 2 -
      2 * Real.pi * Complex.I * u * x)‖ ≤ 1 := by
…

theorem OAI.AsymptoticallyMinimalLittlewood.norm_damped_fourier_le_one line 51
Source documentation
The Fourier-side Gaussian also has modulus at most one.
```
theorem norm_damped_fourier_le_one {b : ℂ} (hb : 0 ≤ b.re) (y : ℝ) :
    ‖Complex.exp (-Real.pi / b * (y : ℂ) ^ 2)‖ ≤ 1 := by
…
```
theorem OAI.AsymptoticallyMinimalLittlewood.integral_schwartz_mul_gaussian_boundary line 63
def OAI.AsymptoticallyMinimalLittlewood.realPhase line 138
theorem OAI.AsymptoticallyMinimalLittlewood.norm_realPhase line 140
theorem OAI.AsymptoticallyMinimalLittlewood.integrable_schwartz_phase line 144
Source documentation
Multiplication by a continuous real phase preserves integrability.
```
theorem integrable_schwartz_phase (f : 𝓢(ℝ, ℂ)) (p : ℝ → ℝ)
    (hp : Continuous p) : Integrable (fun x ↦ f x * realPhase (p x)) := by
…
```
Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase

theorem OAI.AsymptoticallyMinimalLittlewood.integral_schwartz_quadratic_exact line 155

Source documentation

Quadratic Fourier identity with an undamped, nonzero real curvature.

theorem integral_schwartz_quadratic_exact (f : 𝓢(ℝ, ℂ))
    {t : ℝ} (ht : t ≠ 0) (u : ℝ) :
    (∫ x : ℝ, f x * realPhase (Real.pi * t * x ^ 2 - 2 * Real.pi * u * x)) =
    1 / (-Complex.I * (t : ℂ)) ^ (1 / 2 : ℂ) *
      ∫ ξ : ℝ, (𝓕⁻ f : 𝓢(ℝ, ℂ)) ξ * realPhase (-Real.pi / t * (ξ + u) ^ 2) := by
…

Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase

theorem OAI.AsymptoticallyMinimalLittlewood.integral_schwartz_inverse_linear line 183
Source documentation
Fourier inversion specialized to the linear factor in the quadratic formula.
```
theorem integral_schwartz_inverse_linear (f : 𝓢(ℝ, ℂ)) (x : ℝ) :
    (∫ ξ : ℝ, (𝓕⁻ f : 𝓢(ℝ, ℂ)) ξ * realPhase (-2 * Real.pi * ξ * x)) = f x := by
…
```
Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase
theorem OAI.AsymptoticallyMinimalLittlewood.norm_quadratic_multiplier_sub_one line 196
Source documentation
The remaining quadratic Fourier multiplier differs from one by at most π ξ² / |t|, uniformly in the stationary point.
```
theorem norm_quadratic_multiplier_sub_one {t : ℝ} (ξ : ℝ) :
    ‖realPhase (-Real.pi / t * ξ ^ 2) - 1‖ ≤ Real.pi / |t| * ξ ^ 2 := by
…
```
Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase
theorem OAI.AsymptoticallyMinimalLittlewood.realPhase_add line 204
theorem OAI.AsymptoticallyMinimalLittlewood.uniform_quadratic_error line 208
theorem OAI.AsymptoticallyMinimalLittlewood.norm_quadratic_prefactor line 273
Source documentation
The prefactor in uniform quadratic integration has precisely the required modulus. No pointwise lower estimate for a Littlewood polynomial is involved.
```
theorem norm_quadratic_prefactor (t u : ℝ) :
    ‖1 / (-Complex.I * (t : ℂ)) ^ (1 / 2 : ℂ) *
        realPhase (-Real.pi / t * u ^ 2)‖ = 1 / Real.sqrt |t| := by
…
```
Mentions: OAI.AsymptoticallyMinimalLittlewood.realPhase
theorem OAI.AsymptoticallyMinimalLittlewood.arg_negative_imaginary line 285
Source documentation
The argument of the nonzero imaginary curvature, on the principal branch.
```
theorem arg_negative_imaginary {t : ℝ} (ht : t ≠ 0) :
    Complex.arg (-Complex.I * (t : ℂ)) = -Real.sign t * Real.pi / 2 := by
…
```
theorem OAI.AsymptoticallyMinimalLittlewood.quadratic_prefactor_eq line 297
theorem OAI.AsymptoticallyMinimalLittlewood.uniform_quadratic_integration line 320