OAI/Probability/SKBarriers/Scalar/VectorAverageAlgebra.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SK.Analytic.vectorStepAverage_addline 16 - theorem
OAI.SK.Analytic.vectorStepAverage_const_mulline 27 - theorem
OAI.SK.Analytic.vectorStepAverage_constline 32 - theorem
OAI.SK.Analytic.vectorStepAverage_monoline 40 - theorem
OAI.SK.Analytic.vectorIncrementAverage_addline 50 - theorem
OAI.SK.Analytic.vectorIncrementAverage_const_mulline 63 - theorem
OAI.SK.Analytic.vectorIncrementAverage_constline 72 - theorem
OAI.SK.Analytic.vectorIncrementAverage_monoline 81