OAI/Probability/LogConcave/Sampling/TensorGrad.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.spatialSquared_coordinateLift line 15
  2. lemma OAI.LogConcaveSampling.arrayCoordinateLift_polySmooth line 23
  3. lemma OAI.LogConcaveSampling.spatialSquared_reindex line 51
  4. lemma OAI.LogConcaveSampling.spatialEnergy_reindex line 64
  5. def OAI.LogConcaveSampling.tensorGrad line 73
  6. lemma OAI.LogConcaveSampling.tensorGrad_polySmooth line 77
  7. def OAI.LogConcaveSampling.gradSpatialSlots line 81
  8. lemma OAI.LogConcaveSampling.spatialTensor_grad line 87
  9. lemma OAI.LogConcaveSampling.spatialSquared_grad line 95
  10. lemma OAI.LogConcaveSampling.spatialEnergy_grad line 111
  11. def OAI.LogConcaveSampling.lieInside line 133
  12. def OAI.LogConcaveSampling.tensorLie line 137
  13. lemma OAI.LogConcaveSampling.lieInside_polySmooth line 142
  14. lemma OAI.LogConcaveSampling.tensorLie_polySmooth line 147
  15. def OAI.LogConcaveSampling.productEnergyBudget line 152
  16. def OAI.LogConcaveSampling.adjointEnergyBudget line 155
  17. lemma OAI.LogConcaveSampling.productEnergyBudget_nonneg line 159
  18. lemma OAI.LogConcaveSampling.productEnergyBudget_mono line 163
  19. lemma OAI.LogConcaveSampling.adjointEnergyBudget_mono line 170
  20. lemma OAI.LogConcaveSampling.lieInside_energy line 178
  21. lemma OAI.LogConcaveSampling.tensorLie_energy line 193