OAI/Analysis/BackwardIntertwiners/CoefficientSupport.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BackwardIntertwiners.coefficientObstacle line 11
  2. def OAI.BackwardIntertwiners.coefficientEnvelope line 13
  3. lemma OAI.BackwardIntertwiners.CoefficientEnvelope.unbounded line 24
  4. lemma OAI.BackwardIntertwiners.CoefficientEnvelope.minorant line 30
  5. lemma OAI.BackwardIntertwiners.CoefficientEnvelope.properties line 39
  6. theorem OAI.BackwardIntertwiners.no_both_unbounded line 70
  7. def OAI.BackwardIntertwiners.boundedSideTail line 96
  8. lemma OAI.BackwardIntertwiners.boundedSideTail_nonneg line 99
  9. lemma OAI.BackwardIntertwiners.boundedSideTail_mono line 102
  10. lemma OAI.BackwardIntertwiners.boundedSideTail_tendsto line 112
  11. theorem OAI.BackwardIntertwiners.no_unbounded_against_min line 137
  12. def OAI.BackwardIntertwiners.positiveLog line 207
  13. def OAI.BackwardIntertwiners.negativeLog line 208
  14. def OAI.BackwardIntertwiners.stepRatio line 209
  15. lemma OAI.BackwardIntertwiners.stepRatio_summable line 211
  16. lemma OAI.BackwardIntertwiners.bounds_of_weight line 237
  17. lemma OAI.BackwardIntertwiners.boundedSideTail_summable line 252
  18. lemma OAI.BackwardIntertwiners.nat_support_unbounded line 276
  19. lemma OAI.BackwardIntertwiners.bounded_above_of_min line 288