OAI/Probability/GaussianReplacement/Refinement.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentProjection.alignedExperiment_fst line 13
2. lemma OAI.CurrentProjection.alignedExperiment_independence line 23
3. lemma OAI.CurrentProjection.rowInformation_alignedExperiment line 35
4. lemma OAI.CurrentProjection.mutualInformation_pair_right_le line 68
5. lemma OAI.CurrentProjection.mutualInformation_map_right_le line 109
6. lemma OAI.CurrentProjection.exposedInformation_le_entropy line 124
7. lemma OAI.CurrentProjection.exposedInformation_dropMessage line 136
8. lemma OAI.CurrentProjection.exposedInformation_refinement_cost line 154
9. lemma OAI.CurrentProjection.critical_moment_log_bound line 206
10. lemma OAI.CurrentProjection.integrable_log_one_add_real line 261
11. lemma OAI.CurrentProjection.integral_log_one_add_real_le line 271
12. lemma OAI.CurrentProjection.refineSignal_probability line 297
13. lemma OAI.CurrentProjection.refineSignal_fst line 304
14. lemma OAI.CurrentProjection.refineSignal_snd_fst line 311
15. lemma OAI.CurrentProjection.refineSignal_snd_snd line 319
16. def OAI.CurrentProjection.refinementLoss line 327
17. lemma OAI.CurrentProjection.refinementLoss_nonneg line 331
18. lemma OAI.CurrentProjection.refinementLoss_eq line 343
19. lemma OAI.CurrentProjection.refinement_entropy_and_loss line 361
20. lemma OAI.CurrentProjection.refineSignal_snd line 401