OAI/Probability/LogConcave/Dynamics/StationaryPath.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LogConcaveSampling.StationaryPath line 13
  2. lemma OAI.LogConcaveSampling.StationaryPath.measurable_slice line 27
  3. lemma OAI.LogConcaveSampling.StationaryPath.measurePreserving line 30
  4. lemma OAI.LogConcaveSampling.StationaryPath.memLp_slice line 33
  5. lemma OAI.LogConcaveSampling.StationaryPath.integral_eq line 36
  6. lemma OAI.LogConcaveSampling.centeringTrueVelocity_continuous line 46
  7. theorem OAI.LogConcaveSampling.exists_centering_stationaryPath line 67
  8. def OAI.LogConcaveSampling.centeringWeight line 76
  9. def OAI.LogConcaveSampling.centeringRowBudget line 79
  10. lemma OAI.LogConcaveSampling.centeringWeight_bound line 82
  11. lemma OAI.LogConcaveSampling.centeringFullWeight_bound line 90