OAI/Probability/SLE/Geometry/AnalyticCircleSquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The square mean of a holomorphic function bounds its central value. This is the local energy estimate needed for the first exterior coefficient.

  1. lemma OAI.SLEExactGauge.circleAverage_norm_sq_ge line 13
  2. lemma OAI.SLEExactGauge.analytic_circleAverage_norm_sq_ge line 45