OAI/Probability/LogConcave/TensorGraphs/Chain.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.AdjointRemoval.onChain line 19
  2. abbrev OAI.LogConcaveSampling.AdjointRemoval.ChainSlot line 24
  3. lemma OAI.LogConcaveSampling.AdjointRemoval.onChain_iff_incident line 27
  4. def OAI.LogConcaveSampling.AdjointRemoval.chainSlotEquiv line 35
  5. def OAI.LogConcaveSampling.AdjointRemoval.closeTrace line 44
  6. abbrev OAI.LogConcaveSampling.AdjointRemoval.TraceColors line 50
  7. abbrev OAI.LogConcaveSampling.AdjointRemoval.FullColors line 53
  8. def OAI.LogConcaveSampling.AdjointRemoval.chainField line 56
  9. def OAI.LogConcaveSampling.AdjointRemoval.chainBranch line 61
  10. lemma OAI.LogConcaveSampling.AdjointRemoval.split_duplicate line 69
  11. lemma OAI.LogConcaveSampling.AdjointRemoval.split_adjoint line 74
  12. lemma OAI.LogConcaveSampling.AdjointRemoval.chainBranch_eq_split line 78
  13. lemma OAI.LogConcaveSampling.AdjointRemoval.chainBranch_polySmooth line 96
  14. theorem OAI.LogConcaveSampling.AdjointRemoval.integral_chain_expansion line 106
  15. def OAI.LogConcaveSampling.AdjointRemoval.chainPositionTensor line 136
  16. lemma OAI.LogConcaveSampling.AdjointRemoval.primaryPositionTensor_of_chain line 144
  17. theorem OAI.LogConcaveSampling.AdjointRemoval.chain_branch_bound line 155
  18. theorem OAI.LogConcaveSampling.AdjointRemoval.integral_chain_bound line 183
  19. abbrev OAI.LogConcaveSampling.CycleTrace.Primary line 232
  20. def OAI.LogConcaveSampling.CycleTrace.primaryPair line 234
  21. lemma OAI.LogConcaveSampling.CycleTrace.primaryPair_val line 237
  22. def OAI.LogConcaveSampling.CycleTrace.bundle line 241
  23. abbrev OAI.LogConcaveSampling.CycleTrace.Wire line 244
  24. abbrev OAI.LogConcaveSampling.CycleTrace.CycleWire line 245
  25. lemma OAI.LogConcaveSampling.CycleTrace.row_index_lt line 247
  26. lemma OAI.LogConcaveSampling.CycleTrace.row_index_odd line 249
  27. lemma OAI.LogConcaveSampling.CycleTrace.col_index_lt line 251
  28. lemma OAI.LogConcaveSampling.CycleTrace.row_bundle line 253
  29. lemma OAI.LogConcaveSampling.CycleTrace.col_bundle line 256
  30. def OAI.LogConcaveSampling.CycleTrace.encodeWire line 259
  31. def OAI.LogConcaveSampling.CycleTrace.decodeWire line 265
  32. lemma OAI.LogConcaveSampling.CycleTrace.decode_encode line 271
  33. lemma OAI.LogConcaveSampling.CycleTrace.encode_decode line 288
  34. def OAI.LogConcaveSampling.CycleTrace.wireEquiv line 308
  35. def OAI.LogConcaveSampling.CycleTrace.weight line 328
  36. lemma OAI.LogConcaveSampling.CycleTrace.weight_cons line 333
  37. theorem OAI.LogConcaveSampling.CycleTrace.power_entry line 341
  38. theorem OAI.LogConcaveSampling.CycleTrace.trace_power line 373
  39. def OAI.LogConcaveSampling.CycleTrace.advance line 378
  40. lemma OAI.LogConcaveSampling.CycleTrace.snoc_eq_advance line 382
  41. def OAI.LogConcaveSampling.CycleTrace.closedWeight line 391
  42. lemma OAI.LogConcaveSampling.CycleTrace.closedWeight_cons line 396
  43. theorem OAI.LogConcaveSampling.CycleTrace.trace_power_colors line 401
  44. lemma OAI.LogConcaveSampling.CycleTrace.right_row_lt line 422
  45. lemma OAI.LogConcaveSampling.CycleTrace.right_row_bundle line 423
  46. def OAI.LogConcaveSampling.CycleTrace.encodeSlot line 426
  47. def OAI.LogConcaveSampling.CycleTrace.decodeTraceSlot line 456
  48. lemma OAI.LogConcaveSampling.CycleTrace.decode_encodeSlot line 463
  49. lemma OAI.LogConcaveSampling.CycleTrace.encode_decodeSlot line 478
  50. def OAI.LogConcaveSampling.CycleTrace.slotEquiv line 520
  51. def OAI.LogConcaveSampling.CycleTrace.slotEquivAt line 527
  52. lemma OAI.LogConcaveSampling.CycleTrace.slotEquivAt_pair line 544
  53. lemma OAI.LogConcaveSampling.CycleTrace.close_encodeSlot_col line 551
  54. def OAI.LogConcaveSampling.CycleTrace.rowAt line 555
  55. lemma OAI.LogConcaveSampling.CycleTrace.close_encodeSlot_row line 558
  56. abbrev OAI.LogConcaveSampling.CycleTrace.RowColors line 603
  57. def OAI.LogConcaveSampling.CycleTrace.colorEquiv line 605
  58. def OAI.LogConcaveSampling.CycleTrace.liftField line 620
  59. lemma OAI.LogConcaveSampling.CycleTrace.chainField_lift_pair line 624
  60. def OAI.LogConcaveSampling.CycleTrace.adjointMatrix line 638
  61. lemma OAI.LogConcaveSampling.CycleTrace.product_chain_lift line 643
  62. theorem OAI.LogConcaveSampling.CycleTrace.trace_eq_chain line 654