OAI/Probability/LogConcave/Sampling/IterTensorLie.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.tensorLie_scaled_energy line 15
  2. def OAI.LogConcaveSampling.iterTensorLie line 40
  3. def OAI.LogConcaveSampling.iterEnergyBudget line 46
  4. lemma OAI.LogConcaveSampling.iterEnergyBudget_nonneg line 50
  5. lemma OAI.LogConcaveSampling.iterTensorLie_polySmooth line 56
  6. theorem OAI.LogConcaveSampling.iterTensorLie_energy line 64
  7. def OAI.LogConcaveSampling.skewLieField line 102
  8. lemma OAI.LogConcaveSampling.lieInside_apply line 107
  9. lemma OAI.LogConcaveSampling.adjointCoordinate_sum line 113
  10. lemma OAI.LogConcaveSampling.adjointCoordinate_mul line 121
  11. lemma OAI.LogConcaveSampling.tensorLie_eq_directional line 130
  12. lemma OAI.LogConcaveSampling.spatialSquared_zero line 188
  13. lemma OAI.LogConcaveSampling.spatialEnergy_from_split line 197
  14. theorem OAI.LogConcaveSampling.iteratedDerivWithin_lie line 208
  15. theorem OAI.LogConcaveSampling.stationary_lie_energy line 232
  16. theorem OAI.LogConcaveSampling.stationary_time_derivative_squared line 256