OAI/Probability/SKBarriers/Locking/NarrowMomentBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.narrowSusceptibility line 17
2. def OAI.SK.Analytic.narrowMixedMoment line 22
3. def OAI.SK.Analytic.narrowJointMoment line 28
4. def OAI.SK.Analytic.narrowTentSquare line 34
5. theorem OAI.SK.Analytic.narrowSusceptibility_eq line 39
6. theorem OAI.SK.Analytic.narrowSusceptibility_abs_le line 45
7. theorem OAI.SK.Analytic.narrowBaseQuadratic_ramp_le line 51