OAI/Combinatorics/HadwigerCounterexample/MomentCoordinates.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Moment Coordinates

  1. structure OAI.HadwigerCounterexample.Shape line 17

    Source documentation

    Construction parameters that affect dimensions (except n,N). j = selector degree; r = number of ordered tester pairs in a tester. J, h mix and channel indices.

    structure Shape where
…
  2. abbrev OAI.HadwigerCounterexample.Block line 25
  3. abbrev OAI.HadwigerCounterexample.Block.O line 28
  4. abbrev OAI.HadwigerCounterexample.Block.S line 29
  5. abbrev OAI.HadwigerCounterexample.Block.sharp line 30
  6. abbrev OAI.HadwigerCounterexample.Block.Z line 31
  7. abbrev OAI.HadwigerCounterexample.BaseIdx line 34
  8. abbrev OAI.HadwigerCounterexample.Base line 35
  9. abbrev OAI.HadwigerCounterexample.AIdx line 36
  10. abbrev OAI.HadwigerCounterexample.Label line 37
  11. abbrev OAI.HadwigerCounterexample.SelIdx line 38
  12. abbrev OAI.HadwigerCounterexample.Row line 39
  13. abbrev OAI.HadwigerCounterexample.Ray line 40
  14. abbrev OAI.HadwigerCounterexample.Moment line 41
  15. theorem OAI.HadwigerCounterexample.card_baseIdx line 43
  16. def OAI.HadwigerCounterexample.psize line 46
  17. theorem OAI.HadwigerCounterexample.card_row line 47
  18. def OAI.HadwigerCounterexample.emptySel line 51
  19. def OAI.HadwigerCounterexample.selV line 52
  20. def OAI.HadwigerCounterexample.baseV line 53
  21. def OAI.HadwigerCounterexample.putLab line 59

    Source documentation

    Embedding of the affine coordinate space at a fixed label.

    def putLab (n : ℕ) (s : Label p.b) : Vec (AIdx p.g n) →ₗ[F] Ray p n where
…

    Mentions: OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.AIdx, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.Ray

  22. def OAI.HadwigerCounterexample.point line 64
  23. def OAI.HadwigerCounterexample.mom line 65
  24. theorem OAI.HadwigerCounterexample.point_base_eval line 67
  25. theorem OAI.HadwigerCounterexample.point_ne_zero line 70
  26. def OAI.HadwigerCounterexample.Wspace line 76
  27. def OAI.HadwigerCounterexample.allows line 80

    Source documentation

    O-blocks disallowed at l are set to zero.

    def allows {g n} (l : Tag g) (z : Base g n) :=
…

    Mentions: OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Base

  28. def OAI.HadwigerCounterexample.shared line 83
  29. def OAI.HadwigerCounterexample.Wtag line 86
  30. def OAI.HadwigerCounterexample.Wstar line 89
  31. theorem OAI.HadwigerCounterexample.Wstar_le_tag line 94
  32. theorem OAI.HadwigerCounterexample.Wtag_le line 96
  33. theorem OAI.HadwigerCounterexample.Wspace_sym line 99
  34. abbrev OAI.HadwigerCounterexample.Profile line 108

    Source documentation

    Cut profiles in the direct sum over unordered components.

    abbrev Profile (p : Shape) (n : ℕ) := Comp p.g → Moment p n

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Comp, OAI.HadwigerCounterexample.Moment

  35. def OAI.HadwigerCounterexample.cut line 109
  36. def OAI.HadwigerCounterexample.Xspace line 117
  37. theorem OAI.HadwigerCounterexample.mem_X line 120
  38. def OAI.HadwigerCounterexample.getPair line 125

    Source documentation

    For complete generality this returns zero on pairs with equal tags.

    def getPair (p : Shape) (n : ℕ) (l d : Tag p.g) : Profile p n →ₗ[F] Moment p n :=
…

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

  39. theorem OAI.HadwigerCounterexample.getPair_edge line 128
  40. theorem OAI.HadwigerCounterexample.getPair_cut line 131
  41. def OAI.HadwigerCounterexample.atom line 142

    Source documentation

    Single star atoms as profiles in ambient coordinates.

    def atom (p : Shape) (l : Tag p.g) (s : Label p.b) (z : Base p.g n) : Profile p n :=
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.Base, OAI.HadwigerCounterexample.Profile

  42. theorem OAI.HadwigerCounterexample.atom_mem line 145
  43. theorem OAI.HadwigerCounterexample.atom_def line 155