OAI/NumberTheory/JointDickman/Amplification/MultiplicityRates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.halfPoissonRate line 10
2. def OAI.JointDickman.halfRankinExponent line 11
3. theorem OAI.JointDickman.halfRankin_sub_halfPoisson line 15

   Source documentation

   This identity is responsible for cancellation of the numeric sieve and inclusion probability exponents. The conventions at zero agree.

   theorem halfRankin_sub_halfPoisson (r : ℝ) :
       halfRankinExponent r-halfPoissonRate (1/2-r) = (1/2)*Real.binEntropy (2*r) := by
   …

   Mentions: OAI.JointDickman.halfRankinExponent, OAI.JointDickman.halfPoissonRate

4. theorem OAI.JointDickman.halfPoisson_clamped_chernoff line 26

   Source documentation

   A clamped exponential parameter handles the endpoint u=0 without an infinite tilt. The loss is at most the chosen positive clamp δ.

   theorem halfPoisson_clamped_chernoff {u δ : ℝ} (hu : 0 ≤ u) (hu1 : u ≤ 1/2)
       (hδ : 0 < δ) (hδ1 : δ ≤ 1/2) :
       let t := -Real.log (2*max δ u)
   …