OAI/Probability/LogConcave/Sampling/MeanMaterialVector.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.mean_material_polylog line 15
  2. theorem OAI.LogConcaveSampling.mean_path_polylog line 49
  3. def OAI.LogConcaveSampling.meanMaterialVector line 76
  4. lemma OAI.LogConcaveSampling.meanMaterialVector_norm_sq line 81
  5. lemma OAI.LogConcaveSampling.meanMaterial_slice_polySmooth line 87
  6. lemma OAI.LogConcaveSampling.meanMaterial_square_integrable line 109
  7. lemma OAI.LogConcaveSampling.meanMaterial_path_square_integrable line 121
  8. lemma OAI.LogConcaveSampling.meanMaterial_path_norm_integrable line 133
  9. lemma OAI.LogConcaveSampling.meanMaterial_path_norm_integral line 141
  10. lemma OAI.LogConcaveSampling.meanMaterial_path_chain line 151
  11. lemma OAI.LogConcaveSampling.meanMaterialVector_continuousAt line 173
  12. def OAI.LogConcaveSampling.probabilityTimeClamp line 182
  13. lemma OAI.LogConcaveSampling.probabilityTimeClamp_continuous line 184
  14. lemma OAI.LogConcaveSampling.probabilityTimeClamp_mem line 187
  15. lemma OAI.LogConcaveSampling.probabilityTimeClamp_eq line 190
  16. def OAI.LogConcaveSampling.meanPathJet line 194
  17. lemma OAI.LogConcaveSampling.meanPathJet_eq line 200
  18. lemma OAI.LogConcaveSampling.meanPathJet_time_continuous line 207
  19. lemma OAI.LogConcaveSampling.meanPathJet_space_continuous line 219
  20. lemma OAI.LogConcaveSampling.meanPathJet_measurable line 233
  21. lemma OAI.LogConcaveSampling.meanPathJet_chain line 241
  22. lemma OAI.LogConcaveSampling.inverse_sqrt_time_mono line 262
  23. theorem OAI.LogConcaveSampling.mean_path_taylor_rms line 270