OAI/NumberTheory/CubicMoment/Transform/MetaplecticRetainedPowers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Explicit absorption of the retained norm-dyad count and arbitrarily small arithmetic losses in a fixed polynomial scale range.

  1. lemma OAI.CubicFirstMoment.metaplectic_dyad_count_log_bound line 12
  2. lemma OAI.CubicFirstMoment.metaplectic_dyad_count_small_power line 45
  3. theorem OAI.CubicFirstMoment.metaplectic_retained_loss_small_power line 59

    Source documentation

    The exponent used in the coefficient estimate can be chosen before all conductor and length parameters.

    theorem metaplectic_retained_loss_small_power {η B : ℝ} (hη : 0 < η) (hB : 0 ≤ B) :
    ∃ ε C : ℝ, 0 < ε ∧ 0 < C ∧ ∀ Y R J : ℝ, 1 ≤ Y → 0 < R → 1 ≤ J →
      R ≤ Y^B → J ≤ Y^B →
      ((Nat.log 2 ⌊3*J⌋₊+1:ℕ):ℝ)*(6*J)^(3*ε/2)*R^(2*ε) ≤ C*Y^η := by
…