OAI/Probability/LogConcave/TensorGraphs/IncidentMatrix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.GraphSchedule.incidentMatrix line 27
2. lemma OAI.LogConcaveSampling.GraphSchedule.incidentMatrix_global line 35
3. lemma OAI.LogConcaveSampling.GraphSchedule.incidentMatrix_bound line 47
4. theorem OAI.LogConcaveSampling.GraphSchedule.tensor_graph_bound line 64
5. theorem OAI.LogConcaveSampling.GraphSchedule.tensor_graph_integral_bound line 110
6. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_tensor_contraction_bound line 156
7. theorem OAI.LogConcaveSampling.AdjointRemoval.actual_tensor_integral_bound line 170