ResidueFilters.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact counts under uniform low-residue choices

Raw occurrence identities and distinct entry keys may be different types. Neither is deduplicated here: each supplied finite set is partitioned by its residue labels. This is the exact uniform-residue calculation for the counts G, J, and U in the resource proof.

def OAI.LowSpaceSubsetSum.normalizedResidue line 22
theorem OAI.LowSpaceSubsetSum.normalizedResidue_eq_iff line 28
theorem OAI.LowSpaceSubsetSum.sum_label_fibers line 42
theorem OAI.LowSpaceSubsetSum.mean_label_fiber line 48
def OAI.LowSpaceSubsetSum.residueFiltered line 55
theorem OAI.LowSpaceSubsetSum.mean_residueFiltered line 58
def OAI.LowSpaceSubsetSum.twiceResidueFiltered line 63

theorem OAI.LowSpaceSubsetSum.mean_twiceResidueFiltered line 70

Source documentation

Each raw four-leaf occurrence passes one and only one parent/first-child residue pair. The second child's required residue follows by nesting.

theorem mean_twiceResidueFiltered {p q : ℕ} (hp : 0 < p) (hq : 0 < q)
    (T : Finset α) (parent child : α → ℤ) :
    (∑ r : Fin p × Fin q, ((twiceResidueFiltered hp hq T parent child r).card : ℝ)) /
      (p * q : ℕ) = (T.card : ℝ) / (p * q : ℕ) := by
…

Mentions: OAI.LowSpaceSubsetSum.twiceResidueFiltered

theorem OAI.LowSpaceSubsetSum.finite_count_markov line 80

Source documentation

Finite Markov bound for a counted resource. No independence between different resources is required when these marginal bounds are combined.

theorem finite_count_markov {Ω : Type*} [Fintype Ω] [DecidableEq Ω] [Nonempty Ω]
    (count : Ω → ℕ) {T : ℝ} (hT : 0 < T) :
    (((Finset.univ.filter fun r => T < (count r : ℝ)).card : ℝ) / Fintype.card Ω) ≤
      ((∑ r : Ω, (count r : ℝ)) / Fintype.card Ω) / T := by
…

theorem OAI.LowSpaceSubsetSum.residueFiltered_tail line 99
theorem OAI.LowSpaceSubsetSum.twiceResidueFiltered_tail line 107