OAI/Probability/LogConcave/Sampling/HarmonicMeanDefect.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LogConcaveSampling.harmonic_integral_equation line 13
  2. theorem OAI.LogConcaveSampling.conditional_harmonic_integral line 44
  3. def OAI.LogConcaveSampling.harmonicMeanDefect line 95
  4. lemma OAI.LogConcaveSampling.interpolation_error_measurable line 101
  5. lemma OAI.LogConcaveSampling.harmonicMean_measurable line 112
  6. theorem OAI.LogConcaveSampling.harmonic_mean_quadrature_rms line 125
  7. lemma OAI.LogConcaveSampling.harmonicPicard_exact_defect line 172