OAI/Combinatorics/HadwigerCounterexample/RawFrameLaws.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.HadwigerCounterexample.rowDecidableEq line 15
2. instance OAI.HadwigerCounterexample.fullDecidableEq line 16
3. instance OAI.HadwigerCounterexample.fullFintype line 17
4. instance OAI.HadwigerCounterexample.oframeFintype line 18
5. instance OAI.HadwigerCounterexample.orientFintype line 19
6. def OAI.HadwigerCounterexample.gramCond line 21
7. theorem OAI.HadwigerCounterexample.gramCond_exists line 24
8. theorem OAI.HadwigerCounterexample.valid_iff line 27
9. def OAI.HadwigerCounterexample.raw line 35
10. theorem OAI.HadwigerCounterexample.raw_law line 38
11. theorem OAI.HadwigerCounterexample.raw_nonneg line 43
12. theorem OAI.HadwigerCounterexample.raw_carried line 46
13. abbrev OAI.HadwigerCounterexample.UnitType line 55
14. abbrev OAI.HadwigerCounterexample.Place line 56
15. abbrev OAI.HadwigerCounterexample.JointIdx line 57
16. def OAI.HadwigerCounterexample.takeSign line 59
17. def OAI.HadwigerCounterexample.images line 61
18. abbrev OAI.HadwigerCounterexample.Dir line 64
19. abbrev OAI.HadwigerCounterexample.Plan line 65
20. def OAI.HadwigerCounterexample.planRank line 66
21. structure OAI.HadwigerCounterexample.Pin line 71

    Source documentation

    Pin data: stored subspaces of directions with assigned images. We store a full linear map for convenience; only its restriction to the pin directions at each place is used. Counts charge only for the restrictions.

    structure Pin (p : Shape) (n N : ℕ) where
    …

    Mentions: OAI.HadwigerCounterexample.Shape

22. def OAI.HadwigerCounterexample.Pin.agree line 75
23. theorem OAI.HadwigerCounterexample.Pin.agree_pack line 78
24. theorem OAI.HadwigerCounterexample.bp_sum line 98
25. theorem OAI.HadwigerCounterexample.reference_cap line 107

    Source documentation

    Image cap under two independent raw orientations. Uniform over all simultaneous exact-image specifications.

    theorem reference_cap (m : Mixer p n) (a : Pin p n N) {δ : ℝ} (hd : 0 < δ)
        (hu : 2*num (Full p n) - N ≤ -1)
        (hδ : 2*num (Full p n) ≤ δ/2 * N)
        (hA : 4*num (Comp p.g) ≤ δ/2 * N) :
        pr (pairW (raw m N) (raw m N)) a.agree ≤ bp (-(1-δ)*(planRank a.sp)*N) := by
    …

    Mentions: OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.Pin, OAI.HadwigerCounterexample.num, OAI.HadwigerCounterexample.Full, OAI.HadwigerCounterexample.Comp, OAI.HadwigerCounterexample.pr, OAI.HadwigerCounterexample.pairW, OAI.HadwigerCounterexample.raw, OAI.HadwigerCounterexample.bp, OAI.HadwigerCounterexample.planRank