OAI/Combinatorics/LowSpaceSubsetSum/Separators/SeparatorConcreteIncidence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Both incidence bounds for the actual rounded separating families

  1. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.choose_diagonal_le line 12
  2. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.separator_denominator_le line 19
  3. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_containment_incidence line 25
  4. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.complement_rounding line 48

    Source documentation

    Complementing both prescribed counts preserves their rounding errors. This supplies the right-array bound from the same sharp entropy estimate.

    theorem complement_rounding (g c e : ℕ) (heven : 2 ∣ g) (hcHalf : c ≤ g / 2)
    (heg : e ≤ g) (k : ℝ) :
    ((g / 2 - c : ℕ) : ℝ) - (g : ℝ) * (1 / 2 - k) =
        -((c : ℝ) - (g : ℝ) * k) ∧
    ((g - e : ℕ) : ℝ) - (g : ℝ) * ((1 / 2 - k) + separatorY (1 / 2 - k)) =
        -((e : ℝ) - (g : ℝ) * (k + separatorY k)) := by
…

    Mentions: OAI.LowSpaceSubsetSum.separatorY

  5. theorem OAI.LowSpaceSubsetSum.SeparatorExpectation.rounded_avoidance_incidence line 59