OAI/Combinatorics/HadwigerCounterexample/QuadraticTesters.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Quadratic Testers

  1. theorem OAI.HadwigerCounterexample.pair_outers line 12
  2. theorem OAI.HadwigerCounterexample.mpair_sum line 22
  3. theorem OAI.HadwigerCounterexample.mpair_add line 28
  4. theorem OAI.HadwigerCounterexample.mpair_smul line 31
  5. def OAI.HadwigerCounterexample.pick line 36
  6. def OAI.HadwigerCounterexample.readBit line 39
  7. def OAI.HadwigerCounterexample.testM line 42
  8. def OAI.HadwigerCounterexample.etab line 46
  9. def OAI.HadwigerCounterexample.test line 48
  10. theorem OAI.HadwigerCounterexample.pick_point line 51
  11. theorem OAI.HadwigerCounterexample.etab_point line 58
  12. theorem OAI.HadwigerCounterexample.etab_disabled line 64
  13. def OAI.HadwigerCounterexample.etaO line 80

    Source documentation

    all O testers.

    def etaO (n) : Moment p n →ₗ[F] F :=
…

    Mentions: OAI.HadwigerCounterexample.Moment, OAI.HadwigerCounterexample.F

  14. def OAI.HadwigerCounterexample.eta line 83
  15. def OAI.HadwigerCounterexample.roleT line 86

    Source documentation

    a_t read on full ambient profile using allowed tags with partner d.

    def roleT (n : ℕ) (t : Tag p.g) : Profile p n →ₗ[F] F :=
…

    Mentions: OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.F

  16. theorem OAI.HadwigerCounterexample.roleT_cut line 90
  17. def OAI.HadwigerCounterexample.role line 102
  18. theorem OAI.HadwigerCounterexample.role_cut line 104
  19. def OAI.HadwigerCounterexample.sharedT line 113

    Source documentation

    b_t read on the full ambient profile.

    def sharedT (n : ℕ) (t : Tag p.g) : Profile p n →ₗ[F] F :=
…

    Mentions: OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.F

  20. theorem OAI.HadwigerCounterexample.sharedT_cut line 116
  21. def OAI.HadwigerCounterexample.sharpPick line 123
  22. def OAI.HadwigerCounterexample.sharpM line 126
  23. theorem OAI.HadwigerCounterexample.sharpM_point line 131
  24. def OAI.HadwigerCounterexample.selfM line 142
  25. theorem OAI.HadwigerCounterexample.selfM_pair line 146