OAI/Probability/LogConcave/Sampling/TransportCorrectionMajorant.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.probabilityVelocity_iterated_small line 15
  2. def OAI.LogConcaveSampling.transportCorrectionMajorant line 28
  3. lemma OAI.LogConcaveSampling.transportCorrectionMajorant_nonneg line 30
  4. theorem OAI.LogConcaveSampling.probabilityTransport_correction_split line 33
  5. def OAI.LogConcaveSampling.vectorArray line 119
  6. lemma OAI.LogConcaveSampling.vectorArray_spatial line 122
  7. lemma OAI.LogConcaveSampling.vectorArray_polySmooth line 133
  8. lemma OAI.LogConcaveSampling.vectorArray_energy line 155
  9. lemma OAI.LogConcaveSampling.probabilityTransport_lipschitz line 181
  10. lemma OAI.LogConcaveSampling.probabilityTransport_infty line 188
  11. lemma OAI.LogConcaveSampling.probabilityCorrection_polySmooth line 194
  12. lemma OAI.LogConcaveSampling.probabilityCorrection_energy line 207
  13. def OAI.LogConcaveSampling.jointCorrectionArray line 223
  14. lemma OAI.LogConcaveSampling.jointCorrectionArray_energy line 227
  15. lemma OAI.LogConcaveSampling.normalizedTensorMajorant_inv_scale line 258
  16. lemma OAI.LogConcaveSampling.inv_scale_pred line 267
  17. def OAI.LogConcaveSampling.harmonicGradientBound line 272
  18. lemma OAI.LogConcaveSampling.centeringPotential_gradient_uniform line 274
  19. lemma OAI.LogConcaveSampling.harmonicSkew_inv_scaled line 290
  20. lemma OAI.LogConcaveSampling.centeringScore_inv_scaled line 299
  21. lemma OAI.LogConcaveSampling.centeringMean_inv_scaled line 315
  22. lemma OAI.LogConcaveSampling.jointCorrection_inv_scaled line 329