OAI/Analysis/IntegralMeans/CircleBounds.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.circlePoint line 10
  2. def OAI.Brennan.arcInterval line 12
  3. def OAI.Brennan.arcD line 14
  4. def OAI.Brennan.arcX line 16
  5. def OAI.Brennan.arcY line 18
  6. def OAI.Brennan.arcXDeriv line 20
  7. lemma OAI.Brennan.arc_cos_nonneg line 22
  8. lemma OAI.Brennan.arcD_bounds line 26
  9. lemma OAI.Brennan.arcX_bounds line 39
  10. lemma OAI.Brennan.arcY_bounds line 56
  11. lemma OAI.Brennan.arcX_hasDerivAt line 71
  12. lemma OAI.Brennan.arcXDeriv_lower line 86
  13. lemma OAI.Brennan.continuousOn_arcXDeriv line 97
  14. lemma OAI.Brennan.arcX_monotone line 106
  15. lemma OAI.Brennan.circlePoint_norm line 115
  16. lemma OAI.Brennan.circlePoint_re line 118
  17. lemma OAI.Brennan.circlePoint_im line 121
  18. lemma OAI.Brennan.one_add_circlePoint_norm_sq line 124
  19. lemma OAI.Brennan.circlePoint_mem_disk line 140
  20. lemma OAI.Brennan.neg_circlePoint_mem_disk line 143
  21. lemma OAI.Brennan.halfCayley_re line 146
  22. lemma OAI.Brennan.halfCayley_neg_circlePoint line 152
  23. lemma OAI.Brennan.classWeight_vertical_bound line 166
  24. lemma OAI.Brennan.classWeight_vertical_compare line 189
  25. lemma OAI.Brennan.inverse_deriv_square_conversion line 207
  26. lemma OAI.Brennan.continuous_weightAt line 241
  27. def OAI.Brennan.horizontalMass line 250
  28. lemma OAI.Brennan.horizontalMass_apply line 253
  29. lemma OAI.Brennan.continuous_horizontalWeight line 258
  30. lemma OAI.Brennan.horizontalMass_half line 263
  31. lemma OAI.Brennan.horizontalMass_dyadic line 296
  32. lemma OAI.Brennan.horizontalMass_dyadic_le line 305
  33. lemma OAI.Brennan.transferOperator_uniform_growth line 311
  34. lemma OAI.Brennan.continuous_circlePoint line 336
  35. lemma OAI.Brennan.continuous_circle_deriv_rpow line 340
  36. lemma OAI.Brennan.continuous_neg_circle_deriv_rpow line 349
  37. lemma OAI.Brennan.arc_integral_bound line 358
  38. lemma OAI.Brennan.arc_integral_dyadic_bound line 406
  39. def OAI.Brennan.rotateDisk line 426
  40. lemma OAI.Brennan.rotateDisk_maps line 428
  41. lemma OAI.Brennan.rotateDisk_hasDerivAt line 432
  42. lemma OAI.Brennan.rotateDisk_schlicht line 441
  43. lemma OAI.Brennan.circlePoint_shift line 452
  44. lemma OAI.Brennan.circle_arc_dyadic_bound line 457
  45. lemma OAI.Brennan.periodic_circlePoint line 473
  46. lemma OAI.Brennan.full_circle_dyadic_bound line 476
  47. lemma OAI.Brennan.dyadic_growth_compare line 519
  48. lemma OAI.Brennan.uniform_inverse_square_bound line 535