OAI/NumberTheory/GaussianMoat/PassingInformation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.GaussianMoat.FinLaw.cHf_dpi_subadd line 12
2. lemma OAI.GaussianMoat.FinLaw.joint_passing_entropy line 33
3. theorem OAI.GaussianMoat.FinLaw.passing_information_lower line 72
4. lemma OAI.GaussianMoat.FinLaw.conditionOn_support line 133
5. lemma OAI.GaussianMoat.FinLaw.joint_conditionOn_mix line 143
6. lemma OAI.GaussianMoat.FinLaw.mix_support line 157
7. lemma OAI.GaussianMoat.FinLaw.expected_log_card_passingList_le line 163
8. lemma OAI.GaussianMoat.FinLaw.cIf_map line 178
9. theorem OAI.GaussianMoat.FinLaw.posterior_passing_information_lower line 185