OAI/NumberTheory/CubicMoment/Transform/MetaplecticCompletion.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Exact inversion of the cubic completion kernel. The Euler variable for a prime ideal is first weighted, then replaced by its cube. Thus the series identities below retain the actual cube-divisor support; they are not ordinary (uncubed) convolution identities.

  1. abbrev OAI.CubicFirstMoment.ComplexIdealSeries line 17
  2. def OAI.CubicFirstMoment.cubeCompletionSeries line 19
  3. def OAI.CubicFirstMoment.cubeInverseCompletionSeries line 23
  4. lemma OAI.CubicFirstMoment.cube_completion_inverse line 27
  5. lemma OAI.CubicFirstMoment.cube_completion_inversion line 32
  6. lemma OAI.CubicFirstMoment.cubeCompletionSeries_coeff line 37
  7. lemma OAI.CubicFirstMoment.cubeInverseCompletionSeries_coeff line 45
  8. lemma OAI.CubicFirstMoment.cubeCompletionSeries_coeff_zero line 53
  9. lemma OAI.CubicFirstMoment.cubeInverseCompletionSeries_coeff_zero line 58
  10. theorem OAI.CubicFirstMoment.cube_completion_finite_inverse line 64

    Source documentation

    The inverse identity is a literal finite sum at every ideal.

    theorem cube_completion_finite_inverse (x : EisensteinIdealPrime → ℂ)
    (A : ComplexIdealSeries) (ν : EisensteinIdealExponent) :
    (∑ d ∈ Finset.HasAntidiagonal.antidiagonal ν,
      MvPowerSeries.coeff d.1 (cubeInverseCompletionSeries x)*
        ∑ e ∈ Finset.HasAntidiagonal.antidiagonal d.2,
          MvPowerSeries.coeff e.1 (cubeCompletionSeries x)*MvPowerSeries.coeff e.2 A) =
      MvPowerSeries.coeff ν A := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.ComplexIdealSeries, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.cubeInverseCompletionSeries, OAI.CubicFirstMoment.cubeCompletionSeries

  11. theorem OAI.CubicFirstMoment.cube_completion_weighted_inverse line 75

    Source documentation

    Arbitrary finite norm weights may be applied after cube inversion.

    theorem cube_completion_weighted_inverse (x : EisensteinIdealPrime → ℂ)
    (A : ComplexIdealSeries) (S : Finset EisensteinIdealExponent) (W : ℝ → ℂ) :
    (∑ ν ∈ S, W (idealExponentNorm ν)*
      ∑ d ∈ Finset.HasAntidiagonal.antidiagonal ν,
        MvPowerSeries.coeff d.1 (cubeInverseCompletionSeries x)*
          ∑ e ∈ Finset.HasAntidiagonal.antidiagonal d.2,
            MvPowerSeries.coeff e.1 (cubeCompletionSeries x)*MvPowerSeries.coeff e.2 A) =
      ∑ ν ∈ S, W (idealExponentNorm ν)*MvPowerSeries.coeff ν A := by
…

    Mentions: OAI.CubicFirstMoment.EisensteinIdealPrime, OAI.CubicFirstMoment.ComplexIdealSeries, OAI.CubicFirstMoment.EisensteinIdealExponent, OAI.CubicFirstMoment.idealExponentNorm, OAI.CubicFirstMoment.cubeInverseCompletionSeries, OAI.CubicFirstMoment.cubeCompletionSeries

  12. lemma OAI.CubicFirstMoment.primary_nat_pow line 87
  13. lemma OAI.CubicFirstMoment.idealPrimaryGenerator_eq_normalized_prime_product line 93
  14. lemma OAI.CubicFirstMoment.normalized_prime_product_character line 112
  15. def OAI.CubicFirstMoment.metaplecticCompletionWeight line 150

    Source documentation

    The precise inverse-completion weight, including the norm phase created by replacing the length by U / (Nc)^3.

    def metaplecticCompletionWeight (r : Eisenstein) (ℓ : ℤ) (t : ℝ)
    (c : Eisenstein) : ℂ :=
…

    Mentions: OAI.CubicFirstMoment.Eisenstein

  16. lemma OAI.CubicFirstMoment.metaplecticCompletionWeight_one line 156
  17. lemma OAI.CubicFirstMoment.metaplecticCompletionWeight_mul line 160
  18. theorem OAI.CubicFirstMoment.cubeInverseCompletionSeries_at_primary line 178

    Source documentation

    At a primary principal ideal the expanded inverse kernel has exactly the arithmetic weight mu(c)|c| theta_(3ell)(c)(Nc)^(3it). There is no assumption that c is squarefree.

    theorem cubeInverseCompletionSeries_at_primary (r : Eisenstein) (ℓ : ℤ) (t : ℝ)
    {c : Eisenstein} (hc : primary c) :
    MvPowerSeries.coeff (3 • idealExponentOf c)
      (cubeInverseCompletionSeries (fun p => metaplecticCompletionWeight r ℓ t
        (primaryNormalize (idealPrimeRepresentative p)))) =
      (idealMoebius c:ℂ)*metaplecticCompletionWeight r ℓ t c := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.idealExponentOf, OAI.CubicFirstMoment.cubeInverseCompletionSeries, OAI.CubicFirstMoment.metaplecticCompletionWeight, OAI.CubicFirstMoment.primaryNormalize, OAI.CubicFirstMoment.idealPrimeRepresentative, OAI.CubicFirstMoment.idealMoebius

  19. theorem OAI.CubicFirstMoment.cubeCompletionSeries_at_primary line 191
  20. lemma OAI.CubicFirstMoment.norm_metaplecticCompletionWeight line 202
  21. theorem OAI.CubicFirstMoment.norm_cubeInverseCompletionSeries_at_primary line 214