LargeSquareSupport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Sparse support from a large square divisor, used to remove repeated large primes in the exceptional character moments.

def OAI.CubicFirstMoment.largeSquareSupport line 14
lemma OAI.CubicFirstMoment.square_multiples_normBall line 17
theorem OAI.CubicFirstMoment.largeSquareSupport_card_bound line 34
Source documentation
Cardinality is at most C Y / sqrt D, uniformly for positive D. The proof uses only planar lattice counting and a convergent norm series.
```
theorem largeSquareSupport_card_bound :
    ∃ C : ℝ, 0 < C ∧ ∀ Y D : ℝ, 0 ≤ Y → 0 < D →
      ((largeSquareSupport Y D).card:ℝ) ≤ C*Y*D^(-(1/2:ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.largeSquareSupport