SeparatorFamilies.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Finite random separating families

For one fixed disjoint pair of masks, the separating subsets are counted exactly. A family is a uniformly chosen function from its index set to the set of eligible subsets: repeated sets retain distinct indices. Its point probabilities factor, so this is independent sampling with replacement, as required in the manuscript.

def OAI.LowSpaceSubsetSum.finiteUniformProbability line 22
Source documentation
Cardinal-ratio form of the uniform law on a finite sample space.
```
noncomputable def finiteUniformProbability {Ω : Type*} [Fintype Ω] (P : Ω → Prop) : ℝ := by
…
```
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_eq_pmf line 26
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_nonneg line 35
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_le_one line 41
theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_compl line 48

theorem OAI.LowSpaceSubsetSum.uniform_family_point_probability line 58

Source documentation

Every coordinate has the uniform law and the joint point mass is their product.

theorem uniform_family_point_probability {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (ν : ℕ) (f : Fin ν → Ω) :
    PMF.uniformOfFintype (Fin ν → Ω) f =
      ∏ i : Fin ν, PMF.uniformOfFintype Ω (f i) := by
…

theorem OAI.LowSpaceSubsetSum.uniform_family_failure line 65

Source documentation

Exact failure probability for independent uniform draws, including repeated samples.

theorem uniform_family_failure {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (P : Ω → Prop) (ν : ℕ) :
    finiteUniformProbability (fun f : Fin ν → Ω => ∀ i, ¬P (f i)) =
      (1 - finiteUniformProbability P) ^ ν := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

theorem OAI.LowSpaceSubsetSum.uniform_family_coverage line 89

theorem OAI.LowSpaceSubsetSum.finiteUniformProbability_exists_le_sum line 99

Source documentation

Finite union bound; the events need not be independent.

theorem finiteUniformProbability_exists_le_sum {Ω K : Type*}
    [Fintype Ω] [Nonempty Ω] [Fintype K] (P : K → Ω → Prop) :
    finiteUniformProbability (fun ω => ∃ i, P i ω) ≤
      ∑ i, finiteUniformProbability (P i) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

theorem OAI.LowSpaceSubsetSum.four_family_union_bound line 118

Source documentation

The four-block coverage conclusion uses only the four marginal bounds.

theorem four_family_union_bound {Ω : Type*} [Fintype Ω] [Nonempty Ω]
    (Q : Fin 4 → Ω → Prop)
    (hQ : ∀ i, 1 - Real.exp (-10) ≤ finiteUniformProbability (Q i)) :
    1 - 4 * Real.exp (-10) ≤ finiteUniformProbability (fun ω => ∀ i, Q i ω) := by
…

Mentions: OAI.LowSpaceSubsetSum.finiteUniformProbability

theorem OAI.LowSpaceSubsetSum.separating_family_failure_bound line 136
def OAI.LowSpaceSubsetSum.separatingSubsets line 152
Source documentation
Eligible subsets that contain the left mask and avoid the right mask.
```
def separatingSubsets (U L R : Finset ι) (e : ℕ) : Finset (Finset ι) :=
…
```
theorem OAI.LowSpaceSubsetSum.separatingSubsets_eq line 155
theorem OAI.LowSpaceSubsetSum.card_separatingSubsets line 162

theorem OAI.LowSpaceSubsetSum.uniform_separation_probability line 172

Source documentation

The exact one-draw probability for a fixed disjoint pair of masks.

theorem uniform_separation_probability (U L R : Finset ι) (e : ℕ)
    (hL : L ⊆ U) (hR : R ⊆ U) (hdisj : Disjoint L R)
    (he0 : L.card ≤ e) (he : e ≤ U.card) :
    ((PMF.uniformOfFinset (U.powersetCard e) (Finset.powersetCard_nonempty.mpr he)).toOuterMeasure
      {S | L ⊆ S ∧ Disjoint S R}).toReal =
      (Nat.choose (U.card - R.card - L.card) (e - L.card) : ℝ) / Nat.choose U.card e := by
…

theorem OAI.LowSpaceSubsetSum.card_separatingSubsets_half line 183
abbrev OAI.LowSpaceSubsetSum.SeparatorSample line 193
Source documentation
One sample is an indexed, fixed-size subset of the block.
```
abbrev SeparatorSample (U : Finset ι) (e : ℕ) := {S : Finset ι // S ∈ U.powersetCard e}
```
theorem OAI.LowSpaceSubsetSum.separatorSample_success_probability line 195

theorem OAI.LowSpaceSubsetSum.separator_family_coverage line 220

Source documentation

Coverage of a fixed mask pair by the paper's sampled family.

theorem separator_family_coverage (U L R : Finset ι) (e : ℕ)
    (hL : L ⊆ U) (hR : R ⊆ U) (hdisj : Disjoint L R)
    (he0 : L.card ≤ e) (he : e ≤ U.card)
    (heven : 2 ∣ U.card) (hhalf : L.card + R.card = U.card / 2)
    (hfeas : e - L.card ≤ U.card / 2) :
    let θ : ℝ := (Nat.choose (U.card / 2) (e - L.card) : ℝ) / Nat.choose U.card e
…