MetaplecticCodeMean.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Ordinary mean values for the exact finite prefix partition. The coefficient hypotheses here are precisely the support data supplied by metaplectic_retained_support_partition.

lemma OAI.CubicFirstMoment.mean_norm_finset_sum_le line 15
def OAI.CubicFirstMoment.metaplecticPrefixAmplitude line 32
theorem OAI.CubicFirstMoment.metaplectic_code_block_mean line 38

theorem OAI.CubicFirstMoment.metaplectic_code_mean line 109

Source documentation

Reassembling the chosen support codes costs only the sum of the explicit free-block majorants. The original finite frequency polynomial is retained.

theorem metaplectic_code_mean {ε M : ℝ} (hε : 0 < ε)
    (hMV : MontgomeryVaughanBound M) (hM : 0 ≤ M) :
    ∃ D : ℝ, 0 < D ∧ ∀ (a : Eisenstein → MetaplecticDualArgument → ℂ)
      (C : ℝ), 0 ≤ C → ∀ r : Eisenstein, primary r →
      ∀ S : Finset (MetaplecticRetainedCode r),
      (∀ z ∈ S, IsCoprime z.2.2.val r) →
      (∀ z ∈ S, ‖a r (metaplecticRetainedDecode r z).1‖ ≤
        C*3^((max ((z.2.1.1:ℤ)-1) 0:ℤ)/3:ℝ)*Real.sqrt (norm z.2.1.2.2.2)) →
      ∀ I T : ℝ, 0 < T →
      (∀ z ∈ S, I/2 ≤ metaplecticDualNorm (metaplecticRetainedDecode r z) ∧
        metaplecticDualNorm (metaplecticRetainedDecode r z) ≤ I) →
      ∀ ℓ : ℤ, ∀ τ : ℝ,
…

Mentions: OAI.CubicFirstMoment.MontgomeryVaughanBound, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.MetaplecticDualArgument, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.MetaplecticRetainedCode, OAI.CubicFirstMoment.metaplecticRetainedDecode, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.metaplecticDualNorm