OAI/Probability/SKValue/GroundState/ConstantFatou.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SKValueG.constant_limit_integral_le line 14
2. theorem OAI.SKValueG.predictable_coefficients_le_groundState line 48