PrincipalContribution.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The absolute principal contribution to short dispersion

The actual cube-frequency kernel includes the Poisson scalar and the three-to-one multiplicity. Its bound has size A^(2/3) N(ab)^(-1/6).

lemma OAI.CubicFirstMoment.principal_cube_prefactor_scale line 18
def OAI.CubicFirstMoment.principalCubeKernel line 39
Source documentation
The principal kernel after its exact three-to-one cube reindexing.
```
def principalCubeKernel (a b : Eisenstein) (W : ℝ → ℂ) (A : ℝ) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
theorem OAI.CubicFirstMoment.principalCubeKernel_bound line 47
Source documentation
Uniform over the arithmetic coprimality restrictions in the cube kernel; no roughness or coefficient cancellation is used here.
```
theorem principalCubeKernel_bound (W : ℝ → ℂ) (hW : HasCompactSupport W)
    (hW' : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ A : ℝ, 0 < A → ∀ a b : Eisenstein,
      a ≠ 0 → b ≠ 0 →
      ‖principalCubeKernel a b W A‖ ≤ C*A^(2/3:ℝ)*(norm (b*a))^(-(1/6:ℝ)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.principalCubeKernel, OAI.CubicFirstMoment.norm
def OAI.CubicFirstMoment.principalBilinearContribution line 86

theorem OAI.CubicFirstMoment.principalBilinearContribution_bound line 93

Source documentation

The actual principal bilinear contribution satisfies the l¹ term of the short-dispersion estimate, uniformly in the height.

theorem principalBilinearContribution_bound (W : ℝ → ℂ)
    (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W) :
    ∃ C : ℝ, 0 < C ∧ ∀ A B₀ : ℝ, 0 < A → 0 < B₀ →
      ∀ B : Finset Eisenstein, (∀ b ∈ B, B₀ ≤ norm b) →
      ∀ β : Eisenstein → ℂ, ∀ u : ℝ,
      ‖principalBilinearContribution B β u W A‖ ≤
        C*A^(2/3:ℝ)*B₀^(-(1/3:ℝ))*(∑ b ∈ B, ‖β b‖)^2 := by
…

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