OAI/Combinatorics/ParityLifts/SparseStates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Sparsification.bernoulli_split line 7
  2. def OAI.Sparsification.branchBase line 30
  3. lemma OAI.Sparsification.branchBase_gt_one line 32
  4. lemma OAI.Sparsification.split_units line 38
  5. lemma OAI.Sparsification.split_binary line 45
  6. structure OAI.Sparsification.State line 59
  7. def OAI.Sparsification.State.spent line 69
  8. lemma OAI.Sparsification.State.spent_bound line 71
  9. lemma OAI.Sparsification.minimize_subset line 80
  10. def OAI.Sparsification.initialState line 82
  11. lemma OAI.Sparsification.singleton_reduced line 95
  12. lemma OAI.Sparsification.prune_width line 100
  13. lemma OAI.Sparsification.survived_sub_binaries line 108
  14. def OAI.Sparsification.State.addUnits line 116
  15. lemma OAI.Sparsification.State.spent_addUnits line 129
  16. def OAI.Sparsification.State.addBinaries line 135
  17. lemma OAI.Sparsification.State.spent_addBinaries line 156
  18. structure OAI.Sparsification.Split line 168

    Source documentation

    A split stores its actual successor states, progress and the exact semantic branching equation. Its numerical inequality is proved for the three cases.

    structure Split {r : ℕ} (s : State α (r ^ 2)) where
…

    Mentions: OAI.Sparsification.State

  19. def OAI.Sparsification.Terminal line 180
  20. lemma OAI.Sparsification.state_terminal_or_split line 184