OAI/Probability/SLE/Geometry/ConformalLaplacian.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The real Laplacian transforms by the squared complex derivative. This is the change-of-variables identity used for the exterior area proof.

  1. lemma OAI.SLEExactGauge.complex_composition_hessian line 14
  2. lemma OAI.SLEExactGauge.complex_fderiv_apply line 34
  3. lemma OAI.SLEExactGauge.laplacian_holomorphic_comp line 39