OAI/NumberTheory/JointDickman/Amplification/AmplificationMultiplier.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.amplificationMultiplier line 11
2. theorem OAI.JointDickman.amplificationMultiplier_comparable line 13
3. theorem OAI.JointDickman.amplificationMultiplier_valid line 28
4. theorem OAI.JointDickman.power_div_amplificationMultiplier line 38
5. theorem OAI.JointDickman.regular_pair_cap_negligible line 58

   Source documentation

   Both regular weights together are bounded by one power strictly below T's exponent, uniformly in the later tail cutoff.

   theorem regular_pair_cap_negligible {L : ℕ} (hL : 1 ≤ L) {τ : ℝ}
       (hτ : 0 ≤ τ) (hτsmall : τ ≤ samplingTau) :
       ∃ Q : ℕ → ℝ,
         Tendsto (fun B => Q B / amplificationMultiplier B) atTop (nhds 0) ∧
         ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (a : ℕ) (S : Finset ℕ),
           regularCoefficientWeight B L τ C a * regularResidueWeight B L τ C S ≤ Q B := by
   …

   Mentions: OAI.JointDickman.samplingTau, OAI.JointDickman.amplificationMultiplier, OAI.JointDickman.regularCoefficientWeight, OAI.JointDickman.regularResidueWeight