OAI/Probability/LogConcave/Dynamics/Truncated.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.LinearGrowthODE.truncated line 17
  2. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_smooth line 19
  3. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_lipschitz line 22
  4. lemma OAI.LogConcaveSampling.LinearGrowthODE.cutoff_eq_one line 27
  5. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_eq line 35
  6. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_growth line 38
  7. theorem OAI.LogConcaveSampling.LinearGrowthODE.exists_curve line 44
  8. theorem OAI.LogConcaveSampling.LinearGrowthODE.unique line 65
  9. lemma OAI.LogConcaveSampling.LinearGrowthODE.growth_from_right line 99
  10. lemma OAI.LogConcaveSampling.LinearGrowthODE.gronwallBound_initial_mono line 124
  11. def OAI.LogConcaveSampling.LinearGrowthODE.flow line 131
  12. lemma OAI.LogConcaveSampling.LinearGrowthODE.flow_continuous line 134
  13. lemma OAI.LogConcaveSampling.LinearGrowthODE.flow_initial line 137
  14. lemma OAI.LogConcaveSampling.LinearGrowthODE.flow_deriv line 140
  15. lemma OAI.LogConcaveSampling.LinearGrowthODE.flow_growth line 145
  16. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_continuous line 165
  17. lemma OAI.LogConcaveSampling.LinearGrowthODE.truncated_flow_growth line 169
  18. lemma OAI.LogConcaveSampling.LinearGrowthODE.eq_truncated_flow line 181
  19. lemma OAI.LogConcaveSampling.LinearGrowthODE.flow_continuous_initial line 200
  20. lemma OAI.LogConcaveSampling.LinearGrowthODE.backwardTest_vanish line 215
  21. theorem OAI.LogConcaveSampling.GlobalODE.stationary_integral_of_backward_flux line 251
  22. lemma OAI.LogConcaveSampling.LinearGrowthODE.fderiv_zero_of_vanish_outside line 348
  23. theorem OAI.LogConcaveSampling.LinearGrowthODE.stationary_integral_compact line 355
  24. theorem OAI.LogConcaveSampling.LinearGrowthODE.stationary_law line 428