OAI/Geometry/UnitDistances/States.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarUnitDistances.NormalizedCoordinates.center_height line 12
2. theorem OAI.PlanarUnitDistances.NormalizedCoordinates.translate line 21
3. abbrev OAI.PlanarUnitDistances.StateConsistency.Shifts line 64
4. def OAI.PlanarUnitDistances.StateConsistency.shiftLaw line 65
5. instance OAI.PlanarUnitDistances.StateConsistency.(instance at line 66) line 66
6. def OAI.PlanarUnitDistances.StateConsistency.consistent line 68
7. def OAI.PlanarUnitDistances.StateConsistency.error line 76
8. lemma OAI.PlanarUnitDistances.StateConsistency.error_bounds line 79
9. lemma OAI.PlanarUnitDistances.StateConsistency.measurable_consistent line 83
10. lemma OAI.PlanarUnitDistances.StateConsistency.measurable_error line 98
11. lemma OAI.PlanarUnitDistances.StateConsistency.integrable_error line 102
12. lemma OAI.PlanarUnitDistances.StateConsistency.short_jump_z line 111
13. lemma OAI.PlanarUnitDistances.StateConsistency.short_jump_w line 118
14. lemma OAI.PlanarUnitDistances.StateConsistency.long_jump_z line 122
15. lemma OAI.PlanarUnitDistances.StateConsistency.long_jump_w line 135
16. lemma OAI.PlanarUnitDistances.StateConsistency.pointwise_short line 147
17. theorem OAI.PlanarUnitDistances.StateConsistency.expected_error_le line 159
18. lemma OAI.PlanarUnitDistances.StateConsistency.exp_abs_integrable line 184
19. lemma OAI.PlanarUnitDistances.StateConsistency.exp_abs_integral line 195
20. def OAI.PlanarUnitDistances.StateConsistency.envelope line 210
21. lemma OAI.PlanarUnitDistances.StateConsistency.envelope_eq line 213
22. lemma OAI.PlanarUnitDistances.StateConsistency.envelope_nonneg line 219
23. lemma OAI.PlanarUnitDistances.StateConsistency.envelope_integrable line 222
24. lemma OAI.PlanarUnitDistances.StateConsistency.envelope_integral line 227
25. lemma OAI.PlanarUnitDistances.StateConsistency.product_error_integrable line 239
26. theorem OAI.PlanarUnitDistances.StateConsistency.mean_integrated_error_le line 247
27. lemma OAI.PlanarUnitDistances.StateConsistency.unit_norms line 259
28. theorem OAI.PlanarUnitDistances.StateConsistency.exists_shifts line 273
29. lemma OAI.PlanarUnitDistances.StateConsistency.gridLabel_fract_eq_iff line 295
30. def OAI.PlanarUnitDistances.StateConsistency.fractionalShifts line 303
31. lemma OAI.PlanarUnitDistances.StateConsistency.error_fractionalShifts line 306
32. def OAI.PlanarUnitDistances.StateConsistency.Fractional line 311
33. theorem OAI.PlanarUnitDistances.StateConsistency.exists_fractionalShifts line 315
34. lemma OAI.PlanarUnitDistances.StateConsistency.norm_le_sqrt_two_of_same_grid line 328
35. def OAI.PlanarUnitDistances.StateConsistency.localSetoid line 344
36. def OAI.PlanarUnitDistances.StateConsistency.nonarchConsistent line 354
37. lemma OAI.PlanarUnitDistances.StateConsistency.nonarch_unit_scales line 363
38. theorem OAI.PlanarUnitDistances.StateConsistency.nonarch_consistent_off_boundary line 376
39. def OAI.PlanarUnitDistances.FiniteStates.label line 408
40. lemma OAI.PlanarUnitDistances.FiniteStates.label_eq_iff line 409
41. lemma OAI.PlanarUnitDistances.FiniteStates.measurable_label line 419
42. def OAI.PlanarUnitDistances.FiniteStates.archRel line 431
43. def OAI.PlanarUnitDistances.FiniteStates.archState line 434
44. lemma OAI.PlanarUnitDistances.FiniteStates.archRel_measurable line 437
45. lemma OAI.PlanarUnitDistances.FiniteStates.archState_measurable line 445
46. lemma OAI.PlanarUnitDistances.FiniteStates.archState_consistent_iff line 450
47. def OAI.PlanarUnitDistances.FiniteStates.finiteRel line 457
48. def OAI.PlanarUnitDistances.FiniteStates.finiteState line 461
49. lemma OAI.PlanarUnitDistances.FiniteStates.finiteRel_measurable line 465
50. lemma OAI.PlanarUnitDistances.FiniteStates.finiteState_measurable line 469
51. lemma OAI.PlanarUnitDistances.FiniteStates.finiteState_consistent line 473
52. def OAI.PlanarUnitDistances.FiniteLevels.measure line 496
53. instance OAI.PlanarUnitDistances.FiniteLevels.measure_finite line 500
54. lemma OAI.PlanarUnitDistances.FiniteLevels.integrable line 506
55. lemma OAI.PlanarUnitDistances.FiniteLevels.integral_eq line 514
56. lemma OAI.PlanarUnitDistances.FiniteLevels.measurable_pieces line 532
57. def OAI.PlanarUnitDistances.BudgetPlaces.threshold line 546
58. def OAI.PlanarUnitDistances.BudgetPlaces.alpha line 547
59. def OAI.PlanarUnitDistances.BudgetPlaces.differenceProduct line 549
60. lemma OAI.PlanarUnitDistances.BudgetPlaces.differenceProduct_ne_zero line 551
61. lemma OAI.PlanarUnitDistances.BudgetPlaces.inv_difference_abs line 555
62. theorem OAI.PlanarUnitDistances.BudgetPlaces.place_identity line 561
63. lemma OAI.PlanarUnitDistances.BudgetPlaces.alpha_nonneg_nonarch line 576
64. lemma OAI.PlanarUnitDistances.BudgetPlaces.alpha_add_log_two_nonneg line 594
65. theorem OAI.PlanarUnitDistances.BudgetPlaces.score_product_formula line 620
66. theorem OAI.PlanarUnitDistances.BudgetPlaces.arch_allowance line 637
67. def OAI.PlanarUnitDistances.PlaceLevels.finiteSupport line 654
68. lemma OAI.PlanarUnitDistances.PlaceLevels.log_off_support line 657
69. abbrev OAI.PlanarUnitDistances.PlaceLevels.Place line 668
70. instance OAI.PlanarUnitDistances.PlaceLevels.(instance at line 669) line 669
71. instance OAI.PlanarUnitDistances.PlaceLevels.(instance at line 670) line 670
72. instance OAI.PlanarUnitDistances.PlaceLevels.(instance at line 671) line 671
73. def OAI.PlanarUnitDistances.PlaceLevels.av line 673
74. def OAI.PlanarUnitDistances.PlaceLevels.radius line 677
75. lemma OAI.PlanarUnitDistances.PlaceLevels.radius_nonneg line 678
76. lemma OAI.PlanarUnitDistances.PlaceLevels.log_le_radius line 680
77. lemma OAI.PlanarUnitDistances.PlaceLevels.threshold_in_range line 683
78. lemma OAI.PlanarUnitDistances.PlaceLevels.log_in_range line 687
79. lemma OAI.PlanarUnitDistances.PlaceLevels.sum_logs line 691
80. lemma OAI.PlanarUnitDistances.PlaceLevels.sum_log_product_formula line 706