RepresentationResidues.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Adaptive residue hits for the surviving representatives

The top residue is exposed first. A fixed deterministic representative on that hit determines both child shifts, after which the two independent child residues are exposed. Collision bounds use the shared nested-prime seed; independence of the three moduli is unnecessary.

theorem OAI.LowSpaceSubsetSum.normalizedResidue_cast line 21
theorem OAI.LowSpaceSubsetSum.normalizedResidue_eq_normalizedResidue_iff line 25
theorem OAI.LowSpaceSubsetSum.normalizedResidue_eq_modEq line 29
def OAI.LowSpaceSubsetSum.residueTranslation line 35
theorem OAI.LowSpaceSubsetSum.residueTranslation_apply line 48
theorem OAI.LowSpaceSubsetSum.normalizedResidue_image_card line 54
def OAI.LowSpaceSubsetSum.shiftedResidueHit line 69
theorem OAI.LowSpaceSubsetSum.shiftedResidueHit_probability line 72
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_product_and line 92
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_prod_average_left line 107

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_adaptive_lower line 117

Source documentation

A preceding hit may determine the later event, with a uniform lower bound for every successful preceding outcome.

theorem finiteUniformProbability_adaptive_lower {Ω Ψ : Type*}
    [Fintype Ω] [Nonempty Ω] [Fintype Ψ]
    (P : Ω → Prop) (Q : Ω → Ψ → Prop) {p q : ℝ}
    (hq : 0 ≤ q) (hP : p ≤ finiteUniformProbability P)
    (hQ : ∀ x, P x → q ≤ finiteUniformProbability (Q x)) :
    p * q ≤ finiteUniformProbability (fun z : Ω × Ψ => P z.1 ∧ Q z.1 z.2) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

def OAI.LowSpaceSubsetSum.chosenTopRepresentative line 137
Source documentation
The top witness is fixed before either child residue is inspected.
```
noncomputable def chosenTopRepresentative {p : ℕ} (hp : 0 < p)
    (X : Finset ℤ) (c : ℤ) (r : Fin p) : ℤ := by
…
```
theorem OAI.LowSpaceSubsetSum.chosenTopRepresentative_spec line 142
def OAI.LowSpaceSubsetSum.adaptiveResidueHits line 150
theorem OAI.LowSpaceSubsetSum.shiftedResidueHit_lower line 157
theorem OAI.LowSpaceSubsetSum.independent_child_hits_probability line 164
theorem OAI.LowSpaceSubsetSum.adaptiveResidueHits_probability line 181
def OAI.LowSpaceSubsetSum.compatibleRepresentativeResidues line 209
theorem OAI.LowSpaceSubsetSum.adaptiveResidueHits_compatible line 221

theorem OAI.LowSpaceSubsetSum.compatibleRepresentativeResidues_probability line 246

Source documentation

All parent and complementary-child filters hold with the adaptive hit probability; shared factors require divisibility, not coprimality.

theorem compatibleRepresentativeResidues_probability {p0 pL pR : ℕ}
    (h0 : 0 < p0) (hL : 0 < pL) (hR : 0 < pR)
    (hdivL : pL ∣ p0) (hdivR : pR ∣ p0)
    (X0 XL XR : Finset ℤ) (c0 t : ℤ) (cL cR : ℤ → ℤ)
    (u : ℝ) (hu : 0 < u)
    (hX0 : (p0 : ℝ) / u ^ 16 ≤ (X0.image (fun x => x % (p0 : ℤ))).card)
    (hXL : (pL : ℝ) / u ^ 16 ≤ (XL.image (fun x => x % (pL : ℤ))).card)
    (hXR : (pR : ℝ) / u ^ 16 ≤ (XR.image (fun x => x % (pR : ℤ))).card) :
    1 / u ^ 48 ≤ finiteUniformProbability
      (compatibleRepresentativeResidues (p0 := p0) (pL := pL) (pR := pR)
…

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

theorem OAI.LowSpaceSubsetSum.uniform_probability_filter_sum line 261

theorem OAI.LowSpaceSubsetSum.retained_family_energy_mean_bound line 269

Source documentation

The retained-family size pays for the diagonal collisions.

theorem retained_family_energy_mean_bound (X : Finset ℤ) (L u : ℝ) (hu : 2 ≤ u)
    (hsize : (2 : ℝ) ^ L / u ^ 14 ≤ X.card) :
    (X.card : ℝ) + (u ^ 10 / (2 : ℝ) ^ L) * (X.card : ℝ) ^ 2 ≤
      u ^ 15 * (X.card : ℝ) ^ 2 / (2 : ℝ) ^ L := by
…

theorem OAI.LowSpaceSubsetSum.uniform_energy_good_probability line 297

Source documentation

Uniform-law energy control needs only the pairwise marginal collision bound, even when this modulus shares factors with other moduli.

theorem uniform_energy_good_probability {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (X : Finset ℤ) (hash : Ω → ℤ → ℤ) (L u : ℝ) (hu : 2 ≤ u)
    (hsize : (2 : ℝ) ^ L / u ^ 14 ≤ X.card)
    (hcollision : ∀ x ∈ X, ∀ y ∈ X, x ≠ y →
      finiteUniformProbability (fun ω => hash ω x = hash ω y) ≤ u ^ 10 / (2 : ℝ) ^ L) :
    1 - 1 / u ≤ finiteUniformProbability
      (fun ω => (collisionEnergy X (hash ω) : ℝ) ≤
        u ^ 16 * (X.card : ℝ) ^ 2 / (2 : ℝ) ^ L) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability, OAI.LowSpaceSubsetSum.collisionEnergy

theorem OAI.LowSpaceSubsetSum.three_moduli_energy_probability line 329