OAI/Analysis/StrictMeans/DyadicBounds.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.cayleyToDisk_norm_relation line 35
  2. lemma OAI.StrictInverseFirstPower.halfPlaneQ_norm line 45
  3. lemma OAI.StrictInverseFirstPower.halfPlaneQ_strip_bound line 53
  4. def OAI.StrictInverseFirstPower.xyPoint line 104
  5. lemma OAI.StrictInverseFirstPower.xyPoint_re line 105
  6. lemma OAI.StrictInverseFirstPower.xyPoint_im line 106
  7. lemma OAI.StrictInverseFirstPower.affineProduct_xyPoint line 108
  8. def OAI.StrictInverseFirstPower.horizontalPoint line 115
  9. def OAI.StrictInverseFirstPower.dyadicHeight line 117
  10. lemma OAI.StrictInverseFirstPower.dyadicHeight_pos line 118
  11. lemma OAI.StrictInverseFirstPower.dyadicHeight_le_one line 119
  12. lemma OAI.StrictInverseFirstPower.dyadicHeight_succ line 121
  13. def OAI.StrictInverseFirstPower.gridStart line 124
  14. def OAI.StrictInverseFirstPower.gridEnd line 126
  15. lemma OAI.StrictInverseFirstPower.dyadicLeft_gridStart line 129
  16. lemma OAI.StrictInverseFirstPower.dyadicRight_gridEnd line 133
  17. lemma OAI.StrictInverseFirstPower.dyadic_gridMiddle line 137
  18. lemma OAI.StrictInverseFirstPower.dyadic_shift line 143
  19. lemma OAI.StrictInverseFirstPower.affineOperator_norm_bound line 161
  20. lemma OAI.StrictInverseFirstPower.affineOperator_strip_norm line 170
  21. lemma OAI.StrictInverseFirstPower.dyadic_shift_norm_le line 174