OAI/NumberTheory/CubicMoment/Estimates/HuxleyLiftedPacking.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Local multiplicity of the reduced fractions and all their lattice translates.

  1. structure OAI.CubicFirstMoment.HuxleyLift line 10
  2. def OAI.CubicFirstMoment.HuxleyLift.frequency line 16
  3. def OAI.CubicFirstMoment.HuxleyLift.reduced line 19
  4. lemma OAI.CubicFirstMoment.huxleyLift_actual line 25
  5. lemma OAI.CubicFirstMoment.huxleyLift_eq_of_frequency_of_denominator line 33
  6. lemma OAI.CubicFirstMoment.huxleyLift_eq_frequency_of_close line 61
  7. lemma OAI.CubicFirstMoment.huxleyLift_associated_of_close line 68
  8. lemma OAI.CubicFirstMoment.huxleyLift_local_count line 85

    Source documentation

    A small disk contains at most eighteen lifted reduced fractions, counting all associate denominators and all lattice translations.

    lemma huxleyLift_local_count (Q : ℝ) (hQ : 0 < Q) (z : ℂ) (S : Finset HuxleyLift)
    (hred : ∀ i ∈ S, i.reduced Q)
    (hclose : ∀ i ∈ S, ‖i.frequency-z‖ < 1/(3*Q)) :
    (S.card:ℝ) ≤ 18 := by
…

    Mentions: OAI.CubicFirstMoment.HuxleyLift