OAI/Probability/LogConcave/TensorGraphs/AdjointMatrix.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.AdjointRemoval.regular_of_polySmooth line 23
  2. theorem OAI.LogConcaveSampling.TraceWords.integral_word_expansion line 44
  3. def OAI.LogConcaveSampling.TraceWords.adjointMatrix line 65
  4. theorem OAI.LogConcaveSampling.TraceWords.integral_trace_expansion line 71
  5. def OAI.LogConcaveSampling.AdjointRemoval.Hessian.tokens line 116
  6. def OAI.LogConcaveSampling.AdjointRemoval.State.tokens line 119
  7. lemma OAI.LogConcaveSampling.AdjointRemoval.initial_tokens line 123
  8. lemma OAI.LogConcaveSampling.AdjointRemoval.hitPrimary_tokens line 126
  9. lemma OAI.LogConcaveSampling.AdjointRemoval.pair_tokens line 144
  10. lemma OAI.LogConcaveSampling.AdjointRemoval.hitHessian_tokens line 154
  11. lemma OAI.LogConcaveSampling.AdjointRemoval.Step.tokens line 166
  12. theorem OAI.LogConcaveSampling.AdjointRemoval.mem_expand_tokens line 172
  13. theorem OAI.LogConcaveSampling.AdjointRemoval.terminal_ports line 182
  14. abbrev OAI.LogConcaveSampling.AdjointRemoval.TargetVertex line 191
  15. def OAI.LogConcaveSampling.AdjointRemoval.ports line 193
  16. lemma OAI.LogConcaveSampling.AdjointRemoval.sum_ports line 197
  17. abbrev OAI.LogConcaveSampling.AdjointRemoval.Port line 204
  18. def OAI.LogConcaveSampling.AdjointRemoval.portLabel line 206
  19. theorem OAI.LogConcaveSampling.AdjointRemoval.portLabel_bijective line 208
  20. def OAI.LogConcaveSampling.AdjointRemoval.portEquiv line 221
  21. def OAI.LogConcaveSampling.AdjointRemoval.destination line 224
  22. lemma OAI.LogConcaveSampling.AdjointRemoval.destination_label line 227
  23. lemma OAI.LogConcaveSampling.AdjointRemoval.label_mem_destination line 231
  24. lemma OAI.LogConcaveSampling.AdjointRemoval.destination_primary_ne line 238
  25. theorem OAI.LogConcaveSampling.AdjointRemoval.hessian_distinguished_neighbors line 244
  26. def OAI.LogConcaveSampling.AdjointRemoval.Adjacent line 261
  27. lemma OAI.LogConcaveSampling.AdjointRemoval.adjacent_ne line 268
  28. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_removal_graph_order line 283