OAI/Analysis/IntegralMeans/BoundaryTail.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Brennan.outsideCore line 23
  2. lemma OAI.Brennan.measurable_diskCayley line 25
  3. lemma OAI.Brennan.measurableSet_outsideCore line 28
  4. lemma OAI.Brennan.classFun_lower_outsideCore line 31
  5. lemma OAI.Brennan.classFun_ne_zero_outsideCore line 40
  6. def OAI.Brennan.planeClassValue line 44
  7. lemma OAI.Brennan.measurable_planeClassValue line 49
  8. lemma OAI.Brennan.planeClassValue_eq line 60
  9. lemma OAI.Brennan.continuous_classFun_at line 63
  10. lemma OAI.Brennan.measurable_classFun_at line 66
  11. lemma OAI.Brennan.integral_closedBall_translate line 69
  12. lemma OAI.Brennan.volume_real_closedBall_complex line 79
  13. lemma OAI.Brennan.holomorphic_sq_submean_center line 86
  14. lemma OAI.Brennan.holomorphic_sq_submean_lintegral line 97
  15. lemma OAI.Brennan.finite_density_compact_tail line 106
  16. lemma OAI.Brennan.weighted_holomorphic_tail line 124
  17. def OAI.Brennan.HasQuarticTail line 214
  18. lemma OAI.Brennan.quartic_tail_proper line 218
  19. lemma OAI.Brennan.quartic_tail_height_bound line 248
  20. lemma OAI.Brennan.quartic_tail_iff_power line 261
  21. lemma OAI.Brennan.outsideCore_of_norm line 274
  22. lemma OAI.Brennan.class_quartic_tail line 285
  23. lemma OAI.Brennan.class_proper_preimage line 305
  24. lemma OAI.Brennan.class_preimage_height_bound line 314