Documentation

SpherePacking.MagicFunction.a.IntegralEstimates.I4

Constructing Upper-Bounds for I₄ #

The purpose of this file is to construct bounds on the integral I₄ that is part of the definition of the function a. We follow the proof of Proposition 7.8 in the blueprint.

TODO: #

Integrability of g and C₀ * rexp (-2 * π * s) * rexp (-π * r / s)

noncomputable def MagicFunction.a.IntegralEstimates.I₄.g :

ℝ → ℝ → ℂ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_eq_integral_g_Ioo (r : ℝ) :

RealIntegrals.I₄' r = ∫ (t : ℝ) in Set.Ioo 0 1, g r t

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_bounding_aux_1 (r t : ℝ) :

t ∈ Set.Ioo 0 1 → ‖g r t‖ ≤ ‖φ₀'' (-1 / (-↑t + Complex.I))‖ * 2 * Real.exp (-Real.pi * r)

theorem MagicFunction.a.IntegralEstimates.I₄.parametrisation_eq (t : ℝ) :

t ∈ Set.Ioo 0 1 → -1 / (-↑t + Complex.I) = ↑t / (↑t ^ 2 + 1) + 1 / (↑t ^ 2 + 1) * Complex.I

theorem MagicFunction.a.IntegralEstimates.I₄.im_parametrisation_eq (t : ℝ) :

t ∈ Set.Ioo 0 1 → (-1 / (-↑t + Complex.I)).im = 1 / (t ^ 2 + 1)

theorem MagicFunction.a.IntegralEstimates.I₄.im_parametrisation_lower (t : ℝ) :

t ∈ Set.Ioo 0 1 → 1 / 2 < (-1 / (-↑t + Complex.I)).im

theorem MagicFunction.a.IntegralEstimates.I₄.im_parametrisation_upper (t : ℝ) :

t ∈ Set.Ioo 0 1 → (-1 / (-↑t + Complex.I)).im < 1

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_bounding_aux_2 (r : ℝ) :

∃ C₀ > 0, ∀ t ∈ Set.Ioo 0 1, ‖g r t‖ ≤ C₀ * Real.exp (-2 * Real.pi * (-1 / (-↑t + Complex.I)).im) * 2 * Real.exp (-Real.pi * r)

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_bounding_aux_3 (r : ℝ) :

∃ C₀ > 0, ∀ t ∈ Set.Ioo 0 1, ‖g r t‖ ≤ C₀ * Real.exp (-Real.pi) * 2 * Real.exp (-Real.pi * r)

theorem MagicFunction.a.IntegralEstimates.I₄.Bound_integrableOn (r C₀ : ℝ) :

MeasureTheory.IntegrableOn (fun (x : ℝ) => C₀ * Real.exp (-Real.pi) * 2 * Real.exp (-Real.pi * r)) (Set.Ioo 0 1) MeasureTheory.volume

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_bounding_aux_4 (r : ℝ) :

∃ C₀ > 0, ∫ (t : ℝ) in Set.Ioo 0 1, ‖g r t‖ ≤ ∫ (x : ℝ) in Set.Ioo 0 1, C₀ * Real.exp (-Real.pi) * 2 * Real.exp (-Real.pi * r)

theorem MagicFunction.a.IntegralEstimates.I₄.I₄'_bounding (r : ℝ) :

∃ C₁ > 0, ‖RealIntegrals.I₄' r‖ ≤ C₁ * Real.exp (-Real.pi * r)

theorem MagicFunction.a.IntegralEstimates.I₄.decay'₀ (k : ℕ) :

∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖RealIntegrals.I₄' x‖ ≤ C

theorem MagicFunction.a.IntegralEstimates.I₄.decay' (k n : ℕ) :

∃ (C : ℝ), ∀ (x : ℝ), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n RealIntegrals.I₄' x‖ ≤ C