OAI/Probability/LogConcave/TensorGraphs/Vertex.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LogConcaveSampling.TraceOpening.Vertex line 20
  2. def OAI.LogConcaveSampling.TraceOpening.level line 22
  3. lemma OAI.LogConcaveSampling.TraceOpening.auxiliary_between line 26
  4. def OAI.LogConcaveSampling.TraceOpening.Allowed line 35
  5. lemma OAI.LogConcaveSampling.TraceOpening.edge_levels_distinct line 41
  6. theorem OAI.LogConcaveSampling.TraceOpening.all_vertex_splits_nontrivial line 57
  7. def OAI.LogConcaveSampling.TraceOpening.orderKey line 100
  8. lemma OAI.LogConcaveSampling.TraceOpening.orderKey_strict line 103
  9. lemma OAI.LogConcaveSampling.TraceOpening.orderKey_div line 110
  10. lemma OAI.LogConcaveSampling.TraceOpening.orderKey_injective line 117
  11. theorem OAI.LogConcaveSampling.TraceOpening.ordered_nontrivial_splits line 127
  12. def OAI.LogConcaveSampling.traceMomentOrder line 152
  13. lemma OAI.LogConcaveSampling.traceMomentOrder_bounds line 155
  14. lemma OAI.LogConcaveSampling.traceMomentOrder_polynomial line 178
  15. lemma OAI.LogConcaveSampling.traceMomentOrder_dimension_root line 188
  16. lemma OAI.LogConcaveSampling.TraceMoment.psd_norm_le_trace line 213
  17. lemma OAI.LogConcaveSampling.TraceMoment.hermitian_norm_eigenvalues line 225
  18. lemma OAI.LogConcaveSampling.TraceMoment.hermitian_trace_pow line 235
  19. lemma OAI.LogConcaveSampling.TraceMoment.psd_norm_pow_le_trace_pow line 249
  20. theorem OAI.LogConcaveSampling.TraceMoment.rectangular_trace_moment line 265
  21. structure OAI.LogConcaveSampling.AdjointRemoval.Hessian line 279
  22. def OAI.LogConcaveSampling.AdjointRemoval.Hessian.degree line 285
  23. def OAI.LogConcaveSampling.AdjointRemoval.Hessian.hit line 287
  24. structure OAI.LogConcaveSampling.AdjointRemoval.State line 290
  25. def OAI.LogConcaveSampling.AdjointRemoval.State.degree line 295
  26. def OAI.LogConcaveSampling.AdjointRemoval.initial line 298
  27. lemma OAI.LogConcaveSampling.AdjointRemoval.initial_degree line 300
  28. def OAI.LogConcaveSampling.AdjointRemoval.hitPrimary line 303
  29. def OAI.LogConcaveSampling.AdjointRemoval.pair line 306
  30. def OAI.LogConcaveSampling.AdjointRemoval.hitHessian line 309
  31. lemma OAI.LogConcaveSampling.AdjointRemoval.hitPrimary_degree line 312
  32. lemma OAI.LogConcaveSampling.AdjointRemoval.pair_degree line 329
  33. lemma OAI.LogConcaveSampling.AdjointRemoval.hitHessian_degree line 338
  34. inductive OAI.LogConcaveSampling.AdjointRemoval.Step line 349
  35. lemma OAI.LogConcaveSampling.AdjointRemoval.Step.degree_eq line 355
  36. lemma OAI.LogConcaveSampling.AdjointRemoval.Step.pending_lt line 362
  37. theorem OAI.LogConcaveSampling.AdjointRemoval.reachable_degree line 369
  38. def OAI.LogConcaveSampling.AdjointRemoval.State.good line 375
  39. lemma OAI.LogConcaveSampling.AdjointRemoval.initial_good line 378
  40. lemma OAI.LogConcaveSampling.AdjointRemoval.Step.good line 381
  41. theorem OAI.LogConcaveSampling.AdjointRemoval.reachable_good line 411
  42. lemma OAI.LogConcaveSampling.AdjointRemoval.degree_identity line 416
  43. theorem OAI.LogConcaveSampling.AdjointRemoval.terminal_degree_count line 429
  44. def OAI.LogConcaveSampling.AdjointRemoval.branches line 436
  45. lemma OAI.LogConcaveSampling.AdjointRemoval.branches_step line 441
  46. lemma OAI.LogConcaveSampling.AdjointRemoval.hessian_degree_lower line 452
  47. lemma OAI.LogConcaveSampling.AdjointRemoval.branches_length line 460
  48. def OAI.LogConcaveSampling.AdjointRemoval.expand line 470
  49. lemma OAI.LogConcaveSampling.AdjointRemoval.mem_expand_reachable line 476
  50. lemma OAI.LogConcaveSampling.AdjointRemoval.mem_expand_terminal line 492
  51. lemma OAI.LogConcaveSampling.AdjointRemoval.list_sum_constant line 510
  52. lemma OAI.LogConcaveSampling.AdjointRemoval.expand_length line 516
  53. theorem OAI.LogConcaveSampling.AdjointRemoval.full_expansion_bookkeeping line 541
  54. def OAI.LogConcaveSampling.TraceWords.paths line 560
  55. def OAI.LogConcaveSampling.TraceWords.eval line 566
  56. def OAI.LogConcaveSampling.TraceWords.closed line 569
  57. lemma OAI.LogConcaveSampling.TraceWords.sum_flatMap line 572
  58. lemma OAI.LogConcaveSampling.TraceWords.sum_univ_list line 578
  59. lemma OAI.LogConcaveSampling.TraceWords.eval_cons line 582
  60. lemma OAI.LogConcaveSampling.TraceWords.paths_length line 586
  61. lemma OAI.LogConcaveSampling.TraceWords.closed_length line 603
  62. theorem OAI.LogConcaveSampling.TraceWords.power_entry line 610
  63. theorem OAI.LogConcaveSampling.TraceWords.trace_power line 636
  64. lemma OAI.LogConcaveSampling.TraceWords.eval_eq_prod_get line 641
  65. theorem OAI.LogConcaveSampling.NetworkMoments.lintegral_prod_le line 657
  66. theorem OAI.LogConcaveSampling.NetworkMoments.lintegral_prod_norm_le line 682