Documentation

SpherePacking.MagicFunction.a.IntegralEstimates.I3

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: #

We begin by performing changes of variables. We use Ioc intervals everywhere because of the way intervalIntegral is defined.

source
def MagicFunction.a.IntegralEstimates.I₃.f :
ℝ → ℝ
Equations
Instances For
    source
    def MagicFunction.a.IntegralEstimates.I₃.f' :
    ℝ → ℝ
    Equations
    Instances For
      source
      def MagicFunction.a.IntegralEstimates.I₃.g :
      ℝ → ℝ → ℂ
      Equations
      Instances For
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.aux_measurable :
        MeasurableSet (Set.Ioc 0 1)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.aux_hasDeriv (x : ℝ) (hx : x ∈ Set.Ioc 0 1) :
        HasDerivWithinAt f (f' x) (Set.Ioc 0 1) x
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.aux_injOn :
        Set.InjOn f (Set.Ioc 0 1)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Changing_Domain_of_Integration (r : ℝ) :
        ∫ (s : ℝ) in Set.Ici 1, g r s = ∫ (s : ℝ) in f '' Set.Ioc 0 1, g r s
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Changing_Variables (r : ℝ) :
        ∫ (s : ℝ) in f '' Set.Ioc 0 1, g r s = ∫ (t : ℝ) in Set.Ioc 0 1, |f' t| • g r (f t)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Writing_as_intervalIntegral (r : ℝ) :
        ∫ (t : ℝ) in Set.Ioc 0 1, |f' t| • g r (f t) = ∫ (t : ℝ) in 0 ..1, |f' t| • g r (f t)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Reconciling_Change_of_Variables (r : ℝ) :
        RealIntegrals.I₃' r = ∫ (t : ℝ) in Set.Ioc 0 1, |f' t| • g r (f t)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Complete_Change_of_Variables (r : ℝ) :
        RealIntegrals.I₃' r = ∫ (s : ℝ) in Set.Ici 1, g r s
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.I₃'_bounding_aux_1 (r x : ℝ) :
        x ∈ Set.Ici 1 → ‖g r x‖ ≤ ‖φ₀'' (Complex.I * ↑x)‖ * Real.exp (-Real.pi * r / x)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.I₃'_bounding_aux_2 (r : ℝ) :
        ∃ C₀ > 0, ∀ x ∈ Set.Ici 1, ‖g r x‖ ≤ C₀ * Real.exp (-2 * Real.pi * x) * Real.exp (-Real.pi * r / x)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.Bound_integrableOn (r C₀ : ℝ) (hC₀_pos : C₀ > 0) (hC₀ : ∀ x ∈ Set.Ici 1, ‖g r x‖ ≤ C₀ * Real.exp (-2 * Real.pi * x) * Real.exp (-Real.pi * r / x)) :
        MeasureTheory.IntegrableOn (fun (s : ℝ) => C₀ * Real.exp (-2 * Real.pi * s) * Real.exp (-Real.pi * r / s)) (Set.Ici 1) MeasureTheory.volume
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.I₃'_bounding_1_aux_3 (r : ℝ) :
        ∃ C₀ > 0, ∫ (s : ℝ) in Set.Ici 1, ‖g r s‖ ≤ ∫ (s : ℝ) in Set.Ici 1, C₀ * Real.exp (-2 * Real.pi * s) * Real.exp (-Real.pi * r / s)
        source
        theorem MagicFunction.a.IntegralEstimates.I₃.I₃'_bounding (r : ℝ) :
        ∃ C₀ > 0, ‖RealIntegrals.I₃' r‖ ≤ ∫ (s : ℝ) in Set.Ici 1, C₀ * Real.exp (-2 * Real.pi * s) * Real.exp (-Real.pi * r / s)