OAI/Probability/SKGap/Localization/UniformResidual.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKGapCutoff.Recipe.uniform_residual_rule line 17
  2. def OAI.SKGapCutoff.Recipe.residualCoefficientBudget line 36
  3. lemma OAI.SKGapCutoff.Recipe.residualCoefficientBudget_antitone line 38
  4. lemma OAI.SKGapCutoff.Recipe.residualCoefficientBudget_ge line 43
  5. lemma OAI.SKGapCutoff.Recipe.residualCoefficientBudget_step line 48
  6. theorem OAI.SKGapCutoff.Recipe.uniform_ordinary_weak_residual line 56
  7. def OAI.SKGapCutoff.Static.UniformSquare line 86
  8. lemma OAI.SKGapCutoff.Static.UniformSquare.zero line 91
  9. lemma OAI.SKGapCutoff.Static.UniformSquare.congr line 94
  10. lemma OAI.SKGapCutoff.Static.UniformSquare.add line 98
  11. lemma OAI.SKGapCutoff.Static.UniformSquare.neg line 106
  12. lemma OAI.SKGapCutoff.Static.UniformSquare.sub line 112
  13. lemma OAI.SKGapCutoff.Static.UniformSquare.sum line 115
  14. lemma OAI.SKGapCutoff.Static.scalar_product_bounds line 127
  15. lemma OAI.SKGapCutoff.Static.UniformSquare.mul line 151
  16. lemma OAI.SKGapCutoff.Static.UniformSquare.smul line 163
  17. lemma OAI.SKGapCutoff.Static.UniformSquare.base line 167
  18. lemma OAI.SKGapCutoff.Recipe.uniform_square_normalized_pair line 183
  19. lemma OAI.SKGapCutoff.Recipe.uniform_square_prev_zero line 190