OAI/Probability/ThorpRouting/Tail/TypedMarks.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ThorpNine.Tail.Thorp.SparseContact.typedMarks line 11
  2. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.typedMarks_card line 15
  3. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.typedMarks_inclusion line 24
  4. def OAI.ThorpNine.Tail.Thorp.SparseContact.returnRoute line 52
  5. def OAI.ThorpNine.Tail.Thorp.SparseContact.returnGraph line 56
  6. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.returnRoute_card line 62
  7. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mem_returnRoute line 65
  8. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.returnRoute_incidence line 73
  9. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.returnGraph_degree line 94
  10. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.typed_weight_sum line 115
  11. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixed_return_noIsolated line 125
  12. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mean_fresh_cylinder line 142
  13. def OAI.ThorpNine.Tail.Thorp.SparseContact.endpointProb line 168
  14. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.endpointProb_nonneg line 174
  15. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.endpointProb_insert_isolated line 179
  16. def OAI.ThorpNine.Tail.Thorp.SparseContact.partialKernel line 211
  17. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.partialKernel_insert_isolated line 215
  18. def OAI.ThorpNine.Tail.Thorp.SparseContact.ContactEvent line 224
  19. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.alternating_cube_cancel line 227
  20. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.alternating_kernel_cancel line 242
  21. def OAI.ThorpNine.Tail.Thorp.SparseContact.networkOf line 256
  22. def OAI.ThorpNine.Tail.Thorp.SparseContact.mixedTuple line 260
  23. def OAI.ThorpNine.Tail.Thorp.SparseContact.mixedReturn line 264
  24. def OAI.ThorpNine.Tail.Thorp.SparseContact.labelsOf line 268
  25. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mem_labelsOf line 274
  26. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedTuple_eq_iff line 281
  27. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedReturn_eq_iff line 293
  28. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.endpointProb_singleton line 304
  29. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedTuple_mass line 309
  30. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedReturn_mass line 354
  31. def OAI.ThorpNine.Tail.Thorp.SparseContact.mixedInitial line 360
  32. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.typedMarks_mixedInitial line 365
  33. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.typedTuple_injective line 385
  34. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedInitial_card line 397
  35. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.contactEvent_mixedReturn_iff line 405
  36. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.probability_mixed_contact line 426
  37. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.finiteMean_pushforward line 444
  38. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedTuple_expectation line 454
  39. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.mixedReturn_expectation line 468
  40. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.partialKernel_nonneg line 482
  41. def OAI.ThorpNine.Tail.Thorp.SparseContact.retainedKernel line 486
  42. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.retainedKernel_nonneg line 491
  43. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.retainedKernel_le line 499
  44. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.retained_square_row line 507
  45. def OAI.ThorpNine.Tail.Thorp.SparseContact.rectOperator line 549
  46. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.rectOperator_apply line 567
  47. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.rectOperator_adjoint line 571
  48. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.rectOperator_comp_transpose line 586
  49. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.rectOperator_norm_sq_le line 599
  50. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.retained_norm_sq line 625
  51. def OAI.ThorpNine.Tail.Thorp.SparseContact.pointStabilizer line 635
  52. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.swap_mem_pointStabilizer line 641
  53. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.point_symmetrizer_zero line 646
  54. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.point_fixed_zero line 678
  55. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.point_unitary_fixed_zero line 690
  56. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.point_relabelled_fixed_zero line 704
  57. def OAI.ThorpNine.Tail.Thorp.SparseContact.orbitVector line 730
  58. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.orbitVector_at line 734
  59. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.orbitVector_action line 741
  60. def OAI.ThorpNine.Tail.Thorp.SparseContact.Harmonic line 748
  61. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.normalizedCoefficient_harmonic line 752
  62. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.sum_injections line 799
  63. def OAI.ThorpNine.Tail.Thorp.SparseContact.zeroExtend line 811
  64. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.zeroExtend_inj line 816
  65. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.zeroExtend_noninj line 822
  66. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.sum_zeroExtend_mul line 827
  67. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.norm_zeroExtend line 833
  68. lemma OAI.ThorpNine.Tail.Thorp.SparseContact.partial_proper_zero line 841