OAI/NumberTheory/CubicMoment/Estimates/HuxleyGridPacking.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Square-grid packing of the actual lifted reduced fractions.

  1. lemma OAI.CubicFirstMoment.same_floor_abs_sub_lt_one line 11
  2. def OAI.CubicFirstMoment.huxleyGrid line 19
  3. lemma OAI.CubicFirstMoment.huxleyGrid_close line 22
  4. lemma OAI.CubicFirstMoment.huxleyGrid_fiber_count line 38
  5. lemma OAI.CubicFirstMoment.huxleyLift_count_of_grid_mem line 54
  6. lemma OAI.CubicFirstMoment.floor_scaled_in_box line 68
  7. lemma OAI.CubicFirstMoment.huxleyLift_disk_count line 86

    Source documentation

    Uniform disk count for all reduced residue fractions and their translates.

    lemma huxleyLift_disk_count (Q : ℝ) (hQ : 0 < Q) (z : ℂ) (R : ℝ) (hR : 0 ≤ R)
    (S : Finset HuxleyLift) (hred : ∀ i ∈ S, i.reduced Q)
    (hball : ∀ i ∈ S, ‖i.frequency-z‖ ≤ R) :
    (S.card:ℝ) ≤ 6000*(1+Q^2*R^2) := by
…

    Mentions: OAI.CubicFirstMoment.HuxleyLift