GeometricPrimeIntervals.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact norm intervals for the concrete bins used by the stopping construction, including their bounded endpoint convention change.

theorem OAI.CubicFirstMoment.geometricPrimeBin_eq_iff line 13
lemma OAI.CubicFirstMoment.geometricPrimeBin_away_endpoints line 41

theorem OAI.CubicFirstMoment.geometricPrimeBin_endpoint_difference line 57

Source documentation

Replacing a half-open bin by the open-closed interval used by prime partial summation changes only the two endpoint norms.

theorem geometricPrimeBin_endpoint_difference {ρ B : ℝ} (hρ : 1 < ρ) (hρ₂ : ρ ≤ 2)
    {j : ℕ} (hj : j < geometricBinCount ρ B) (S : Finset Eisenstein)
    (hS : ∀ p ∈ S, primaryPrime p ∧ norm p ≤ B)
    (f : Eisenstein → ℂ) {M : ℝ} (hM : 0 ≤ M) (hf : ∀ p ∈ S, ‖f p‖ ≤ M) :
    ‖(∑ p ∈ S with geometricPrimeBin ρ B p = j, f p)-
      (∑ p ∈ S with geometricBinLower ρ B j < norm p ∧
        norm p ≤ ρ*geometricBinLower ρ B j, f p)‖ ≤ 4*M := by
…

Mentions: OAI.CubicFirstMoment.geometricBinCount, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.geometricPrimeBin, OAI.CubicFirstMoment.geometricBinLower