OAI/Combinatorics/LowSpaceSubsetSum/Counting/NestedPrimes.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The at-most-three-factor nested prime construction

An increment below four contributes the factor one. Larger increments use the actual prime range. Seed identities are retained in the product sampling space even when numerical factors coincide. This proves the size and collision bounds used in alg:filter-bounds without a coprimality premise.

  1. def OAI.LowSpaceSubsetSum.factorRange line 19
  2. theorem OAI.LowSpaceSubsetSum.factorRange_nonempty line 22
  3. theorem OAI.LowSpaceSubsetSum.factor_size_bounds line 27
  4. theorem OAI.LowSpaceSubsetSum.factor_divisor_probability_le line 51
  5. def OAI.LowSpaceSubsetSum.tripleRange line 69
  6. def OAI.LowSpaceSubsetSum.tripleModulus line 72
  7. theorem OAI.LowSpaceSubsetSum.tripleRange_nonempty line 74
  8. theorem OAI.LowSpaceSubsetSum.cumulative_moduli_dvd line 78
  9. theorem OAI.LowSpaceSubsetSum.triple_size_bounds line 82
  10. theorem OAI.LowSpaceSubsetSum.triple_divisor_probability_le line 103
  11. theorem OAI.LowSpaceSubsetSum.nested_size_bounds line 124

    Source documentation

    The real log scale differs from the total integer increments by less than one. All discarded increments and repeated factors are included.

    theorem nested_size_bounds {a b c u : ℕ} {L : ℝ} (hu : 256 ≤ u)
    (ha : a ≤ u) (hb : b ≤ u) (hc : c ≤ u)
    (hL0 : (a + b + c : ℕ) ≤ L) (hL1 : L < (a + b + c : ℕ) + 1)
    {z : (ℕ × ℕ) × ℕ} (hz : z ∈ tripleRange a b c) :
    (2 : ℝ) ^ L / (u : ℝ) ^ 5 ≤ tripleModulus z ∧
      (tripleModulus z : ℝ) ≤ (2 : ℝ) ^ L := by
…

    Mentions: OAI.LowSpaceSubsetSum.tripleRange, OAI.LowSpaceSubsetSum.tripleModulus

  12. theorem OAI.LowSpaceSubsetSum.nested_divisor_probability_le line 152
  13. def OAI.LowSpaceSubsetSum.tripleProbability line 177
  14. theorem OAI.LowSpaceSubsetSum.tripleProbability_sum line 180
  15. theorem OAI.LowSpaceSubsetSum.nested_pairwise_collision_bound line 188

    Source documentation

    The collision-energy interface is supplied for the actual product sampler, under the same polynomial-bit difference bound as the single prime.

    theorem nested_pairwise_collision_bound (X : Finset ℤ) {a b c u : ℕ} {L : ℝ}
    (hu : 256 ≤ u) (ha : a ≤ u) (hb : b ≤ u) (hc : c ≤ u)
    (hL1 : L < (a + b + c : ℕ) + 1)
    (hbits : ∀ x ∈ X, ∀ y ∈ X, (x - y).natAbs < 2 ^ (2 * u)) :
    PairwiseCollisionBound (tripleRange a b c) (tripleProbability a b c) X
      (fun z x => x % (tripleModulus z : ℤ)) ((u : ℝ) ^ 10 / (2 : ℝ) ^ L) := by
…

    Mentions: OAI.LowSpaceSubsetSum.PairwiseCollisionBound, OAI.LowSpaceSubsetSum.tripleRange, OAI.LowSpaceSubsetSum.tripleProbability, OAI.LowSpaceSubsetSum.tripleModulus

  16. theorem OAI.LowSpaceSubsetSum.nested_occupied_probability line 211