ResidueCoverage.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Collision energy and occupied residue classes

The collision-to-occupancy argument is used in §6 of A Low-Space Algorithm for Worst-Case Subset Sum. Its published antecedents are Austrin, Kaski, Koivisto and Nederlof, Dense Subset Sum May Be the Hardest, STACS 2016, Proposition 3.5, and Nederlof and Węgrzycki, Improving Schroeppel and Shamir's Algorithm for Subset Sum via Orthogonal Vectors, arXiv:2010.08576v2, Lemma 3.2, especially equation (1) and the following Cauchy–Schwarz argument.

Those published statements assume exponentially bounded integer weights. The finite collision-to-occupancy bound instead takes the collision estimate as an explicit hypothesis. The manuscript's prime-factor estimate supplies that hypothesis for polynomial-bit inputs.

def OAI.LowSpaceSubsetSum.fiberSize line 32
Source documentation
The multiplicity of one image value, counting the distinct elements of X.
```
def fiberSize (X : Finset α) (f : α → β) (b : β) : ℕ :=
…
```
def OAI.LowSpaceSubsetSum.collisionEnergy line 36
Source documentation
The sum of squared residue-class sizes.
```
def collisionEnergy (X : Finset α) (f : α → β) : ℕ :=
…
```
def OAI.LowSpaceSubsetSum.collisionPairs line 40
Source documentation
Ordered collisions include diagonal pairs.
```
def collisionPairs (X : Finset α) (f : α → β) : Finset (α × α) :=
…
```
theorem OAI.LowSpaceSubsetSum.sum_fiberSize line 43
theorem OAI.LowSpaceSubsetSum.card_sq_le_occupied_mul_energy line 49
Source documentation
The deterministic Cauchy–Schwarz step: a small collision energy forces many distinct occupied residue classes.
```
theorem card_sq_le_occupied_mul_energy (X : Finset α) (f : α → β) :
    X.card ^ 2 ≤ (X.image f).card * collisionEnergy X f := by
…
```
Mentions: OAI.LowSpaceSubsetSum.collisionEnergy
theorem OAI.LowSpaceSubsetSum.collisionEnergy_eq_card_pairs line 58
theorem OAI.LowSpaceSubsetSum.collisionEnergy_eq_sum_pairs line 75
theorem OAI.LowSpaceSubsetSum.occupied_ge_of_energy_le line 85
Source documentation
A pointwise collision-energy bound gives a quantitative occupied-class bound. The statement uses real cardinalities to avoid integer rounding.
```
theorem occupied_ge_of_energy_le (X : Finset α) (f : α → β)
    {T : ℝ} (hT : 0 < T) (henergy : (collisionEnergy X f : ℝ) ≤ T) :
    (X.card : ℝ) ^ 2 / T ≤ (X.image f).card := by
…
```
Mentions: OAI.LowSpaceSubsetSum.collisionEnergy
def OAI.LowSpaceSubsetSum.PairwiseCollisionBound line 97
Source documentation
The smallest probabilistic interface needed from a random modulus: every distinct pair has collision probability at most δ. The weights prob form a finite probability distribution on seeds.
```
def PairwiseCollisionBound (seeds : Finset Ω) (prob : Ω → ℝ)
    (X : Finset α) (hash : Ω → α → β) (δ : ℝ) : Prop :=
…
```

theorem OAI.LowSpaceSubsetSum.expected_energy_le line 104

Source documentation

The published collision-energy calculation, for an arbitrary finite sampling law and with its exact collision bound exposed as a hypothesis.

theorem expected_energy_le (seeds : Finset Ω) (prob : Ω → ℝ)
    (X : Finset α) (hash : Ω → α → β) {δ : ℝ}
    (hprob : ∑ ω ∈ seeds, prob ω = 1) (hδ : 0 ≤ δ)
    (hcollision : PairwiseCollisionBound seeds prob X hash δ) :
    (∑ ω ∈ seeds, prob ω * (collisionEnergy X (hash ω) : ℝ)) ≤
      X.card + δ * (X.card : ℝ) ^ 2 := by
…

Mentions: OAI.LowSpaceSubsetSum.PairwiseCollisionBound, OAI.LowSpaceSubsetSum.collisionEnergy

theorem OAI.LowSpaceSubsetSum.probability_energy_le line 137

Source documentation

A finite-law Markov bound, retaining precisely the good event needed for the occupancy argument.

theorem probability_energy_le (seeds : Finset Ω) (prob : Ω → ℝ)
    (X : Finset α) (hash : Ω → α → β)
    (hnonneg : ∀ ω ∈ seeds, 0 ≤ prob ω)
    (hprob : ∑ ω ∈ seeds, prob ω = 1)
    {M T : ℝ} (hT : 0 < T)
    (hmean : (∑ ω ∈ seeds, prob ω * (collisionEnergy X (hash ω) : ℝ)) ≤ M) :
    1 - M / T ≤
      ∑ ω ∈ seeds.filter (fun ω => (collisionEnergy X (hash ω) : ℝ) ≤ T), prob ω := by
…

Mentions: OAI.LowSpaceSubsetSum.collisionEnergy

theorem OAI.LowSpaceSubsetSum.occupied_probability_of_collision_bound line 179

Source documentation

Collision bounds imply a lower bound on the probability of many occupied classes. This includes the Markov and Cauchy–Schwarz steps, rather than assuming the desired occupancy conclusion.

theorem occupied_probability_of_collision_bound
    (seeds : Finset Ω) (prob : Ω → ℝ)
    (X : Finset α) (hash : Ω → α → β)
    (hnonneg : ∀ ω ∈ seeds, 0 ≤ prob ω)
    (hprob : ∑ ω ∈ seeds, prob ω = 1)
    {δ T : ℝ} (hδ : 0 ≤ δ) (hT : 0 < T)
    (hcollision : PairwiseCollisionBound seeds prob X hash δ) :
    1 - ((X.card : ℝ) + δ * (X.card : ℝ) ^ 2) / T ≤
      ∑ ω ∈ seeds.filter
        (fun ω => (X.card : ℝ) ^ 2 / T ≤ ((X.image (hash ω)).card : ℝ)), prob ω := by
…

Mentions: OAI.LowSpaceSubsetSum.PairwiseCollisionBound