OAI/Geometry/UnitDistances/Sequence.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PlanarUnitDistances.IncidenceSequence.Plane line 9
2. def OAI.PlanarUnitDistances.IncidenceSequence.information line 11
3. lemma OAI.PlanarUnitDistances.IncidenceSequence.information_bound line 16
4. structure OAI.PlanarUnitDistances.IncidenceSequence.Good line 28
5. theorem OAI.PlanarUnitDistances.IncidenceSequence.fixed_accuracy line 46
6. lemma OAI.PlanarUnitDistances.IncidenceSequence.Good.point_degree_pos line 127
7. lemma OAI.PlanarUnitDistances.IncidenceSequence.Good.center_degree_pos line 133
8. lemma OAI.PlanarUnitDistances.IncidenceSequence.Good.information_nonneg line 139
9. structure OAI.PlanarUnitDistances.IncidenceSequence.Sequence line 154
10. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.tendsto line 162
11. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.accuracy_limit line 166
12. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.error_limit line 169
13. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.information_limit line 173
14. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.cardP_power line 179
15. lemma OAI.PlanarUnitDistances.IncidenceSequence.Sequence.wedge_power line 185
16. theorem OAI.PlanarUnitDistances.IncidenceSequence.diagonal_sequence line 192
17. theorem OAI.PlanarUnitDistances.CommonField.exists_normal_field line 215
18. lemma OAI.PlanarUnitDistances.CommonField.integral_I line 230
19. lemma OAI.PlanarUnitDistances.CommonField.algebraic_ofReal line 235
20. lemma OAI.PlanarUnitDistances.CommonField.algebraic_coordinates line 238
21. abbrev OAI.PlanarUnitDistances.CommonFieldModel.Plane line 250
22. def OAI.PlanarUnitDistances.CommonFieldModel.location line 252
23. structure OAI.PlanarUnitDistances.CommonFieldModel.Model line 254
24. instance OAI.PlanarUnitDistances.CommonFieldModel.(instance at line 264) line 264
25. instance OAI.PlanarUnitDistances.CommonFieldModel.(instance at line 265) line 265
26. instance OAI.PlanarUnitDistances.CommonFieldModel.(instance at line 266) line 266
27. instance OAI.PlanarUnitDistances.CommonFieldModel.(instance at line 267) line 267
28. theorem OAI.PlanarUnitDistances.CommonFieldModel.exists_model line 269
29. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.point_injective line 300
30. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.center_injective line 306
31. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.unit_identity line 312
32. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.wpoint_injective line 320
33. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.wcenter_injective line 327
34. def OAI.PlanarUnitDistances.CommonFieldModel.Model.support line 335
35. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.sub_mem line 341
36. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.wsub_mem line 344
37. lemma OAI.PlanarUnitDistances.CommonFieldModel.Model.difference_mem line 347
38. def OAI.PlanarUnitDistances.ExpansionConsequences.mass line 357
39. def OAI.PlanarUnitDistances.ExpansionConsequences.rect line 358
40. def OAI.PlanarUnitDistances.ExpansionConsequences.left line 364
41. def OAI.PlanarUnitDistances.ExpansionConsequences.right line 365
42. def OAI.PlanarUnitDistances.ExpansionConsequences.conditional line 366
43. lemma OAI.PlanarUnitDistances.ExpansionConsequences.left_nonneg line 370
44. lemma OAI.PlanarUnitDistances.ExpansionConsequences.right_nonneg line 373
45. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mass_nonneg line 375
46. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mass_le_one line 377
47. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mass_mono line 382
48. lemma OAI.PlanarUnitDistances.ExpansionConsequences.right_sum line 385
49. lemma OAI.PlanarUnitDistances.ExpansionConsequences.rectangle_right line 390
50. lemma OAI.PlanarUnitDistances.ExpansionConsequences.conditional_nonneg line 394
51. lemma OAI.PlanarUnitDistances.ExpansionConsequences.conditional_le_one line 398
52. lemma OAI.PlanarUnitDistances.ExpansionConsequences.right_mul_conditional line 404
53. lemma OAI.PlanarUnitDistances.ExpansionConsequences.conditional_mean line 413
54. lemma OAI.PlanarUnitDistances.ExpansionConsequences.rectangle_conditional line 419
55. lemma OAI.PlanarUnitDistances.ExpansionConsequences.threshold_markov line 424
56. def OAI.PlanarUnitDistances.ExpansionConsequences.wedgeMass line 439
57. lemma OAI.PlanarUnitDistances.ExpansionConsequences.wedge_split line 442
58. theorem OAI.PlanarUnitDistances.ExpansionConsequences.wedge_rare line 462
59. theorem OAI.PlanarUnitDistances.ExpansionConsequences.one_small_set line 492
60. theorem OAI.PlanarUnitDistances.ExpansionConsequences.height_tail_mass line 502
61. def OAI.PlanarUnitDistances.ExpansionConsequences.mismatch line 517
62. def OAI.PlanarUnitDistances.ExpansionConsequences.outside line 520
63. lemma OAI.PlanarUnitDistances.ExpansionConsequences.outside_mass line 522
64. lemma OAI.PlanarUnitDistances.ExpansionConsequences.matched_add_mismatch line 529
65. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mass_left_indicator line 542
66. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mass_right_indicator line 545
67. lemma OAI.PlanarUnitDistances.ExpansionConsequences.rect_outside_indicator line 549
68. lemma OAI.PlanarUnitDistances.ExpansionConsequences.exactly_one_le_mismatch line 559
69. lemma OAI.PlanarUnitDistances.ExpansionConsequences.diagonal_expansion line 573
70. theorem OAI.PlanarUnitDistances.ExpansionConsequences.matching_dominant line 594
71. lemma OAI.PlanarUnitDistances.ExpansionConsequences.independent_mismatch_le line 663
72. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mismatch_nonneg line 684
73. lemma OAI.PlanarUnitDistances.ExpansionConsequences.mismatch_le_one line 688
74. theorem OAI.PlanarUnitDistances.ExpansionConsequences.matching_parameters line 695
75. theorem OAI.PlanarUnitDistances.ExpansionConsequences.uniform_label_matching line 724
76. lemma OAI.PlanarUnitDistances.LawExpansion.push_event line 791
77. lemma OAI.PlanarUnitDistances.LawExpansion.mass_event line 794
78. lemma OAI.PlanarUnitDistances.LawExpansion.rect_event line 799
79. lemma OAI.PlanarUnitDistances.LawExpansion.left_val line 813
80. lemma OAI.PlanarUnitDistances.LawExpansion.right_val line 818
81. lemma OAI.PlanarUnitDistances.LawExpansion.total line 821
82. lemma OAI.PlanarUnitDistances.LawExpansion.mismatch_event line 824
83. lemma OAI.PlanarUnitDistances.LawExpansion.outside_event line 828
84. lemma OAI.PlanarUnitDistances.LawExpansion.fiber_domination line 833
85. lemma OAI.PlanarUnitDistances.LawExpansion.pushed_left line 840
86. lemma OAI.PlanarUnitDistances.LawExpansion.pushed_right line 845
87. theorem OAI.PlanarUnitDistances.LawExpansion.matching line 851
88. lemma OAI.PlanarUnitDistances.LabelFromMatching.pair_mismatch line 903
89. lemma OAI.PlanarUnitDistances.LabelFromMatching.control line 912