StoppedCoefficients.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Literal independent coefficients from the stopping construction. The selected-side test may contain the first-stage failure and crossing conditions; the remaining-side test is a separate condition on its divisor. No coprimality condition is inserted between the two sides.

def OAI.CubicFirstMoment.primaryPairSupport line 15
def OAI.CubicFirstMoment.primaryPairFiber line 18
def OAI.CubicFirstMoment.primaryPairCoefficient line 22
lemma OAI.CubicFirstMoment.primaryPairCoefficient_sum line 26
def OAI.CubicFirstMoment.stoppedBeta line 43
def OAI.CubicFirstMoment.stoppedAlpha line 49

theorem OAI.CubicFirstMoment.stopped_coefficients_sum line 56

Source documentation

Exact collection of the stopped divisors. The selected test depends only on r,d and the remaining test only on e.

theorem stopped_coefficients_sum (R D E U : Finset Eisenstein)
    (v : Eisenstein → ℂ) (ψ : ℝ → ℝ) (w : ℝ)
    (selected : Eisenstein → Eisenstein → Prop) (remaining : Eisenstein → Prop)
    (K : Eisenstein → ℂ) :
    (∑ a ∈ primaryPairSupport E U, ∑ b ∈ primaryPairSupport R D,
      stoppedAlpha E U ψ w remaining a*stoppedBeta R D v ψ w selected b*K (a*b)) =
    ∑ p ∈ E ×ˢ U, ∑ q ∈ R ×ˢ D,
      if remaining p.1 ∧ selected q.1 q.2 then
        cutoffMoebius ψ w p.1*v q.1*cutoffMoebius ψ w q.2*
          K ((p.1*p.2)*(q.1*q.2)) else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPairSupport, OAI.CubicFirstMoment.stoppedAlpha, OAI.CubicFirstMoment.stoppedBeta, OAI.CubicFirstMoment.cutoffMoebius

theorem OAI.CubicFirstMoment.stopped_coefficients_squarefree line 94

Source documentation

Enlarging the independent sums adds only terms killed individually by a kernel supported on squarefree products.

theorem stopped_coefficients_squarefree (R D E U : Finset Eisenstein)
    (v : Eisenstein → ℂ) (ψ : ℝ → ℝ) (w : ℝ)
    (selected : Eisenstein → Eisenstein → Prop) (remaining : Eisenstein → Prop)
    (K : Eisenstein → ℂ) (hK : ∀ n, ¬Squarefree n → K n = 0) :
    (∑ a ∈ primaryPairSupport E U, ∑ b ∈ primaryPairSupport R D,
      stoppedAlpha E U ψ w remaining a*stoppedBeta R D v ψ w selected b*K (a*b)) =
    ∑ p ∈ E ×ˢ U, ∑ q ∈ R ×ˢ D,
      if remaining p.1 ∧ selected q.1 q.2 ∧ Squarefree ((p.1*p.2)*(q.1*q.2)) then
        cutoffMoebius ψ w p.1*v q.1*cutoffMoebius ψ w q.2*
          K ((p.1*p.2)*(q.1*q.2)) else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPairSupport, OAI.CubicFirstMoment.stoppedAlpha, OAI.CubicFirstMoment.stoppedBeta, OAI.CubicFirstMoment.cutoffMoebius

lemma OAI.CubicFirstMoment.primaryPairFiber_card_le line 113
lemma OAI.CubicFirstMoment.primaryPairCoefficient_norm_le line 130