OAI/Combinatorics/ParityLifts/SparseBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ParityWL.Complexity.cnf_card_bound line 7
  2. def OAI.ParityWL.Complexity.ClauseControlled line 29

    Source documentation

    Finite-memory invariant: stored representatives, not just their sets.

    def ClauseControlled {α : Type} [TreeCodec α] (S : ℕ) (C : List α) : Prop :=
…

    Mentions: OAI.ParityWL.Complexity.TreeCodec

  3. def OAI.ParityWL.Complexity.ListControlled line 32
  4. lemma OAI.ParityWL.Complexity.ClauseControlled.subset line 35
  5. lemma OAI.ParityWL.Complexity.ListControlled.width line 39
  6. lemma OAI.ParityWL.Complexity.ListControlled.size line 45
  7. lemma OAI.ParityWL.Complexity.compact_controlled line 64
  8. lemma OAI.ParityWL.Complexity.minimize_controlled line 68
  9. lemma OAI.ParityWL.Complexity.prune_controlled line 74
  10. lemma OAI.ParityWL.Complexity.selected_controlled line 83
  11. lemma OAI.ParityWL.Complexity.sparseStep_controlled line 103
  12. lemma OAI.ParityWL.Complexity.SparseTree.controlled line 121