OAI/Probability/SKValue/GroundState/EmpiricalLog.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValueG.empiricalMean line 12
2. lemma OAI.SKValueG.empiricalMean_integrable line 15
3. lemma OAI.SKValueG.integral_empiricalMean line 20
4. lemma OAI.SKValueG.empirical_log_lower line 30
5. lemma OAI.SKValueG.empiricalMean_pos line 38
6. theorem OAI.SKValueG.expected_log_empiricalMean_tendsto line 44