OAI/Combinatorics/LowSpaceSubsetSum/Counting/NestedOccupancy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous occupancy for the actual nested prime sampler

All three moduli are prefixes of one sampled factor tuple. Projection to the first one or two factors has the exact uniform marginal. The three energy estimates are therefore combined by a union bound on that one space.

  1. theorem OAI.LowSpaceSubsetSum.triple_prefixTwo_probability line 17
  2. theorem OAI.LowSpaceSubsetSum.triple_prefixOne_probability line 29
  3. theorem OAI.LowSpaceSubsetSum.nested_uniform_collision_probability line 40
  4. def OAI.LowSpaceSubsetSum.prefixModulus line 58
  5. def OAI.LowSpaceSubsetSum.prefixExponent line 61
  6. theorem OAI.LowSpaceSubsetSum.factorRange_pos line 63
  7. theorem OAI.LowSpaceSubsetSum.prefixModulus_pos line 69
  8. theorem OAI.LowSpaceSubsetSum.prefixModulus_nested line 81
  9. theorem OAI.LowSpaceSubsetSum.nested_prefix_collision_probability line 86
  10. theorem OAI.LowSpaceSubsetSum.nested_simultaneous_energy_probability line 133
  11. theorem OAI.LowSpaceSubsetSum.occupied_of_retained_energy line 149
  12. theorem OAI.LowSpaceSubsetSum.nested_simultaneous_occupancy_probability line 161
  13. theorem OAI.LowSpaceSubsetSum.prefixModulus_upper line 177
  14. theorem OAI.LowSpaceSubsetSum.nested_simultaneous_fraction_probability line 212

    Source documentation

    The normalized occupied-class fraction feeds the following uniform top/child residue experiment.

    theorem nested_simultaneous_fraction_probability {a b c u : ℕ}
    (hu : 256 ≤ u) (ha : a ≤ u) (hb : b ≤ u) (hc : c ≤ u)
    (X : Fin 3 → Finset ℤ) (L : Fin 3 → ℝ)
    (hL0 : ∀ i, (prefixExponent a b c i : ℝ) ≤ L i)
    (hL1 : ∀ i, L i < (prefixExponent a b c i : ℝ) + 1)
    (hsize : ∀ i, (2 : ℝ) ^ L i / (u : ℝ) ^ 14 ≤ (X i).card)
    (hbits : ∀ i x, x ∈ X i → ∀ y, y ∈ X i → (x - y).natAbs < 2 ^ (2 * u)) :
    1 - 3 / (u : ℝ) ≤ finiteUniformProbability
      (fun z : ↥(tripleRange a b c) => ∀ i,
        (prefixModulus z.val i : ℝ) / (u : ℝ) ^ 16 ≤
          ((X i).image (fun x => x % (prefixModulus z.val i : ℤ))).card) := by
…

    Mentions: OAI.LowSpaceSubsetSum.prefixExponent, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.tripleRange, OAI.LowSpaceSubsetSum.prefixModulus

  15. theorem OAI.LowSpaceSubsetSum.nested_seed_compatible_probability line 231

    Source documentation

    On each good common prime seed, the subsequent actual uniform residue draws retain compatible representatives with probability at least u⁻⁴⁸.

    theorem nested_seed_compatible_probability {a b c : ℕ} (z : ↥(tripleRange a b c))
    (X : Fin 3 → Finset ℤ) (c0 t : ℤ) (cL cR : ℤ → ℤ) (u : ℝ) (hu : 0 < u)
    (hoccupied : ∀ i, (prefixModulus z.val i : ℝ) / u ^ 16 ≤
      ((X i).image (fun x => x % (prefixModulus z.val i : ℤ))).card) :
    1 / u ^ 48 ≤ finiteUniformProbability
      (compatibleRepresentativeResidues
        (p0 := prefixModulus z.val 0) (pL := prefixModulus z.val 1)
…

    Mentions: OAI.LowSpaceSubsetSum.tripleRange, OAI.LowSpaceSubsetSum.prefixModulus, OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.compatibleRepresentativeResidues