OAI/Probability/SLE/Geometry/ExteriorLaplacianTest.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A compactly supported quadratic test near the omitted set of an exterior conformal map. Its Laplacian has nonpositive integral over the image domain.

  1. lemma OAI.SLEExactGauge.complex_laplacian_norm_sq line 15
  2. lemma OAI.SLEExactGauge.exists_compact_quadratic_test line 26
  3. lemma OAI.SLEExactGauge.hasCompactSupport_laplacian line 42
  4. lemma OAI.SLEExactGauge.compact_quadratic_test_complement_integral line 50