OAI/NumberTheory/JointDickman/Amplification/RegularOmissionChoices.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.regularOmissionChoices line 12
2. theorem OAI.JointDickman.regularOmissionChoices_count line 19

   Source documentation

   Encoding the omitted primes by their portions below and above the prefix keeps the exact addition cardinality in the entropy window.

   theorem regularOmissionChoices_count {B L k : ℕ} {τ C : ℝ}
       (A U : Finset ℕ) (d : ℕ) (hL : 1 ≤ L) (hk : k ∈ Icc 1 L)
       (hτ : 0 ≤ τ) (hℓ : 0 < auxiliaryLogLength B)
       (hA : RegularPrimeSet B L τ C A) (hU : RegularPrimeSet B L τ C U) :
       (regularOmissionChoices B L k τ C A U d).card ≤
         (subsetCardWindow (A ∩ primePrefix B ((k : ℝ)/L) (A ∪ U))
           (auxiliaryLogLength B) ((k : ℝ)/L)
           (min ((d : ℝ)/(((k : ℝ)/L)*auxiliaryLogLength B)) (1/2)) τ).card *
         (((A \ primePrefix B ((k : ℝ)/L) (A ∪ U)).powerset).filter
           (fun R => (R.card : ℝ) ≤ 4*τ*auxiliaryLogLength B)).card := by
   …

   Mentions: OAI.JointDickman.auxiliaryLogLength, OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.regularOmissionChoices, OAI.JointDickman.subsetCardWindow, OAI.JointDickman.primePrefix