OAI/Probability/SLE/Geometry/HolomorphicAcrossReal.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A continuous function holomorphic on both sides of the real line is holomorphic across it, by splitting rectangular Cauchy integrals.

  1. lemma OAI.SLEExactGauge.rectangle_differentiable_off_real line 13
  2. lemma OAI.SLEExactGauge.rectangle_wedge_zero_one_side line 30
  3. theorem OAI.SLEExactGauge.differentiableOn_of_continuousOn_off_real line 37