OAI/Combinatorics/HadwigerCounterexample/LinearResponse.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HadwigerCounterexample.PureForms line 13
2. abbrev OAI.HadwigerCounterexample.ChanOut line 14
3. abbrev OAI.HadwigerCounterexample.Xpair line 15
4. def OAI.HadwigerCounterexample.pureSpace line 17
5. def OAI.HadwigerCounterexample.deltaSpace line 19
6. theorem OAI.HadwigerCounterexample.pureSpace_mem line 22
7. theorem OAI.HadwigerCounterexample.deltaSpace_mem line 25
8. def OAI.HadwigerCounterexample.chanInner line 29
9. def OAI.HadwigerCounterexample.chanDeriv line 31
10. def OAI.HadwigerCounterexample.purePair line 34
11. def OAI.HadwigerCounterexample.react line 37
12. def OAI.HadwigerCounterexample.orth line 67
13. theorem OAI.HadwigerCounterexample.solve_by_dual line 70
14. theorem OAI.HadwigerCounterexample.orth_pure line 89

    Source documentation

    Pure test annihilation vanishes in the factor quotients.

    theorem orth_pure {f b : Plan p n} {x : Xpair p n} {C : ChanOut p n} {j}
        (h : orth p C f b j x) (e : Comp p.g) :
        vanish (f (e,true)) (f (e,false)) (purePair p n x e) := by
    …

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Xpair, OAI.HadwigerCounterexample.ChanOut, OAI.HadwigerCounterexample.orth, OAI.HadwigerCounterexample.Comp, OAI.HadwigerCounterexample.vanish, OAI.HadwigerCounterexample.purePair