OAI/Analysis/IntegralMeans/NegativeArea.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Brennan.polar_symm_circle line 10
  2. lemma OAI.Brennan.disk_lintegral_le_polar line 13
  3. lemma OAI.Brennan.integrableOn_disk_of_circle_bound line 42
  4. lemma OAI.Brennan.circle_lintegral_eq line 63
  5. lemma OAI.Brennan.continuousOn_deriv_univalent line 83
  6. lemma OAI.Brennan.continuousOn_deriv_norm_rpow line 87
  7. lemma OAI.Brennan.integrableOn_boundary_rpow line 93
  8. lemma OAI.Brennan.integrableOn_disk_of_power_circle_bound line 100
  9. lemma OAI.Brennan.integrableOn_disk_boundary_power line 110
  10. lemma OAI.Brennan.integrableOn_geometric_product line 128
  11. lemma OAI.Brennan.schlicht_inverse_bound_small line 149
  12. lemma OAI.Brennan.inverse_square_bound_all line 161
  13. lemma OAI.Brennan.weighted_inverse_integrable line 185
  14. lemma OAI.Brennan.schlicht_negative_area line 224