OAI/Probability/ThorpRouting/SparseSaving/Main.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typedMarks line 11
2. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typedMarks_card line 15
3. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typedMarks_inclusion line 24
4. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.returnRoute line 52
5. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.returnGraph line 56
6. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.returnRoute_card line 62
7. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mem_returnRoute line 65
8. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.returnRoute_incidence line 73
9. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.returnGraph_degree line 94
10. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typed_weight_sum line 115
11. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixed_return_noIsolated line 125
12. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mean_fresh_cylinder line 142
13. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.endpointProb line 168
14. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.endpointProb_nonneg line 174
15. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.endpointProb_insert_isolated line 179
16. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.partialKernel line 211
17. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.partialKernel_insert_isolated line 215
18. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.ContactEvent line 224
19. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.alternating_cube_cancel line 227
20. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.alternating_kernel_cancel line 242
21. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.networkOf line 256
22. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedTuple line 260
23. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedReturn line 264
24. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.labelsOf line 268
25. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mem_labelsOf line 274
26. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedTuple_eq_iff line 281
27. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedReturn_eq_iff line 293
28. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.endpointProb_singleton line 304
29. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedTuple_mass line 309
30. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedReturn_mass line 354
31. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedInitial line 360
32. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typedMarks_mixedInitial line 365
33. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.typedTuple_injective line 385
34. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedInitial_card line 397
35. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.contactEvent_mixedReturn_iff line 405
36. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.probability_mixed_contact line 426
37. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.finiteMean_pushforward line 444
38. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedTuple_expectation line 454
39. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.mixedReturn_expectation line 468
40. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.partialKernel_nonneg line 482
41. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.retainedKernel line 486
42. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.retainedKernel_nonneg line 491
43. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.retainedKernel_le line 499
44. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.retained_square_row line 507
45. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.rectOperator line 549
46. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.rectOperator_apply line 567
47. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.rectOperator_adjoint line 571
48. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.rectOperator_comp_transpose line 586
49. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.rectOperator_norm_sq_le line 599
50. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.retained_norm_sq line 625
51. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.pointStabilizer line 635
52. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.swap_mem_pointStabilizer line 641
53. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.point_symmetrizer_zero line 646
54. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.point_fixed_zero line 678
55. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.point_unitary_fixed_zero line 690
56. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.point_relabelled_fixed_zero line 704
57. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.orbitVector line 730
58. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.orbitVector_at line 734
59. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.orbitVector_action line 741
60. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.Harmonic line 748
61. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.normalizedCoefficient_harmonic line 752
62. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sum_injections line 805
63. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.zeroExtend line 817
64. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.zeroExtend_inj line 822
65. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.zeroExtend_noninj line 828
66. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sum_zeroExtend_mul line 833
67. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.norm_zeroExtend line 839
68. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.partial_proper_zero line 847
69. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.partial_full_action line 884
70. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.alternating_retained_eq line 903
71. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.alternating_harmonic_action line 913
72. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.harmonic_action_bound line 942
73. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.harmonic_action_zero_one line 980
74. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.MainStatement line 1002
75. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.exists_exact_fixed_unit line 1018
76. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweep_forward_norm line 1039
77. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweep_norm_le_one line 1047
78. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sample_sweep_bound line 1055
79. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sample_sweep_zero_one line 1080
80. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweep_norm_bound line 1101
81. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweep_zero_one line 1121
82. def OAI.ThorpNine.SparseSaving.Thorp.SparseContact.contactConstant line 1144
83. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.contactConstant_gt_one line 1146
84. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.contactConstant_gt_two line 1151
85. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.inflated_contact_bound line 1156
86. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.contact_crude_arithmetic line 1177
87. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseContact.sweep_sharp_bound line 1191
88. theorem OAI.ThorpNine.SparseSaving.Thorp.SparseContact.uniform_sparse_contact line 1223
89. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.log_contact_eventually line 1244
90. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.contact_power_saving line 1261
91. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.inverse_dyadic_power line 1279
92. lemma OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.sparse_finite_correction line 1287
93. theorem OAI.ThorpNine.SparseSaving.Thorp.SparseRegime.exponential_sparse_saving line 1303