CrossForms.lean`

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Cross Forms

def OAI.HadwigerCounterexample.flipZ line 13
theorem OAI.HadwigerCounterexample.flipZ_flip line 14
abbrev OAI.HadwigerCounterexample.Cross line 16
def OAI.HadwigerCounterexample.reciprocal line 17
theorem OAI.HadwigerCounterexample.reciprocal_twice line 18
def OAI.HadwigerCounterexample.actual line 21
theorem OAI.HadwigerCounterexample.reciprocal_actual line 24
def OAI.HadwigerCounterexample.rowAgree line 30
Source documentation
two abstract cross sets agree at every row coming from these frozen directions. Also apply this notion reciprocally to check columns.
```
def rowAgree (q : Plan p n) (A B : Cross p n) :=
…
```
Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Cross
def OAI.HadwigerCounterexample.tableFlag line 36
Source documentation
The flag on an orientation of A. Test all entries on the table spaces with column in the B pins. Test the other entries by the reciprocal flag. Together these are §5 admissibility (when units are in the pin leaves).
```
def tableFlag (a b : Pin p n N) (M : Cross p n) (x : UnitType p n N) :=
…
```
Mentions: OAI.HadwigerCounterexample.Pin, OAI.HadwigerCounterexample.Cross, OAI.HadwigerCounterexample.UnitType
theorem OAI.HadwigerCounterexample.ev_gram line 40
theorem OAI.HadwigerCounterexample.flag_actual line 45
def OAI.HadwigerCounterexample.channelOut line 50
def OAI.HadwigerCounterexample.tableInj line 56
Source documentation
small table injecting condition, at this role. Row directions are in a.sp and wholly in the indicated primal block; output is viewed modulo hPin at the same sign, not the sign of the tested columns.
```
def tableInj (a b : Plan p n) (M : Cross p n) :=
…
```
Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Cross
def OAI.HadwigerCounterexample.contract line 62
Source documentation
Contraction on x, computed in full table coordinates; at the small table only its restriction to C_i is initially meaningful.
```
def contract (p : Shape) {n} (M : Cross p n) (i j : Bool) :
    Profile p n →ₗ[F] F where
…
```
Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Cross, OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.F
theorem OAI.HadwigerCounterexample.contract_actual line 71
def OAI.HadwigerCounterexample.innerP line 99