AmplificationHighCoins.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact high-prime no-change probability

def OAI.JointDickman.highPrimePart line 12
def OAI.JointDickman.highCoinAgreement line 16
theorem OAI.JointDickman.highCoinAgreement_eq line 22
Source documentation
Fair coins preserve every specified high-prime assignment with this exact probability.
```
theorem highCoinAgreement_eq (Y : ℝ) (S : Finset ℕ) (keep : Bool) :
    highCoinAgreement Y S keep = (1 / 2 : ℝ)^(highPrimePart Y S).card := by
…
```
Mentions: OAI.JointDickman.highCoinAgreement, OAI.JointDickman.highPrimePart

theorem OAI.JointDickman.regular_four_high_coin_bound line 33

Source documentation

Four independent sets of fair second coins, for two selected and two remaining subsets. The high-prime lower cutoffs give the full exponent 1.6 log 2.

theorem regular_four_high_coin_bound {B L i : ℕ} {τ C : ℝ} {A D R Q : Finset ℕ}
    (hB : 0 < (B : ℝ)) (hY : 0 < primeTailEndpoint B i)
    (hA : RegularPrimeSet B L τ C A) (hD : RegularPrimeSet B L τ C D)
    (hR : RegularPrimeSet B L τ C R) (hQ : RegularPrimeSet B L τ C Q) :
    highCoinAgreement (primeTailEndpoint B i) A true *
      highCoinAgreement (primeTailEndpoint B i) D true *
      highCoinAgreement (primeTailEndpoint B i) R false *
      highCoinAgreement (primeTailEndpoint B i) Q false ≤
      (2 : ℝ)^(4 * C) * (primeTailEndpoint B i / B)^amplificationExponent := by
…

Mentions: OAI.JointDickman.primeTailEndpoint, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.highCoinAgreement, OAI.JointDickman.amplificationExponent