OAI/Analysis/StrictMeans/AreaCoefficients.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.norm_sq_sub_complex line 12
  2. theorem OAI.StrictInverseFirstPower.norm_sq_center_le_circleAverage line 18
  3. lemma OAI.StrictInverseFirstPower.inverse_sq_conj_of_norm_eq line 52
  4. lemma OAI.StrictInverseFirstPower.norm_sq_inverse_sq_sub line 66
  5. theorem OAI.StrictInverseFirstPower.circleAverage_norm_sq_pole line 73
  6. theorem OAI.StrictInverseFirstPower.circleAverage_norm_sq_pole_lower line 105
  7. lemma OAI.StrictInverseFirstPower.circleAverage_eq_integral_neg_pi line 112
  8. lemma OAI.StrictInverseFirstPower.lintegral_circle_eq line 119
  9. lemma OAI.StrictInverseFirstPower.annulus_lintegral_polar_lower line 138
  10. lemma OAI.StrictInverseFirstPower.radial_pole_integral line 174
  11. lemma OAI.StrictInverseFirstPower.pole_circle_density_lower line 193
  12. theorem OAI.StrictInverseFirstPower.annulus_pole_area_lower line 216
  13. theorem OAI.StrictInverseFirstPower.re_le_of_forall_mem_frontier_re_le line 276
  14. theorem OAI.StrictInverseFirstPower.norm_realLinear_le_of_frontier line 286
  15. theorem OAI.StrictInverseFirstPower.det_complexDerivative line 315
  16. theorem OAI.StrictInverseFirstPower.holomorphic_area line 323
  17. theorem OAI.StrictInverseFirstPower.holomorphic_integral_image line 331
  18. def OAI.StrictInverseFirstPower.ellipseLinear line 339
  19. lemma OAI.StrictInverseFirstPower.ellipseLinear_apply line 342
  20. lemma OAI.StrictInverseFirstPower.det_ellipseLinear line 344
  21. lemma OAI.StrictInverseFirstPower.norm_ellipseLinear_lower line 353
  22. def OAI.StrictInverseFirstPower.ellipseInverse line 360
  23. lemma OAI.StrictInverseFirstPower.ellipseLinear_inverse line 362
  24. lemma OAI.StrictInverseFirstPower.norm_ellipseInverse_le_two line 374
  25. lemma OAI.StrictInverseFirstPower.ellipseInverse_add line 381
  26. lemma OAI.StrictInverseFirstPower.ellipseInverse_linear line 386
  27. lemma OAI.StrictInverseFirstPower.volume_ellipse_le line 396
  28. lemma OAI.StrictInverseFirstPower.norm_ellipseInverse_eq line 407
  29. theorem OAI.StrictInverseFirstPower.ellipse_max_annulus line 412
  30. theorem OAI.StrictInverseFirstPower.volume_image_annulus_le line 444
  31. lemma OAI.StrictInverseFirstPower.ellipse_pole_identity line 464
  32. lemma OAI.StrictInverseFirstPower.ellipse_pole_boundary line 473
  33. lemma OAI.StrictInverseFirstPower.deriv_diffContOnCl_inner line 488
  34. lemma OAI.StrictInverseFirstPower.pole_annulus_comparison line 494
  35. lemma OAI.StrictInverseFirstPower.pole_area_small_radius line 538
  36. lemma OAI.StrictInverseFirstPower.pole_coefficient_radius line 595
  37. theorem OAI.StrictInverseFirstPower.pole_coefficient_le_one line 615