OAI/Analysis/BackwardIntertwiners/BackwardWeights.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.plusResidue line 14
  2. def OAI.BackwardIntertwiners.minusResidue line 15
  3. lemma OAI.BackwardIntertwiners.plusResidue_bounds line 16
  4. lemma OAI.BackwardIntertwiners.minusResidue_bounds line 17
  5. def OAI.BackwardIntertwiners.explicitExponent line 24
  6. def OAI.BackwardIntertwiners.explicitBeta line 26
  7. def OAI.BackwardIntertwiners.explicitWeight line 28
  8. lemma OAI.BackwardIntertwiners.measurable_halfExponent line 31
  9. lemma OAI.BackwardIntertwiners.measurable_plusResidue line 38
  10. lemma OAI.BackwardIntertwiners.measurable_minusResidue line 39
  11. lemma OAI.BackwardIntertwiners.measurable_explicitExponent line 41
  12. lemma OAI.BackwardIntertwiners.measurable_explicitBeta line 45
  13. lemma OAI.BackwardIntertwiners.measurable_halfSum line 47
  14. lemma OAI.BackwardIntertwiners.measurable_explicitWeight line 50
  15. lemma OAI.BackwardIntertwiners.explicitBeta_pos line 54
  16. lemma OAI.BackwardIntertwiners.explicitWeight_pos line 55
  17. lemma OAI.BackwardIntertwiners.explicitBeta_le line 56
  18. lemma OAI.BackwardIntertwiners.explicitBeta_zero line 59
  19. lemma OAI.BackwardIntertwiners.explicitWeight_zero line 61
  20. lemma OAI.BackwardIntertwiners.explicitWeight_neg_one line 63
  21. lemma OAI.BackwardIntertwiners.explicitWeight_ratio line 66
  22. lemma OAI.BackwardIntertwiners.weightBlock_eventually_ge line 70
  23. lemma OAI.BackwardIntertwiners.halfExponent_drift line 75
  24. lemma OAI.BackwardIntertwiners.halfSum_eventually_affine line 97
  25. def OAI.BackwardIntertwiners.rawBackward line 112
  26. lemma OAI.BackwardIntertwiners.rawBackward_pos line 114
  27. lemma OAI.BackwardIntertwiners.rawBackward_zero line 116
  28. lemma OAI.BackwardIntertwiners.measurable_rawBackward line 118
  29. lemma OAI.BackwardIntertwiners.rawBackward_recurrence line 121
  30. lemma OAI.BackwardIntertwiners.rawBackward_nat_succ line 130
  31. lemma OAI.BackwardIntertwiners.rawBackward_neg_nat line 140
  32. lemma OAI.BackwardIntertwiners.sqrt_error_linear line 150
  33. lemma OAI.BackwardIntertwiners.halfExponent_linear_upper line 155
  34. lemma OAI.BackwardIntertwiners.tendsto_exp_neg45 line 161
  35. lemma OAI.BackwardIntertwiners.rawBackward_decay line 169
  36. lemma OAI.BackwardIntertwiners.rawBackward_bddAbove line 193
  37. def OAI.BackwardIntertwiners.backwardBound line 207
  38. lemma OAI.BackwardIntertwiners.measurable_backwardBound line 208
  39. lemma OAI.BackwardIntertwiners.backwardBound_ge_one line 210
  40. lemma OAI.BackwardIntertwiners.rawBackward_le_bound line 213
  41. def OAI.BackwardIntertwiners.backwardCoeff line 218
  42. lemma OAI.BackwardIntertwiners.measurable_backwardCoeff line 221
  43. lemma OAI.BackwardIntertwiners.backwardCoeff_bounds line 224
  44. lemma OAI.BackwardIntertwiners.backwardCoeff_pos line 231
  45. lemma OAI.BackwardIntertwiners.backwardCoeff_recurrence line 234
  46. lemma OAI.BackwardIntertwiners.backwardCoeff_ae_pos line 240