OAI/NumberTheory/JointDickman/Amplification/AmplificationReindex.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Reindexing the actual arithmetic amplification into a divisor form

  1. def OAI.JointDickman.arithmeticResidueWeight line 10
  2. def OAI.JointDickman.amplificationDivisorForm line 14
  3. theorem OAI.JointDickman.sum_two_divisors_reindex line 24
  4. theorem OAI.JointDickman.arithmeticAmplification_reindex line 34

    Source documentation

    The finite first-form identity, including the precise endpoint.

    theorem arithmeticAmplification_reindex (B L : ℕ) (τ C : ℝ)
    (w : ℕ → ℕ → ℝ) (H : ℕ → ℂ) (N : ℕ) :
    (∑ n ∈ range N, H n * (arithmeticSubsetAmplification B L τ C w n : ℂ)) =
      (1 / (B : ℂ)) * amplificationDivisorForm B L τ C w H N := by
…

    Mentions: OAI.JointDickman.arithmeticSubsetAmplification, OAI.JointDickman.amplificationDivisorForm