OAI/Probability/LogConcave/TensorGraphs/RankEquiv.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.Frontier.coordinate_contraction_bound_upto line 27
  2. theorem OAI.LogConcaveSampling.GraphSchedule.scheduled_coordinate_bound_upto line 51
  3. theorem OAI.LogConcaveSampling.GraphSchedule.reduced_coordinate_bound_upto line 85
  4. def OAI.LogConcaveSampling.TraceOpening.rankEquiv line 103
  5. lemma OAI.LogConcaveSampling.TraceOpening.rankEquiv_lt line 108
  6. theorem OAI.LogConcaveSampling.TraceOpening.compress_order line 113
  7. lemma OAI.LogConcaveSampling.GraphSchedule.length_equiv_val line 122
  8. def OAI.LogConcaveSampling.GraphSchedule.stageEquiv line 141
  9. lemma OAI.LogConcaveSampling.GraphSchedule.stageEquiv_val line 145
  10. lemma OAI.LogConcaveSampling.GraphSchedule.product_stages line 148
  11. lemma OAI.LogConcaveSampling.GraphSchedule.product_stage_range line 152
  12. theorem OAI.LogConcaveSampling.GraphSchedule.ranked_coordinate_bound line 165
  13. theorem OAI.LogConcaveSampling.NetworkMoments.lintegral_primary_auxiliary_le line 203
  14. theorem OAI.LogConcaveSampling.GraphSchedule.integrated_coordinate_bound line 231
  15. theorem OAI.LogConcaveSampling.AdjointRemoval.terminal_moment_budgets line 269
  16. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_ranked_schedule line 306
  17. def OAI.LogConcaveSampling.GraphSchedule.IncidentAt line 338
  18. lemma OAI.LogConcaveSampling.GraphSchedule.incidentAt_iff line 343
  19. def OAI.LogConcaveSampling.GraphSchedule.incidentSplit line 370
  20. lemma OAI.LogConcaveSampling.AdjointRemoval.destination_iff_mem line 395
  21. lemma OAI.LogConcaveSampling.AdjointRemoval.ports_nodup line 404
  22. lemma OAI.LogConcaveSampling.AdjointRemoval.derivatives_nodup line 412
  23. def OAI.LogConcaveSampling.AdjointRemoval.derivativeEdgeEquiv line 415
  24. lemma OAI.LogConcaveSampling.AdjointRemoval.derivativeEdgeEquiv_val line 420
  25. lemma OAI.LogConcaveSampling.AdjointRemoval.hessian_slots_nodup line 424
  26. def OAI.LogConcaveSampling.AdjointRemoval.hessianEdgeEquiv line 428
  27. lemma OAI.LogConcaveSampling.AdjointRemoval.hessianEdgeEquiv_val line 434
  28. def OAI.LogConcaveSampling.GraphSchedule.rankExtend line 442
  29. lemma OAI.LogConcaveSampling.GraphSchedule.rankExtend_at line 448