CubeExclusions.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The cost of excluding prime divisors from the principal cube lattice.

theorem OAI.CubicFirstMoment.radial_cube_lattice_norm_sum_bound line 14

Source documentation

The absolute sum has the same area bound as its arbitrary bounded twists.

theorem radial_cube_lattice_norm_sum_bound (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ K : ℝ, 0 < K ∧ ∀ q : ℝ, 0 < q →
      (∑' j : Eisenstein, if j = 0 then 0 else
        ‖radialDualProfile W (q^3*(norm j)^3)‖) ≤ K/q := by
…

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

lemma OAI.CubicFirstMoment.tsum_divisible line 44

theorem OAI.CubicFirstMoment.radial_cube_multiples_bound line 57

Source documentation

This remains valid when the sublattice spacing exceeds the natural radius; there is no spurious constant term for the deleted origin.

theorem radial_cube_multiples_bound (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ K : ℝ, 0 < K ∧ ∀ q : ℝ, 0 < q → ∀ m : Eisenstein, m ≠ 0 →
      (∑' j : Eisenstein, if m ∣ j ∧ j ≠ 0 then
        ‖radialDualProfile W (q^3*(norm j)^3)‖ else 0) ≤ K/(q*norm m) := by
…

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

lemma OAI.CubicFirstMoment.not_coprime_prime_cover line 86