OAI/Analysis/StrictMeans/CircleBounds.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.horizontalQMean line 11
  2. lemma OAI.StrictInverseFirstPower.continuous_Q_slice line 14
  3. lemma OAI.StrictInverseFirstPower.horizontalQMean_apply line 18
  4. lemma OAI.StrictInverseFirstPower.continuous_Q_slice_apply line 27
  5. lemma OAI.StrictInverseFirstPower.dyadic_left_xy line 33
  6. lemma OAI.StrictInverseFirstPower.dyadic_right_xy line 40
  7. lemma OAI.StrictInverseFirstPower.horizontalQMean_half line 47
  8. lemma OAI.StrictInverseFirstPower.horizontalQMean_dyadic line 78
  9. lemma OAI.StrictInverseFirstPower.horizontalQMean_bound line 87
  10. def OAI.StrictInverseFirstPower.arcDenom line 105
  11. def OAI.StrictInverseFirstPower.arcX line 106
  12. def OAI.StrictInverseFirstPower.arcY line 107
  13. def OAI.StrictInverseFirstPower.arcXDeriv line 108
  14. lemma OAI.StrictInverseFirstPower.arcDenom_pos line 111
  15. lemma OAI.StrictInverseFirstPower.arcDenom_le_four line 118
  16. lemma OAI.StrictInverseFirstPower.arcDenom_ge_one line 124
  17. lemma OAI.StrictInverseFirstPower.arcX_continuous line 131
  18. lemma OAI.StrictInverseFirstPower.arcY_continuous line 136
  19. lemma OAI.StrictInverseFirstPower.arcX_hasDerivAt line 141
  20. lemma OAI.StrictInverseFirstPower.arcXDeriv_continuous line 153
  21. lemma OAI.StrictInverseFirstPower.arcXDeriv_lower line 158
  22. lemma OAI.StrictInverseFirstPower.arcX_bounds line 168
  23. lemma OAI.StrictInverseFirstPower.arcY_pos line 183
  24. lemma OAI.StrictInverseFirstPower.arcY_scale_bounds line 187
  25. lemma OAI.StrictInverseFirstPower.cayley_leftArc line 202
  26. lemma OAI.StrictInverseFirstPower.uniform_vertical_Q_bound line 233
  27. lemma OAI.StrictInverseFirstPower.vertical_Q_comparison line 248
  28. lemma OAI.StrictInverseFirstPower.arc_integral_change_bound line 271
  29. lemma OAI.StrictInverseFirstPower.inverse_disk_deriv_cayley_bound line 309
  30. lemma OAI.StrictInverseFirstPower.half_arc_inverse_bound line 330
  31. def OAI.StrictInverseFirstPower.diskNegateMap line 390
  32. lemma OAI.StrictInverseFirstPower.diskNegateMap_extension line 394
  33. lemma OAI.StrictInverseFirstPower.diskNegateMap_hasDerivAt line 404
  34. def OAI.StrictInverseFirstPower.diskNegateFamily line 414
  35. def OAI.StrictInverseFirstPower.circleInverseDensity line 424
  36. def OAI.StrictInverseFirstPower.leftArcInverseDensity line 427
  37. lemma OAI.StrictInverseFirstPower.circlePoint_mem_disk line 430
  38. lemma OAI.StrictInverseFirstPower.circleInverseDensity_continuous line 435
  39. lemma OAI.StrictInverseFirstPower.circleInverseDensity_periodic line 443
  40. lemma OAI.StrictInverseFirstPower.circleInverseDensity_shift_pi line 454
  41. lemma OAI.StrictInverseFirstPower.leftArcInverseDensity_negate line 462
  42. lemma OAI.StrictInverseFirstPower.wholeCircle_eq_two_left_arcs line 472
  43. lemma OAI.StrictInverseFirstPower.whole_circle_dyadic_operator_bound line 492