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

• MagicFunction.a.IntegralEstimates.I₆.g r t = Complex.I * φ₀'' (Complex.I * ↑t) * Complex.exp (-↑Real.pi * ↑r * ↑t)

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_eq_integral_g_Ioo (r : ℝ) : RealIntegrals.I₆' r = 2 * ∫ (t : ℝ) in Set.Ici 1, g r t

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_bounding_aux_1 (r t : ℝ) : t ∈ Set.Ici 1 → ‖g r t‖ = ‖φ₀'' (Complex.I * ↑t)‖ * Real.exp (-Real.pi * r * t)

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_bounding_aux_2 (r : ℝ) : ∃ C₀ > 0, ∀ t ∈ Set.Ici 1, ‖g r t‖ ≤ C₀ * Real.exp (-2 * Real.pi * t) * Real.exp (-Real.pi * r * t)

theorem MagicFunction.a.IntegralEstimates.I₆.Bound_integrableOn (r C₀ : ℝ) (hC₀_pos : C₀ > 0) (hC₀ : ∀ t ∈ Set.Ici 1, ‖g r t‖ ≤ C₀ * Real.exp (-2 * Real.pi * t) * Real.exp (-Real.pi * r * t)) : MeasureTheory.IntegrableOn (fun (t : ℝ) => C₀ * Real.exp (-2 * Real.pi * t) * Real.exp (-Real.pi * r * t)) (Set.Ici 1) MeasureTheory.volume

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_bounding_aux_3 (r : ℝ) : ∃ C₀ > 0, ∫ (t : ℝ) in Set.Ici 1, ‖g r t‖ ≤ ∫ (t : ℝ) in Set.Ici 1, C₀ * Real.exp (-2 * Real.pi * t) * Real.exp (-Real.pi * r * t)

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_bounding (r : ℝ) : ∃ C₁ > 0, ‖RealIntegrals.I₆' r‖ ≤ ∫ (t : ℝ) in Set.Ici 1, C₁ * Real.exp (-2 * Real.pi * t) * Real.exp (-Real.pi * r * t)

theorem MagicFunction.a.IntegralEstimates.I₆.I₆'_bounding_eq (r : ℝ) : ∃ C₂ > 0, ‖RealIntegrals.I₆' r‖ ≤ C₂ * Real.exp (-Real.pi * (r ^ 2 + 2)) / (r ^ 2 + 2)

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