OAI/Probability/SKGap/Localization/LocalCoefficient.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGapCutoff.Recipe.Args line 15
  2. def OAI.SKGapCutoff.Recipe.localArgs line 17
  3. def OAI.SKGapCutoff.Recipe.partialAt line 20
  4. lemma OAI.SKGapCutoff.Recipe.linear_apply_coordinates line 22
  5. lemma OAI.SKGapCutoff.Recipe.flipHalfDiff_coordinate line 30
  6. lemma OAI.SKGapCutoff.Recipe.coefficient_chain line 37
  7. lemma OAI.SKGapCutoff.Recipe.local_argument_bound line 46
  8. def OAI.SKGapCutoff.Recipe.coefficient line 63
  9. def OAI.SKGapCutoff.Recipe.localPartial line 67
  10. def OAI.SKGapCutoff.Recipe.taylorError line 71
  11. lemma OAI.SKGapCutoff.Recipe.source_derivative_exact line 78
  12. lemma OAI.SKGapCutoff.Recipe.taylor_error_bound line 96