OAI/Probability/LogConcave/Sampling/AdjointCoordinateContinuous.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.adjointCoordinate_continuous line 23
  2. lemma OAI.LogConcaveSampling.adjointCoordinate_growth line 29
  3. lemma OAI.LogConcaveSampling.integrable_adjointCoordinate_mul line 39
  4. theorem OAI.LogConcaveSampling.tensorAdjoint_energy_identity line 47
  5. lemma OAI.LogConcaveSampling.matrix_cross_le_squares line 97
  6. lemma OAI.LogConcaveSampling.directional_hessian line 107
  7. lemma OAI.LogConcaveSampling.hessian_quadratic_le line 123
  8. lemma OAI.LogConcaveSampling.integrable_directional_square_sum line 158
  9. lemma OAI.LogConcaveSampling.integrable_square_sum line 170
  10. theorem OAI.LogConcaveSampling.tensorAdjoint_energy_le line 179
  11. theorem OAI.LogConcaveSampling.tensorAdjoint_frobenius_squared line 222
  12. theorem OAI.LogConcaveSampling.tensorAdjoint_frobenius_l2 line 235
  13. lemma OAI.LogConcaveSampling.directional_prod line 264
  14. lemma OAI.LogConcaveSampling.PolyC1.const line 274
  15. lemma OAI.LogConcaveSampling.PolyC1.prod line 282
  16. theorem OAI.LogConcaveSampling.adjointCoordinate_product_pairing line 292
  17. theorem OAI.LogConcaveSampling.tensorAdjoint_product_pairing line 316
  18. lemma OAI.LogConcaveSampling.jet_directional line 335
  19. lemma OAI.LogConcaveSampling.jet_neg line 346
  20. theorem OAI.LogConcaveSampling.jet_adjointCoordinate line 351
  21. theorem OAI.LogConcaveSampling.jet_tensorAdjoint line 373
  22. lemma OAI.LogConcaveSampling.commutator_term_count line 391