OAI/NumberTheory/CubicMoment/Decomposition/StoppedSelectedReindex.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original selected-divisor sum is exactly the finite collection of free-prime rows. Its squarefree support, global largest-prime choice, output interval, exclusion and stopping predicates are all retained.

  1. def OAI.CubicFirstMoment.selectedStoppedDivisorSet line 13
  2. def OAI.CubicFirstMoment.selectedStoppedRowPairs line 21
  3. lemma OAI.CubicFirstMoment.selectedStopped_forward line 28
  4. lemma OAI.CubicFirstMoment.selectedStopped_backward line 62
  5. theorem OAI.CubicFirstMoment.selectedStopped_sum_reindex line 97

    Source documentation

    Every original selected-divisor term occurs exactly once.

    theorem selectedStopped_sum_reindex (B ρ a b : ℝ) (j j₀ k h : ℕ) (Z Q : ℝ)
    (early : Bool) (r e : Eisenstein) (hr : primary r) (hbB : b ≤ B)
    (F : Eisenstein → ℂ) :
    (∑ d ∈ selectedStoppedDivisorSet B ρ a b j j₀ k h Z Q early r e, F d) =
      ∑ t ∈ selectedStoppedRowPairs B ρ a b j j₀ k h Z Q early r e, F (t.2*t.1) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.selectedStoppedDivisorSet, OAI.CubicFirstMoment.selectedStoppedRowPairs