OAI/Probability/LogConcave/Sampling/ClosedFieldMean.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.integral_abs_center_le_sqrt line 22
  2. lemma OAI.LogConcaveSampling.poincare_integral_norm_center line 32
  3. lemma OAI.LogConcaveSampling.norm_integral_sub_map_mean_le line 71
  4. lemma OAI.LogConcaveSampling.conditionalFieldMean_center_error line 87
  5. lemma OAI.LogConcaveSampling.conditionalFieldMean_error line 103
  6. lemma OAI.LogConcaveSampling.conditionalFieldMean_norm_bound line 130
  7. lemma OAI.LogConcaveSampling.conditionalFieldMean_endpoint_error line 145
  8. lemma OAI.LogConcaveSampling.conditionalFieldMean_tendsto_endpoint line 163
  9. def OAI.LogConcaveSampling.closedFieldMean line 188
  10. lemma OAI.LogConcaveSampling.closedFieldMean_continuous line 192
  11. def OAI.LogConcaveSampling.fullProbabilityVelocity line 220
  12. lemma OAI.LogConcaveSampling.fullProbabilityVelocity_continuous line 224
  13. lemma OAI.LogConcaveSampling.fullProbabilityVelocity_eq line 232
  14. lemma OAI.LogConcaveSampling.fullProbabilityVelocity_endpoint line 237
  15. lemma OAI.LogConcaveSampling.fullProbabilityVelocity_lipschitz line 241