OAI/Probability/SKBarriers/Hierarchy/WeightedMoments.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.weightedPartition line 14
2. theorem OAI.SK.Analytic.weightedPartition_integrable line 17
3. theorem OAI.SK.Analytic.weightedPartition_mean line 22
4. theorem OAI.SK.Analytic.weightedPartition_sq line 32
5. theorem OAI.SK.Analytic.weightedPartition_sq_integrable line 45
6. theorem OAI.SK.Analytic.weightedPartition_secondMoment line 51
7. theorem OAI.SK.Analytic.abs_overlap_le_one line 81
8. def OAI.SK.Analytic.weightedOverlapMass line 96
9. theorem OAI.SK.Analytic.weightedPartition_secondMoment_le line 99