OAI/Probability/SKGap/Localization/StartedResidualStep.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_started_new_partial line 15
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_started_source line 22
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_started_partial line 31
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_started_preserves_vanishing line 41
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.started_auxiliary_split line 48
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendStein_started_auxiliary line 58
7. theorem OAI.SKGapCutoff.Recipe.OrdinaryData.started_residual_step line 75
8. lemma OAI.SKGapCutoff.Static.halfDiff_zero_off_neighborhood line 112
9. lemma OAI.SKGapCutoff.Static.local_multiplier_energy line 117
10. lemma OAI.SKGapCutoff.Static.local_multiplier_starSquared line 164
11. lemma OAI.SKGapCutoff.Static.local_star_multiplier line 186