OAI/Probability/SLE/Geometry/ComplexDirichletSlices.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite holomorphic energy gives square-integrable derivatives and low-energy angular sections in each unit logarithmic strip.

  1. lemma OAI.SLEExactGauge.deriv_memLp_two_of_energy line 13
  2. lemma OAI.SLEExactGauge.exists_complex_energy_section line 24