PrimeBinGeometry.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform norm distortion for the multiplicative bin surrogate. The bin ratio is fixed before the norm parameter; all selected subsets simultaneously satisfy the manuscript's small-power distortion bound.

lemma OAI.CubicFirstMoment.primaryPrime_norm_ge_two line 16
lemma OAI.CubicFirstMoment.primary_prime_subset_norm_le line 28
lemma OAI.CubicFirstMoment.primary_prime_subset_two_pow_le line 34
lemma OAI.CubicFirstMoment.primeSurrogate_norm_bounds line 44

theorem OAI.CubicFirstMoment.uniform_prime_bin_distortion line 60

Source documentation

A fixed ratio larger than one can be chosen so that all selected subproducts in every squarefree envelope have distortion at most X^(kappa/4). No bin occupancy vector is enumerated.

theorem uniform_prime_bin_distortion {κ C : ℝ} (hκ : 0 < κ) (hC : 0 < C) :
    ∃ ρ : ℝ, 1 < ρ ∧ ∀ᶠ X : ℝ in atTop,
      ∀ n : Eisenstein, primary n → Squarefree n → norm n ≤ C*X →
      ∀ s : Finset Eisenstein, s ⊆ primaryPrimeFactors n →
      ∀ (b : Eisenstein → ℕ) (ell : ℕ → ℝ),
        (∀ p ∈ s, 0 ≤ ell (b p) ∧ ell (b p) ≤ norm p ∧ norm p ≤ ρ*ell (b p)) →
      primeSurrogate s b ell ≤ norm (∏ p ∈ s, p) ∧
        norm (∏ p ∈ s, p) ≤ X^(κ/4)*primeSurrogate s b ell := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.primeSurrogate