OAI/Probability/SLE/Geometry/AnalyticFluxEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The first Taylor coefficient is bounded by the signed area of a holomorphic disk map. No injectivity of the disk map is needed.

  1. lemma OAI.SLEExactGauge.analytic_norm_sq_laplacian line 15
  2. lemma OAI.SLEExactGauge.analytic_flux_ge_first_coefficient line 21