OAI/NumberTheory/JointDickman/Probability/HighCoinExponent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The four high-prime factors after averaging the remaining subsets

  1. theorem OAI.JointDickman.high_coin_cutoff_identity line 10

    Source documentation

    The count cutoff's fourth power is exactly the required scale decay.

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

    Mentions: OAI.JointDickman.amplificationExponent

  2. theorem OAI.JointDickman.high_coin_four_factor_bound line 25