AmplificationScaleSum.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The convergent scale sum in the amplification second moment

theorem OAI.JointDickman.amplification_scale_sum line 12
theorem OAI.JointDickman.amplification_no_change_tendsto line 44
Source documentation
The no-change contribution, including the outside factor B, tends to zero.
```
theorem amplification_no_change_tendsto :
    Tendsto (fun B : ℕ => (B : ℝ) * (auxiliaryRatio B)^(-amplificationExponent))
      atTop (𝓝 0) := by
…
```
Mentions: OAI.JointDickman.auxiliaryRatio, OAI.JointDickman.amplificationExponent

theorem OAI.JointDickman.four_tail_coin_bound line 58

Source documentation

Four regular high-prime sets supply the exponent strictly exceeding one.

theorem four_tail_coin_bound {B Y C : ℝ} {n : ℕ}
    (hB : 0 < B) (hY : 0 < Y)
    (hn : 4 * ((2 / 5 : ℝ) * Real.log (B / Y) - C) ≤ (n : ℝ)) :
    (1 / 2 : ℝ)^n ≤ (2 : ℝ)^(4 * C) * (Y / B)^amplificationExponent := by
…

Mentions: OAI.JointDickman.amplificationExponent