OAI/Probability/SKBarriers/Scalar/PrefixAlgebra.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.hierarchyTerminalGibbs_eq_affineGibbs line 22
  2. theorem OAI.SK.Analytic.hierarchyGaussian_terminal_marginal line 30
  3. theorem OAI.SK.Analytic.hierarchyMomentLevel_tower line 65
  4. theorem OAI.SK.Analytic.hierarchyPathLaw_integrable line 86
  5. theorem OAI.SK.Analytic.hierarchyPathLaw_moment_orthogonality line 98
  6. theorem OAI.SK.Analytic.hierarchyPathLaw_moment_square_mono line 141
  7. theorem OAI.SK.Analytic.hierarchyMomentLevel_retained line 158
  8. theorem OAI.SK.Analytic.hierarchyMomentLevel_family line 177
  9. theorem OAI.SK.Analytic.hierarchyPathLaw_fixed_mul line 199
  10. def OAI.SK.Analytic.hierarchySpinMean line 211
  11. theorem OAI.SK.Analytic.hierarchySpinMean_regular line 215
  12. theorem OAI.SK.Analytic.hierarchyLevel_spinMean line 222