OAI/Probability/SKBarriers/Scalar/CovarianceRegular.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.finiteCovariance_abs_le_two line 17
  2. theorem OAI.SK.Analytic.matrix_trace_square_norm_bound line 41
  3. theorem OAI.SK.Analytic.finiteMean_continuous line 59
  4. theorem OAI.SK.Analytic.finiteCovariance_continuous line 65
  5. theorem OAI.SK.Analytic.traceSquare_continuous line 71
  6. def OAI.SK.Analytic.hierarchyTraceSquare line 81
  7. theorem OAI.SK.Analytic.hierarchyTraceSquare_regular line 86
  8. theorem OAI.SK.Analytic.hierarchyTraceSquare_integrable line 96
  9. theorem OAI.SK.Analytic.hierarchyPathLaw_moment_integral line 103