OAI/Combinatorics/HadwigerCounterexample/AtomFlavors.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Atom Flavors

  1. abbrev OAI.HadwigerCounterexample.Flavor line 15
  2. abbrev OAI.HadwigerCounterexample.Flavor.full line 17
  3. abbrev OAI.HadwigerCounterexample.Flavor.sharedOnly line 18
  4. abbrev OAI.HadwigerCounterexample.Flavor.pure line 19
  5. def OAI.HadwigerCounterexample.Flavor.keeps line 21
  6. instance OAI.HadwigerCounterexample.Flavor.(instance at line 28) line 28
  7. theorem OAI.HadwigerCounterexample.Flavor.keep_o line 31
  8. theorem OAI.HadwigerCounterexample.Flavor.keepZ line 37
  9. theorem OAI.HadwigerCounterexample.Flavor.keepSharp line 39
  10. abbrev OAI.HadwigerCounterexample.Knobs line 44
  11. def OAI.HadwigerCounterexample.lit line 46
  12. theorem OAI.HadwigerCounterexample.lit_allows line 49
  13. def OAI.HadwigerCounterexample.useAtom line 53
  14. theorem OAI.HadwigerCounterexample.mem_useAtom line 55
  15. abbrev OAI.HadwigerCounterexample.ProbeIdx line 59
  16. abbrev OAI.HadwigerCounterexample.Digest line 60
  17. def OAI.HadwigerCounterexample.asBlock line 62
  18. theorem OAI.HadwigerCounterexample.asBlock_inj line 63
  19. def OAI.HadwigerCounterexample.zget line 66
  20. def OAI.HadwigerCounterexample.tested line 67
  21. def OAI.HadwigerCounterexample.scan line 70
  22. def OAI.HadwigerCounterexample.Digest.feasible line 77
  23. def OAI.HadwigerCounterexample.Digest.diagO line 79
  24. def OAI.HadwigerCounterexample.Digest.sumBit line 80
  25. theorem OAI.HadwigerCounterexample.scan_feasible line 84
  26. theorem OAI.HadwigerCounterexample.scan_is line 87
  27. theorem OAI.HadwigerCounterexample.etaScan line 107
  28. theorem OAI.HadwigerCounterexample.role_scan line 113
  29. def OAI.HadwigerCounterexample.dialed line 130
  30. def OAI.HadwigerCounterexample.spins line 133
  31. theorem OAI.HadwigerCounterexample.spins_law line 135
  32. def OAI.HadwigerCounterexample.scopedBit line 139

    Source documentation

    Projection notation for conditioning on a specified (possible) diagnostic or diagonal only.

    def scopedBit (p : Shape) (n : ℕ) (l : Tag p.g) (f : Flavor p.g) (q : F) :
    Wgt (Knobs p.g n) := onW (spins p n) (fun x => dialed p l f x=q)

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Flavor, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Wgt, OAI.HadwigerCounterexample.Knobs, OAI.HadwigerCounterexample.onW, OAI.HadwigerCounterexample.spins, OAI.HadwigerCounterexample.dialed

  33. def OAI.HadwigerCounterexample.scopedScan line 141