CubeRoughness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A finite prime-cover bound for restoring coprimality in the cube term.

lemma OAI.CubicFirstMoment.norm_tsum_restriction_le_cover line 12

theorem OAI.CubicFirstMoment.radial_cube_coprimality_error line 42

Source documentation

Restoring coprimality costs exactly the expected sum of reciprocal prime norms. The estimate is uniform over the lattice scale.

theorem radial_cube_coprimality_error (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ K : ℝ, 0 < K ∧ ∀ q : ℝ, 0 < q → ∀ a b : Eisenstein,
      primary a → Squarefree a → primary b → Squarefree b →
      ‖(∑' j : Eisenstein, if j = 0 then 0 else
          radialDualProfile W (q^3*(norm j)^3)) -
        (∑' j : Eisenstein, if j = 0 then 0 else
          (if IsCoprime a j ∧ IsCoprime b j then
            radialDualProfile W (q^3*(norm j)^3) else 0))‖ ≤
        K/q * ∑ p ∈ primaryPrimeFactors a ∪ primaryPrimeFactors b, 1/norm p := by
…

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