OAI/Probability/FreeIsing/Brownian/FourthMoment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem367.standardGaussianFourthMoment line 12
2. theorem OAI.Problem367.standardGaussianFourthMoment_nonneg line 15
3. theorem OAI.Problem367.integrable_gaussian_norm_fourth line 18
4. theorem OAI.Problem367.gaussian_norm_fourth_eq line 23
5. theorem OAI.Problem367.preBrownian_increment_fourth_moment line 43
6. theorem OAI.Problem367.integrable_preBrownian_increment_fourth line 53
7. theorem OAI.Problem367.preBrownian_isKolmogorovProcess line 60