OAI/Probability/LogConcave/Sampling/ProbabilityNodes.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.mean_cell_taylor_rms line 16
  2. lemma OAI.LogConcaveSampling.meanPathJet_taylor_continuous line 38
  3. def OAI.LogConcaveSampling.probabilityNodes line 60
  4. lemma OAI.LogConcaveSampling.probabilityNodes_injective line 62
  5. lemma OAI.LogConcaveSampling.probabilityNodes_mem line 69
  6. theorem OAI.LogConcaveSampling.mean_cell_interpolation_rms line 77
  7. theorem OAI.LogConcaveSampling.harmonic_mean_interpolation_rms line 132
  8. def OAI.LogConcaveSampling.finiteCoordinateProjection line 201
  9. lemma OAI.LogConcaveSampling.finiteCoordinateProjection_norm_le line 206
  10. def OAI.LogConcaveSampling.meanOutputEmbedding line 217
  11. def OAI.LogConcaveSampling.meanOutputProjection line 220
  12. lemma OAI.LogConcaveSampling.meanOutputProjection_mean line 223
  13. lemma OAI.LogConcaveSampling.projection_interpolation line 233
  14. theorem OAI.LogConcaveSampling.harmonic_point_interpolation_rms line 239
  15. abbrev OAI.LogConcaveSampling.ProbabilityNode line 294
  16. def OAI.LogConcaveSampling.probabilityCellLength line 296
  17. def OAI.LogConcaveSampling.probabilityNodeTime line 299
  18. def OAI.LogConcaveSampling.probabilityWeight line 302
  19. lemma OAI.LogConcaveSampling.probabilityCellLength_pos line 305
  20. lemma OAI.LogConcaveSampling.probabilityCellLength_sum line 309
  21. lemma OAI.LogConcaveSampling.probabilityNodeTime_mem line 316
  22. lemma OAI.LogConcaveSampling.probabilityWeight_budget line 330
  23. lemma OAI.LogConcaveSampling.probabilityNode_card line 341
  24. def OAI.LogConcaveSampling.probabilityMeanVelocity line 357
  25. def OAI.LogConcaveSampling.probabilityMeanLipschitz line 360
  26. lemma OAI.LogConcaveSampling.probabilityMeanVelocity_lipschitz line 363
  27. def OAI.LogConcaveSampling.probabilityPicard line 379
  28. lemma OAI.LogConcaveSampling.probabilityConstantPath_lipschitz line 385
  29. theorem OAI.LogConcaveSampling.probabilityPicard_lipschitz line 393
  30. def OAI.LogConcaveSampling.probabilityMeanCalls line 423
  31. lemma OAI.LogConcaveSampling.probabilityMeanCalls_succ line 425
  32. def OAI.LogConcaveSampling.harmonicWeight line 444
  33. lemma OAI.LogConcaveSampling.harmonicWeight_budget line 448
  34. def OAI.LogConcaveSampling.harmonicFree line 480
  35. lemma OAI.LogConcaveSampling.harmonicFree_lipschitz line 483
  36. def OAI.LogConcaveSampling.harmonicMeanVelocity line 500
  37. lemma OAI.LogConcaveSampling.harmonicMeanVelocity_lipschitz line 503
  38. def OAI.LogConcaveSampling.harmonicPicard line 512
  39. theorem OAI.LogConcaveSampling.harmonicPicard_lipschitz line 516
  40. def OAI.LogConcaveSampling.harmonicMeanCalls line 536
  41. lemma OAI.LogConcaveSampling.harmonicMeanCalls_succ line 538
  42. lemma OAI.LogConcaveSampling.harmonicWeight_sum_integral line 558
  43. theorem OAI.LogConcaveSampling.harmonic_quadrature_error_rms line 573