OAI/NumberTheory/JointDickman/Amplification/BinLabelAmplification.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.binLabel_auxiliary_multipliers line 12
2. theorem OAI.JointDickman.binLabel_amplification_first_form line 27

   Source documentation

   The exact normalized first-form identity holds at all sufficiently large integer scales; no multiplicativity of the centered second factor is used.

   theorem binLabel_amplification_first_form {ι : Type*} [Fintype ι]
       (J : ℕ) (hJ : 0 < J) (k : ι → ℕ) (hk : ∀ i, 1 ≤ k i) (z : ι → ℂ)
       (B L : ℕ) (τ C : ℝ) (u : ℕ → ℝ) (v : ℕ → ℕ → ℝ) (H : ℕ → ℕ → ℂ) :
       ∀ᶠ N : ℕ in atTop,
         (∑ n ∈ range N, (star (binLabel (fun i => primeBin (N : ℝ) J (k i)) z n) * H N n) *
           (arithmeticSubsetAmplification B L τ C (fun a c => u c * v a c) n : ℂ)) / (N : ℂ) =
         (1 / (B : ℂ)) * firstDivisorForm B L τ C u v
           (binLabel (fun i => primeBin (N : ℝ) J (k i)) z) (H N) N := by
   …

   Mentions: OAI.JointDickman.binLabel, OAI.JointDickman.primeBin, OAI.JointDickman.arithmeticSubsetAmplification, OAI.JointDickman.firstDivisorForm