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.

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