MetaplecticCubeEnergy.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Energy of the actual cube-completed primal polynomial. Cube-divisor fibers cost an arbitrary small power; the remaining weighted pair count is linear in the norm cutoff, because the d-variable has exponent -2.

def OAI.CubicFirstMoment.metaplecticCubeProduct line 15
lemma OAI.CubicFirstMoment.metaplecticCubeProduct_norm line 17
def OAI.CubicFirstMoment.metaplecticCubeCoefficient line 23
lemma OAI.CubicFirstMoment.metaplectic_cube_fiber_card line 27
lemma OAI.CubicFirstMoment.metaplectic_cube_pair_weight line 46

theorem OAI.CubicFirstMoment.metaplectic_cube_energy line 89

Source documentation

The coefficient energy after collecting actual cube products.

theorem metaplectic_cube_energy {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset (Eisenstein × Eisenstein)),
      (∀ du ∈ S, primary du.1 ∧ primary du.2) →
      ∀ (w : Eisenstein × Eisenstein → ℂ) (V M : ℝ), 1 ≤ V → 0 ≤ M →
      (∀ du ∈ S, norm (metaplecticCubeProduct du) ≤ V) →
      (∀ du ∈ S, ‖w du‖^2 ≤ norm du.1*M^2) →
      (∑ b ∈ S.image metaplecticCubeProduct, ‖metaplecticCubeCoefficient S w b‖^2) ≤
        C*V^(1+ε)*M^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCubeProduct, OAI.CubicFirstMoment.metaplecticCubeCoefficient

def OAI.CubicFirstMoment.metaplecticPrimalCoefficient line 139
Source documentation
The literal primal summand before its norm-phase, as in the published completed sum.
```
def metaplecticPrimalCoefficient (r : Eisenstein) (ℓ : ℤ) (W : ℝ → ℂ)
    (X : ℝ) (du : Eisenstein × Eisenstein) : ℂ :=
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.metaplecticPrimalCoefficient_sq_le line 146

theorem OAI.CubicFirstMoment.metaplectic_primal_energy line 175

Source documentation

No coefficient-energy hypothesis remains for the actual completed Gauss summand: its modulus bound is supplied by the Gauss and angular identities.

theorem metaplectic_primal_energy {ε : ℝ} (hε : 0 < ε) :
    ∃ C : ℝ, 0 < C ∧ ∀ (S : Finset (Eisenstein × Eisenstein)),
      (∀ du ∈ S, primary du.1 ∧ primary du.2) →
      ∀ (r : Eisenstein), primary r → ∀ (ℓ : ℤ) (W : ℝ → ℂ) (X V M : ℝ),
      1 ≤ V → 0 ≤ M → (∀ du ∈ S, norm (metaplecticCubeProduct du) ≤ V) →
      (∀ du ∈ S, ‖W (norm (metaplecticCubeProduct du)/X)‖ ≤ M) →
      (∑ b ∈ S.image metaplecticCubeProduct,
        ‖metaplecticCubeCoefficient S (metaplecticPrimalCoefficient r ℓ W X) b‖^2) ≤
          C*V^(1+ε)*M^2 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticCubeProduct, OAI.CubicFirstMoment.metaplecticCubeCoefficient, OAI.CubicFirstMoment.metaplecticPrimalCoefficient