OAI/NumberTheory/CubicMoment/Estimates/RamifiedIdealParts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Exact separation of the finitely many primes above three in the complete ideal lattice. No ramified Euler term is discarded.

  1. def OAI.CubicFirstMoment.ramifiedPart line 13
  2. def OAI.CubicFirstMoment.unramifiedPart line 16
  3. lemma OAI.CubicFirstMoment.ramified_add_unramified line 19
  4. lemma OAI.CubicFirstMoment.unramifiedPart_primary line 22
  5. lemma OAI.CubicFirstMoment.ramifiedPart_le line 28
  6. lemma OAI.CubicFirstMoment.unramifiedPart_le line 33
  7. lemma OAI.CubicFirstMoment.ramifiedPart_norm_le line 38
  8. lemma OAI.CubicFirstMoment.idealExponent_exponent_bound line 44
  9. lemma OAI.CubicFirstMoment.ramifiedPart_support line 60
  10. theorem OAI.CubicFirstMoment.ramified_parts_card_le line 66

    Source documentation

    The number of ramified parts in a full norm ball grows only as a fixed power of the logarithm.

    theorem ramified_parts_card_le {J : ℝ} :
    ((fullIdealBall J).image ramifiedPart).card ≤
      (Nat.log 2 ⌊J⌋₊+1)^ramifiedIdealPrimes.card := by
…

    Mentions: OAI.CubicFirstMoment.fullIdealBall, OAI.CubicFirstMoment.ramifiedPart

  11. def OAI.CubicFirstMoment.ramifiedParts line 90
  12. def OAI.CubicFirstMoment.unramifiedFiber line 93
  13. lemma OAI.CubicFirstMoment.sum_unramifiedFiber line 97
  14. lemma OAI.CubicFirstMoment.ideal_sum_ramified_partition line 113
  15. lemma OAI.CubicFirstMoment.mellinPhase_mul_pos line 120
  16. theorem OAI.CubicFirstMoment.normalizedDualPolynomial_ramified_partition line 128

    Source documentation

    Exact separation of the ramified part in a normalized dual polynomial. Each ramified character value is a row scalar; the inner support is prime to three, with its precise rescaled normalization length.

    theorem normalizedDualPolynomial_ramified_partition
    (S : Finset EisensteinIdealExponent) (χ : EisensteinIdealExponent → ℂ)
    (hχ : ∀ ν κ, χ (ν+κ) = χ ν*χ κ) (J u : ℝ) :
    normalizedDualPolynomial S χ idealExponentNorm J u =
      ∑ ρ ∈ ramifiedParts S, (χ ρ*mellinPhase u (idealExponentNorm ρ))*
        normalizedDualPolynomial (unramifiedFiber S ρ) χ idealExponentNorm
          (J/idealExponentNorm ρ) u := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.normalizedDualPolynomial, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.ramifiedParts, OAI.CubicFirstMoment.mellinPhase, OAI.CubicFirstMoment.unramifiedFiber

  17. lemma OAI.CubicFirstMoment.unramifiedFiber_primary line 146
  18. lemma OAI.CubicFirstMoment.ramifiedParts_card_le line 152
  19. lemma OAI.CubicFirstMoment.unramifiedFiber_norm line 158
  20. lemma OAI.CubicFirstMoment.ramifiedPart_norm_le_upper line 171