OAI/NumberTheory/CubicMoment/Estimates/HuxleyGaussianPacking.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CubicFirstMoment.huxley_gaussian_weight_summable line 11
2. def OAI.CubicFirstMoment.huxleyGaussianConstant line 18
3. lemma OAI.CubicFirstMoment.huxleyGaussianConstant_pos line 21
4. lemma OAI.CubicFirstMoment.huxleyLift_gaussian_bin_bound line 28
5. lemma OAI.CubicFirstMoment.huxleyLift_gaussian_sum_bound line 63

   Source documentation

   The Gaussian row bound has exactly the required two-dimensional scale.

   lemma huxleyLift_gaussian_sum_bound (Q : ℝ) (hQ : 0 < Q) (z : ℂ)
       {t : ℝ} (ht : 0 < t) (S : Finset HuxleyLift)
       (hred : ∀ i ∈ S, i.reduced Q) :
       (∑ i ∈ S, Real.exp (-t*‖i.frequency-z‖^2)) ≤
         huxleyGaussianConstant*(1+Q^2/t) := by
   …

   Mentions: OAI.CubicFirstMoment.HuxleyLift, OAI.CubicFirstMoment.huxleyGaussianConstant

6. def OAI.CubicFirstMoment.huxleyLiftGaussian line 94
7. lemma OAI.CubicFirstMoment.huxleyLiftGaussian_finite_bound line 97
8. lemma OAI.CubicFirstMoment.huxleyLiftGaussian_summable line 104
9. lemma OAI.CubicFirstMoment.huxleyLiftGaussian_tsum_bound line 112