OAI/Probability/SKGap/Localization/QueryResidual.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Regression.map_prod_section_congr line 44
2. def OAI.SKGapCutoff.Regression.queryResidual line 59
3. def OAI.SKGapCutoff.Regression.queryAnswer line 63
4. lemma OAI.SKGapCutoff.Regression.queryComplement_apply line 67
5. lemma OAI.SKGapCutoff.Regression.measurable_queryResidual line 71
6. lemma OAI.SKGapCutoff.Regression.measurable_queryAnswer line 79
7. lemma OAI.SKGapCutoff.Regression.measurable_queryInnovation line 87
8. lemma OAI.SKGapCutoff.Regression.measurable_queryResidual_comp line 95
9. lemma OAI.SKGapCutoff.Regression.measurable_queryAnswer_comp line 106
10. lemma OAI.SKGapCutoff.Regression.measurable_queryInnovation_comp line 117
11. lemma OAI.SKGapCutoff.Regression.queryResidual_measurable line 128
12. lemma OAI.SKGapCutoff.Regression.queryAnswer_measurable line 133
13. lemma OAI.SKGapCutoff.Regression.queryInnovation_measurable line 138
14. lemma OAI.SKGapCutoff.Regression.query_joint_law line 143
15. theorem OAI.SKGapCutoff.Regression.adaptive_query_joint_law line 158
16. lemma OAI.SKGapCutoff.Regression.map_triple_exchange line 198
17. def OAI.SKGapCutoff.Regression.answerHistoryLaw line 224
18. theorem OAI.SKGapCutoff.Regression.adaptive_query_regeneration line 230