OAI/Probability/GaussianPropeller/CapIntegral.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianPropeller.Cap.p_eq_integral_indicator line 37
2. lemma OAI.GaussianPropeller.Cap.p_le_one line 47
3. lemma OAI.GaussianPropeller.Cap.density_le_one line 52
4. abbrev OAI.GaussianPropeller.Cap.CE line 58
5. def OAI.GaussianPropeller.Cap.capP line 60
6. def OAI.GaussianPropeller.Cap.capM line 61
7. lemma OAI.GaussianPropeller.Cap.integrable_p_norm line 63
8. lemma OAI.GaussianPropeller.Cap.capP_zero line 71
9. lemma OAI.GaussianPropeller.Cap.hasDerivAt_capP line 74
10. lemma OAI.GaussianPropeller.Cap.capM_eq line 100
11. lemma OAI.GaussianPropeller.Cap.capP_deriv_two line 112
12. lemma OAI.GaussianPropeller.Cap.capP_two line 125