OAI/NumberTheory/JointDickman/Amplification/OmissionEnvelope.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An omission envelope independent of the random remainder

  1. def OAI.JointDickman.omissionEnvelope line 13

    Source documentation

    The old-prime choices can be enumerated before drawing the other remainder. This is essential when applying the inclusion bound to a fixed numeric addition.

    noncomputable def omissionEnvelope (B L k : ℕ) (τ : ℝ) (A : Finset ℕ) (d : ℕ) : Finset (Finset ℕ) :=
…
  2. theorem OAI.JointDickman.regular_omission_mem_envelope line 20
  3. theorem OAI.JointDickman.omissionEnvelope_count line 49
  4. theorem OAI.JointDickman.omissionEnvelope_entropy line 79