HuxleyFractionSeparation.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Separation of the actual reduced Eisenstein fractions in the additive sieve.

lemma OAI.CubicFirstMoment.eisenstein_fraction_cross_norm line 11
lemma OAI.CubicFirstMoment.eisenstein_fraction_separation line 24
lemma OAI.CubicFirstMoment.reduced_fraction_associated_denominators line 41
lemma OAI.CubicFirstMoment.reduced_fraction_nonassociated_separation line 54
lemma OAI.CubicFirstMoment.residue_fraction_separation line 63
Source documentation
Distinct residue classes at the same denominator stay separated modulo the lattice.
```
lemma residue_fraction_separation {q : Eisenstein} (hq : q ≠ 0)
    {x y : Residues q} (hxy : x ≠ y) {Q : ℝ} (hqQ : norm q ≤ Q) (z : Eisenstein) :
    1/Q^2 ≤ ‖(residueRepresentative q x:ℂ)/(q:ℂ)-
      (residueRepresentative q y:ℂ)/(q:ℂ)-(z:ℂ)‖^2 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.residueRepresentative

lemma OAI.CubicFirstMoment.huxley_reduced_fraction_separation line 83

Source documentation

The unit conditions in Huxley's literal residue sum are exactly the coprimality conditions used in the cross-determinant separation proof.

lemma huxley_reduced_fraction_separation {q r : Eisenstein}
    (hq : q ≠ 0) (hr : r ≠ 0) (x : Residues q) (y : Residues r)
    (hx : IsUnit x) (hy : IsUnit y) (hnot : ¬Associated q r)
    {Q : ℝ} (hqQ : norm q ≤ Q) (hrQ : norm r ≤ Q) (z : Eisenstein) :
    1/Q^2 ≤ ‖(residueRepresentative q x:ℂ)/(q:ℂ)-
      (residueRepresentative r y:ℂ)/(r:ℂ)-(z:ℂ)‖^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.Residues, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.residueRepresentative

lemma OAI.CubicFirstMoment.eisenstein_fraction_eq_of_close line 93
lemma OAI.CubicFirstMoment.translated_fraction_eq_of_close line 108
lemma OAI.CubicFirstMoment.associated_denominator_count line 121
Source documentation
All associates have a uniformly bounded multiplicity; an explicit lattice bound suffices, so the large sieve does not require classifying the six units.
```
lemma associated_denominator_count (S : Finset Eisenstein) (q : Eisenstein) :
    ((S.filter (fun r => Associated q r)).card:ℝ) ≤ 18 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein