OAI/Analysis/BackwardIntertwiners/ExplicitWeights.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.weightBlock line 11
  2. def OAI.BackwardIntertwiners.residueScale line 12
  3. def OAI.BackwardIntertwiners.residueCorrection line 14
  4. def OAI.BackwardIntertwiners.halfExponent line 16
  5. def OAI.BackwardIntertwiners.ResidueBounds line 19
  6. lemma OAI.BackwardIntertwiners.residueScale_ge_two line 21
  7. lemma OAI.BackwardIntertwiners.residueCorrection_nonneg line 25
  8. lemma OAI.BackwardIntertwiners.residueCorrection_le line 32
  9. lemma OAI.BackwardIntertwiners.residueCorrection_mono line 41
  10. lemma OAI.BackwardIntertwiners.halfExponent_mono line 61
  11. lemma OAI.BackwardIntertwiners.halfExponent_lower line 68
  12. lemma OAI.BackwardIntertwiners.halfExponent_zero line 74
  13. lemma OAI.BackwardIntertwiners.residueScale_sq_le line 77
  14. lemma OAI.BackwardIntertwiners.residueCorrection_sqrt_bound line 89
  15. def OAI.BackwardIntertwiners.halfSum line 100
  16. lemma OAI.BackwardIntertwiners.halfSum_zero line 102
  17. lemma OAI.BackwardIntertwiners.halfSum_succ line 103
  18. lemma OAI.BackwardIntertwiners.halfSum_linear line 106
  19. lemma OAI.BackwardIntertwiners.halfSum_bounds line 115
  20. lemma OAI.BackwardIntertwiners.halfSum_quadratic line 134
  21. def OAI.BackwardIntertwiners.bilateralExponent line 162
  22. def OAI.BackwardIntertwiners.bilateralBeta line 166
  23. def OAI.BackwardIntertwiners.bilateralWeight line 169
  24. lemma OAI.BackwardIntertwiners.bilateralWeight_nat line 173
  25. lemma OAI.BackwardIntertwiners.bilateralWeight_neg_nat line 175
  26. lemma OAI.BackwardIntertwiners.bilateralExponent_nonneg line 181
  27. lemma OAI.BackwardIntertwiners.bilateralWeight_pos line 194
  28. lemma OAI.BackwardIntertwiners.bilateralWeight_ratio line 197
  29. lemma OAI.BackwardIntertwiners.bilateralWeight_antitone line 216
  30. lemma OAI.BackwardIntertwiners.halfSum_discreteConvex line 226
  31. lemma OAI.BackwardIntertwiners.halfSum_root_bound line 230
  32. lemma OAI.BackwardIntertwiners.bilateralWeight_roots_summable line 237
  33. lemma OAI.BackwardIntertwiners.bilateralWeight_quadratic line 269