OAI/Probability/GaussianInformation/Dyadic/ScoreBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.finiteInformation line 18
2. lemma OAI.RepeatedLocalization.infoContribution_le_negative_xlog_mass line 21
3. lemma OAI.RepeatedLocalization.finiteInformation_le_entropy_mass line 29
4. lemma OAI.RepeatedLocalization.scoreMass_zero_of_sq_integral_zero line 40
5. lemma OAI.RepeatedLocalization.finiteInformation_good_bound line 54
6. lemma OAI.RepeatedLocalization.binary_log_sum line 102
7. lemma OAI.RepeatedLocalization.infoContribution_add_le line 120
8. lemma OAI.RepeatedLocalization.finiteInformation_good_bad_bound line 167
9. lemma OAI.RepeatedLocalization.eLpNorm_eq_sqrt_integral_sq line 204