OAI/Probability/SKGap/Brownian/WorstContinuousPolynomialUpper.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.worstContinuous_polynomial_upper line 150
2. lemma OAI.SKGapCutoff.field_mean_from_linear_envelope line 223
3. lemma OAI.SKGapCutoff.field_mgf_from_linear_envelope line 260
4. theorem OAI.SKGapCutoff.continuous_upper_from_typical_gradient line 288