OAI/Probability/ThorpRouting/Casimir/TypedSet.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.noIsolated_weight_le line 11
  2. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.noIsolated_probability_le line 90
  3. def OAI.ThorpNine.Casimir.Thorp.SparseContact.typedSet line 114
  4. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mem_typedSet line 119
  5. def OAI.ThorpNine.Casimir.Thorp.SparseContact.fiber line 124
  6. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mem_fiber line 129
  7. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedSet_fiber line 134
  8. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedSet_prod line 140
  9. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedSet_card line 150
  10. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.subset_typedSet line 159
  11. def OAI.ThorpNine.Casimir.Thorp.SparseContact.typedMarks line 168
  12. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedMarks_card line 172
  13. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedMarks_inclusion line 181
  14. def OAI.ThorpNine.Casimir.Thorp.SparseContact.returnRoute line 209
  15. def OAI.ThorpNine.Casimir.Thorp.SparseContact.returnGraph line 213
  16. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.returnRoute_card line 219
  17. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mem_returnRoute line 222
  18. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.returnRoute_incidence line 230
  19. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.returnGraph_degree line 251
  20. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typed_weight_sum line 272
  21. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixed_return_noIsolated line 282
  22. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mean_fresh_cylinder line 299
  23. def OAI.ThorpNine.Casimir.Thorp.SparseContact.endpointProb line 325
  24. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.endpointProb_nonneg line 331
  25. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.endpointProb_insert_isolated line 336
  26. def OAI.ThorpNine.Casimir.Thorp.SparseContact.partialKernel line 368
  27. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.partialKernel_insert_isolated line 372
  28. def OAI.ThorpNine.Casimir.Thorp.SparseContact.ContactEvent line 381
  29. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.alternating_cube_cancel line 384
  30. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.alternating_kernel_cancel line 399
  31. def OAI.ThorpNine.Casimir.Thorp.SparseContact.networkOf line 413
  32. def OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedTuple line 417
  33. def OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedReturn line 421
  34. def OAI.ThorpNine.Casimir.Thorp.SparseContact.labelsOf line 425
  35. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mem_labelsOf line 431
  36. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedTuple_eq_iff line 438
  37. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedReturn_eq_iff line 450
  38. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.endpointProb_singleton line 461
  39. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedTuple_mass line 466
  40. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedReturn_mass line 511
  41. def OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedInitial line 517
  42. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedMarks_mixedInitial line 522
  43. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.typedTuple_injective line 542
  44. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedInitial_card line 554
  45. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.contactEvent_mixedReturn_iff line 562
  46. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.probability_mixed_contact line 583
  47. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.finiteMean_pushforward line 601
  48. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedTuple_expectation line 611
  49. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.mixedReturn_expectation line 625
  50. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.partialKernel_nonneg line 639
  51. def OAI.ThorpNine.Casimir.Thorp.SparseContact.retainedKernel line 643
  52. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.retainedKernel_nonneg line 648
  53. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.retainedKernel_le line 656
  54. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.retained_square_row line 664
  55. def OAI.ThorpNine.Casimir.Thorp.SparseContact.rectOperator line 706
  56. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.rectOperator_apply line 724
  57. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.rectOperator_adjoint line 728
  58. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.rectOperator_comp_transpose line 743
  59. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.rectOperator_norm_sq_le line 756
  60. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.retained_norm_sq line 782
  61. def OAI.ThorpNine.Casimir.Thorp.SparseContact.orbitVector line 798
  62. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.orbitVector_at line 802
  63. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.orbitVector_action line 809
  64. def OAI.ThorpNine.Casimir.Thorp.SparseContact.Harmonic line 816
  65. lemma OAI.ThorpNine.Casimir.Thorp.SparseContact.normalizedCoefficient_harmonic line 820