CubeLatticeBounds.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The correctly scaled absolute cube-lattice bound

The dyadic norm count and rapid decay give the norm-area scale q⁻¹ for a profile evaluated at q³ N(j)³. This is the cube contribution needed even when no lattice asymptotic is available.

lemma OAI.CubicFirstMoment.cube_decay_comparison line 19
lemma OAI.CubicFirstMoment.radial_cube_pointwise_bound line 29

theorem OAI.CubicFirstMoment.radial_cube_lattice_weighted_bound line 45

Source documentation

Uniform absolute bound at the cube-lattice scale.

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

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

theorem OAI.CubicFirstMoment.radial_cube_lattice_absolute_bound line 98
Source documentation
The unweighted cube lattice is a special case of the bound with arbitrary fixed exclusions and unit-modulus twists.
```
theorem radial_cube_lattice_absolute_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