OAI/Combinatorics/StripMass/NorthBijection.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalStrip.Diagram.ColumnChain.read_ofFn line 16
2. lemma OAI.CriticalStrip.SewnRectangle.clips_left line 24
3. lemma OAI.CriticalStrip.SewnRectangle.clips_right line 30
4. lemma OAI.CriticalStrip.SewnRectangle.fits_ofFn line 36
5. structure OAI.CriticalStrip.CrossTopArch line 47
6. lemma OAI.CriticalStrip.CrossTopArch.ext line 55
7. def OAI.CriticalStrip.CrossTopArch.Fits line 69
8. def OAI.CriticalStrip.CrossTopArch.weight line 71
9. lemma OAI.CriticalStrip.CrossTopArch.exists_fits line 73
10. abbrev OAI.CriticalStrip.CrossTopArch.Bounded line 77
11. structure OAI.CriticalStrip.NorthHistory line 83
12. lemma OAI.CriticalStrip.NorthHistory.ext line 95
13. instance OAI.CriticalStrip.NorthHistory.(instance at line 98) line 98
14. def OAI.CriticalStrip.NorthHistory.leftState line 101
15. def OAI.CriticalStrip.NorthHistory.rightState line 103
16. lemma OAI.CriticalStrip.NorthHistory.runs_left line 106
17. lemma OAI.CriticalStrip.NorthHistory.runs_right line 110
18. lemma OAI.CriticalStrip.NorthHistory.glues line 114
19. lemma OAI.CriticalStrip.NorthHistory.shape_left_exists line 117
20. lemma OAI.CriticalStrip.NorthHistory.shape_right_exists line 124
21. def OAI.CriticalStrip.NorthHistory.ls line 131
22. def OAI.CriticalStrip.NorthHistory.rs line 133
23. lemma OAI.CriticalStrip.NorthHistory.ls_spec line 135
24. lemma OAI.CriticalStrip.NorthHistory.rs_spec line 140
25. def OAI.CriticalStrip.NorthHistory.toCross line 147
26. lemma OAI.CriticalStrip.NorthHistory.toCross_extend line 154
27. lemma OAI.CriticalStrip.NorthHistory.toCross_fits line 162
28. def OAI.CriticalStrip.NorthHistory.ofCross line 173
29. lemma OAI.CriticalStrip.NorthHistory.ofCross_toCross line 180
30. lemma OAI.CriticalStrip.NorthHistory.toCross_ofCross line 186
31. def OAI.CriticalStrip.NorthHistory.equivCross line 202
32. def OAI.CriticalStrip.NorthHistory.weight line 208
33. lemma OAI.CriticalStrip.NorthHistory.ofCross_weight line 212
34. lemma OAI.CriticalStrip.NorthHistory.toCross_weight line 216
35. lemma OAI.CriticalStrip.Diagram.augmentedReversed_nonnegative line 234
36. lemma OAI.CriticalStrip.Diagram.augmentedReversed_vacuum_block line 238
37. lemma OAI.CriticalStrip.Diagram.augmentedReversed_source_block line 248
38. theorem OAI.CriticalStrip.Diagram.reversed_vacuum_summablePowers line 256
39. theorem OAI.CriticalStrip.Diagram.reversed_source_summablePowers line 263
40. lemma OAI.CriticalStrip.Diagram.reversed_column_nonnegative line 270
41. lemma OAI.CriticalStrip.Diagram.reversed_source_nonnegative line 275
42. lemma OAI.CriticalStrip.Diagram.reversed_angleScalar_ne_zero line 280
43. lemma OAI.CriticalStrip.Diagram.reversed_L_ne_zero line 285
44. theorem OAI.CriticalStrip.Diagram.reversed_vacuum_eq_tsum line 289
45. theorem OAI.CriticalStrip.Diagram.reversed_vacuum_nonneg line 299
46. theorem OAI.CriticalStrip.Diagram.reversed_northSource_eq_tsum line 308
47. theorem OAI.CriticalStrip.Diagram.reversed_source_weighted_summable line 317
48. theorem OAI.CriticalStrip.Diagram.angleVacuum_real line 330
49. theorem OAI.CriticalStrip.Diagram.angleNorthSource_real line 360
50. lemma OAI.CriticalStrip.Diagram.physical_northSource_real line 380
51. lemma OAI.CriticalStrip.Diagram.reversed_northSource_real line 387
52. lemma OAI.CriticalStrip.Diagram.angleEvaluation_reflect line 394
53. def OAI.CriticalStrip.Diagram.realNorthSeparator line 435
54. lemma OAI.CriticalStrip.Diagram.physical_angleScalar line 439
55. lemma OAI.CriticalStrip.Diagram.reversed_angleScalar line 445
56. lemma OAI.CriticalStrip.Diagram.physical_polynomialNorthSource line 451
57. lemma OAI.CriticalStrip.Diagram.reversed_polynomialNorthSource line 459
58. lemma OAI.CriticalStrip.Diagram.polynomialNorthGluing_physical line 467
59. lemma OAI.CriticalStrip.Diagram.archCandidate_physical line 489
60. theorem OAI.CriticalStrip.Diagram.realNorthSeparator_arch line 506