OAI/Probability/LogConcave/Analysis/AffinePotential.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.affinePotential line 16
  2. lemma OAI.LogConcaveSampling.gradient_affinePotential line 19
  3. lemma OAI.LogConcaveSampling.Admissible.affinePrimitive line 36
  4. def OAI.LogConcaveSampling.OracleCompiler.Program.affineReplies line 56
  5. lemma OAI.LogConcaveSampling.OracleCompiler.Program.measurable_affineReplies line 59
  6. lemma OAI.LogConcaveSampling.OracleCompiler.Program.affineReplies_zero line 63
  7. lemma OAI.LogConcaveSampling.OracleCompiler.Program.affineReplies_update line 66
  8. def OAI.LogConcaveSampling.OracleCompiler.Program.affineOracle line 74
  9. lemma OAI.LogConcaveSampling.OracleCompiler.Program.affineOracle_history line 84
  10. lemma OAI.LogConcaveSampling.OracleCompiler.Program.affineOracle_run line 101
  11. lemma OAI.LogConcaveSampling.gaussian_inner_law line 124
  12. lemma OAI.LogConcaveSampling.gaussian_exp_inner_integrable line 132
  13. lemma OAI.LogConcaveSampling.gaussian_exp_inner_integral line 138
  14. def OAI.LogConcaveSampling.gaussianShiftRatio line 146
  15. lemma OAI.LogConcaveSampling.gaussianShiftRatio_integrable line 149
  16. lemma OAI.LogConcaveSampling.gaussianShiftRatio_integral line 155
  17. lemma OAI.LogConcaveSampling.gaussianShiftRatio_density line 164
  18. lemma OAI.LogConcaveSampling.TVAtMost_of_density line 197
  19. lemma OAI.LogConcaveSampling.density_root_L1_sq line 209
  20. lemma OAI.LogConcaveSampling.gaussian_shift_L1 line 253
  21. theorem OAI.LogConcaveSampling.TVAtMost_gaussian_shift line 287
  22. lemma OAI.LogConcaveSampling.TVAtMost.mono line 295
  23. lemma OAI.LogConcaveSampling.TVAtMost.symm line 299
  24. lemma OAI.LogConcaveSampling.TVAtMost.trans line 304
  25. theorem OAI.LogConcaveSampling.TVAtMost_gaussian_affine line 309