OAI/Probability/LogConcave/Sampling/HarmonicStationaryMoment.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.growth_vector_memLp line 13
  2. lemma OAI.LogConcaveSampling.centering_lipschitz_memLp line 18
  3. lemma OAI.LogConcaveSampling.stationary_sq_integral line 32
  4. def OAI.LogConcaveSampling.harmonicStationaryMoment line 42
  5. lemma OAI.LogConcaveSampling.harmonicStationaryMoment_nonneg line 46
  6. lemma OAI.LogConcaveSampling.harmonicMean_stationary_sq line 49
  7. lemma OAI.LogConcaveSampling.harmonicFree_initial_rms line 63
  8. lemma OAI.LogConcaveSampling.meanCell_error_measurable line 147
  9. theorem OAI.LogConcaveSampling.mean_cell_quadrature_rms line 169
  10. def OAI.LogConcaveSampling.meanCellResidual line 209
  11. lemma OAI.LogConcaveSampling.meanCellResidual_measurable line 216
  12. lemma OAI.LogConcaveSampling.meanCellResidual_eq line 224
  13. theorem OAI.LogConcaveSampling.mean_cell_residual_rms line 236
  14. lemma OAI.LogConcaveSampling.affineUnit_mem line 274
  15. lemma OAI.LogConcaveSampling.meanPathJet_cutoff line 279
  16. lemma OAI.LogConcaveSampling.meanCellResidual_cutoff line 285
  17. def OAI.LogConcaveSampling.probabilityMeanDefect line 306
  18. lemma OAI.LogConcaveSampling.probabilityMeanDefect_eq line 312
  19. theorem OAI.LogConcaveSampling.probability_mean_defect_rms line 334
  20. lemma OAI.LogConcaveSampling.meanMaterialVector_zero line 376
  21. lemma OAI.LogConcaveSampling.meanPathJet_zero line 383
  22. lemma OAI.LogConcaveSampling.probabilityFlow_mean_integral line 390
  23. lemma OAI.LogConcaveSampling.probabilityPicard_exact_defect line 408