OAI/Probability/LogConcave/Numerics/CenteringStateQuadratureBudget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.centeringStateQuadratureBudget line 22
  2. def OAI.LogConcaveSampling.centeringMeanQuadratureBudget line 26
  3. lemma OAI.LogConcaveSampling.centeringStateQuadratureBudget_nonneg line 30
  4. lemma OAI.LogConcaveSampling.centeringMeanQuadratureBudget_nonneg line 35
  5. theorem OAI.LogConcaveSampling.centering_state_quadrature_rms line 42
  6. theorem OAI.LogConcaveSampling.centering_mean_quadrature_rms line 67
  7. theorem OAI.LogConcaveSampling.centering_initial_rms line 89
  8. def OAI.LogConcaveSampling.stationaryPicard line 127
  9. lemma OAI.LogConcaveSampling.stationaryPicard_measurable line 130
  10. theorem OAI.LogConcaveSampling.stationaryPicard_rms line 138