OAI/Probability/SKGap/Localization/Envelope.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.GaussianHistory.envelope line 13
2. lemma OAI.SKGap.GaussianHistory.envelope_nonneg line 17
3. lemma OAI.SKGap.GaussianHistory.var_le_envelope line 24
4. lemma OAI.SKGap.GaussianHistory.envelope_le_square line 31
5. lemma OAI.SKGap.GaussianHistory.measurable_envelope line 39
6. lemma OAI.SKGap.GaussianHistory.integrable_envelope_weight line 44
7. def OAI.SKGap.GaussianHistory.envelopeIntegral line 54
8. lemma OAI.SKGap.GaussianHistory.variance_le_envelope_zero line 57
9. lemma OAI.SKGap.GaussianHistory.integrable_envelope_section line 65
10. lemma OAI.SKGap.GaussianHistory.envelope_step_point line 81
11. theorem OAI.SKGap.GaussianHistory.envelope_step_bound line 121
12. theorem OAI.SKGap.GaussianHistory.envelope_terminal_bound line 158