OAI/Probability/ThorpRouting/Adaptive/TypedSet.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.noIsolated_probability_le line 11
2. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedSet line 35
3. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mem_typedSet line 40
4. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.fiber line 45
5. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mem_fiber line 50
6. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedSet_fiber line 55
7. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedSet_prod line 61
8. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedSet_card line 71
9. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.subset_typedSet line 80
10. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedMarks line 89
11. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedMarks_card line 93
12. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedMarks_inclusion line 102
13. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.returnRoute line 130
14. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.returnGraph line 134
15. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.returnRoute_card line 140
16. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mem_returnRoute line 143
17. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.returnRoute_incidence line 151
18. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.returnGraph_degree line 172
19. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typed_weight_sum line 193
20. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixed_return_noIsolated line 203
21. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mean_fresh_cylinder line 220
22. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.endpointProb line 246
23. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.endpointProb_nonneg line 252
24. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.endpointProb_insert_isolated line 257
25. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.partialKernel line 289
26. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.partialKernel_insert_isolated line 293
27. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.ContactEvent line 302
28. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.alternating_cube_cancel line 305
29. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.alternating_kernel_cancel line 320
30. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.networkOf line 334
31. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedTuple line 338
32. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedReturn line 342
33. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.labelsOf line 346
34. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mem_labelsOf line 352
35. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedTuple_eq_iff line 359
36. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedReturn_eq_iff line 371
37. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.endpointProb_singleton line 382
38. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedTuple_mass line 387
39. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedReturn_mass line 432
40. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedInitial line 438
41. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedMarks_mixedInitial line 443
42. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.typedTuple_injective line 463
43. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedInitial_card line 475
44. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.contactEvent_mixedReturn_iff line 483
45. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.probability_mixed_contact line 504
46. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.finiteMean_pushforward line 522
47. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedTuple_expectation line 532
48. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.mixedReturn_expectation line 546
49. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.partialKernel_nonneg line 560
50. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.retainedKernel line 564
51. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.retainedKernel_nonneg line 569
52. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.retainedKernel_le line 577
53. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.retained_square_row line 585
54. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.rectOperator line 627
55. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.rectOperator_apply line 645
56. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.rectOperator_adjoint line 649
57. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.rectOperator_comp_transpose line 664
58. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.rectOperator_norm_sq_le line 677
59. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.retained_norm_sq line 703
60. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.orbitVector line 719
61. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.orbitVector_at line 723
62. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.orbitVector_action line 730
63. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.Harmonic line 737
64. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.normalizedCoefficient_harmonic line 741
65. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sum_injections line 788
66. def OAI.ThorpNine.Adaptive.Thorp.SparseContact.zeroExtend line 800
67. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.zeroExtend_inj line 805
68. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.zeroExtend_noninj line 811
69. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.sum_zeroExtend_mul line 816
70. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.norm_zeroExtend line 822
71. lemma OAI.ThorpNine.Adaptive.Thorp.SparseContact.partial_proper_zero line 830