OAI/Probability/SKGap/Localization/TargetAttempt.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.targetAttempt line 152
2. lemma OAI.SKGapCutoff.targetAttempt_nonneg line 166
3. lemma OAI.SKGapCutoff.targetAttempt_generator line 177
4. lemma OAI.SKGapCutoff.targetAttempt_mean line 194
5. lemma OAI.SKGapCutoff.logistic_shift_bound line 201
6. lemma OAI.SKGapCutoff.tanh_outcome_shift_bound line 209
7. lemma OAI.SKGapCutoff.targetAttempt_perturbed_le line 223
8. lemma OAI.SKGapCutoff.gibbsExpectation_attempt line 243
9. lemma OAI.SKGapCutoff.expectation_pow_le line 252
10. lemma OAI.SKGapCutoff.exp_refresh_uniformization line 268
11. lemma OAI.SKGapCutoff.gibbsExpectation_exp_refresh_le line 276
12. def OAI.SKGapCutoff.preparationFlow line 306
13. lemma OAI.SKGapCutoff.preparationFlow_density_bound line 311