DispersionCommonFactors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Common factors in the dispersion Poisson identity

The shared Gauss factors cancel before the remaining coprimality condition is removed by the finite ideal Möbius expansion. The formulas hold even if a shared factor also divides a residual factor: the character then vanishes. There is no tacit coprimality assumption on the original pair.

theorem OAI.CubicFirstMoment.common_gauss_pair_cancellation line 20

Source documentation

The exact surviving character after the Gauss factors cancel.

theorem common_gauss_pair_cancellation {k a b : Eisenstein}
    (hk : primary k) (ha : primary a) (hb : primary b)
    (hsk : Squarefree k) (hsa : Squarefree a) (hsb : Squarefree b) :
    gauss (k*a) * star (gauss (k*b)) * (gauss b * star (gauss a)) =
      mixedCubic b a k := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.gauss, OAI.CubicFirstMoment.mixedCubic

theorem OAI.CubicFirstMoment.common_amplitude_pair_cancellation line 38

theorem OAI.CubicFirstMoment.dispersion_common_pair_poisson line 55

Source documentation

The existing exact Möbius/Poisson formula applied to a pair with a shared factor, with all normalized Gauss factors cancelled.

theorem dispersion_common_pair_poisson {k a b : Eisenstein}
    (hk : primary k) (ha : primary a) (hb : primary b)
    (hsk : Squarefree k) (hsa : Squarefree a) (hsb : Squarefree b)
    (hab : IsCoprime a b) (β : Eisenstein → ℂ) (u : ℝ)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hW' : ContDiff ℝ ∞ W)
    {A : ℝ} (hA : 0 < A) :
    dispersionAmplitude β u (k*a) * star (dispersionAmplitude β u (k*b)) *
      primaryCharacterGram (k*b) (k*a) W A =
      ∑ s ∈ (primaryPrimeFactors k).powerset,
        let m := ∏ p ∈ s, p
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.dispersionAmplitude, OAI.CubicFirstMoment.primaryCharacterGram, OAI.CubicFirstMoment.primaryPrimeFactors