OAI/Probability/LogConcave/TensorGraphs/History.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LogConcaveSampling.Frontier.History line 25
  2. def OAI.LogConcaveSampling.Frontier.Consistent line 27
  3. def OAI.LogConcaveSampling.Frontier.historyOf line 32
  4. lemma OAI.LogConcaveSampling.Frontier.historyOf_consistent line 34
  5. lemma OAI.LogConcaveSampling.Frontier.consistent_color line 39
  6. def OAI.LogConcaveSampling.Frontier.historyEquiv line 51
  7. theorem OAI.LogConcaveSampling.Frontier.sum_consistent_histories line 62
  8. def OAI.LogConcaveSampling.Frontier.graphStep line 85
  9. lemma OAI.LogConcaveSampling.Frontier.consistent_iff_spectators line 90
  10. lemma OAI.LogConcaveSampling.Frontier.pathWeight_graphStep line 103
  11. theorem OAI.LogConcaveSampling.Frontier.coordinate_sum_eq_circuit line 127
  12. theorem OAI.LogConcaveSampling.Frontier.coordinate_contraction_bound line 150
  13. abbrev OAI.LogConcaveSampling.GraphSchedule.Edge line 171
  14. def OAI.LogConcaveSampling.GraphSchedule.length line 173
  15. lemma OAI.LogConcaveSampling.GraphSchedule.key_lt_length line 175
  16. def OAI.LogConcaveSampling.GraphSchedule.emit line 178
  17. def OAI.LogConcaveSampling.GraphSchedule.absorb line 183
  18. lemma OAI.LogConcaveSampling.GraphSchedule.emit_lt_absorb line 189
  19. lemma OAI.LogConcaveSampling.GraphSchedule.emit_le_length line 200
  20. def OAI.LogConcaveSampling.GraphSchedule.inputEdges line 207
  21. def OAI.LogConcaveSampling.GraphSchedule.outputEdges line 228
  22. def OAI.LogConcaveSampling.GraphSchedule.close line 256
  23. lemma OAI.LogConcaveSampling.GraphSchedule.input_card line 263
  24. def OAI.LogConcaveSampling.GraphSchedule.Adjacent line 274
  25. lemma OAI.LogConcaveSampling.GraphSchedule.incident_sides line 277
  26. theorem OAI.LogConcaveSampling.GraphSchedule.factor_splits_nonempty line 290
  27. abbrev OAI.LogConcaveSampling.AdjointRemoval.InternalEdge line 307
  28. def OAI.LogConcaveSampling.AdjointRemoval.edgeSource line 309
  29. def OAI.LogConcaveSampling.AdjointRemoval.edgeTarget line 313
  30. lemma OAI.LogConcaveSampling.AdjointRemoval.internal_adjacent line 318
  31. lemma OAI.LogConcaveSampling.AdjointRemoval.internal_source_ne line 325
  32. lemma OAI.LogConcaveSampling.AdjointRemoval.adjacent_has_edge line 330
  33. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_removal_schedule line 343
  34. lemma OAI.LogConcaveSampling.GraphSchedule.close_output_apply line 375
  35. lemma OAI.LogConcaveSampling.GraphSchedule.closing_iff line 382
  36. def OAI.LogConcaveSampling.GraphSchedule.duplicate line 397
  37. def OAI.LogConcaveSampling.GraphSchedule.cutColorEquiv line 402
  38. theorem OAI.LogConcaveSampling.GraphSchedule.sum_closed_coordinates line 416
  39. theorem OAI.LogConcaveSampling.GraphSchedule.scheduled_coordinate_bound line 446
  40. theorem OAI.LogConcaveSampling.GraphSchedule.reduced_coordinate_bound line 480