ActualFiniteBoundaryExtension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite boundary extension required by the SLE application, proved from the capacity witness. Small inverse half-disks are Cauchy; completeness gives the boundary limits and the existing tip limit fixes the extension at the driver.

lemma OAI.SLEExactGauge.IsCapacityTwoWitness.finite_real_boundary_limit line 17
theorem OAI.SLEExactGauge.actual_finiteLoewnerBoundaryExtension line 41
Source documentation
Continuous finite boundary extension of the inverse Loewner map.
```
theorem actual_finiteLoewnerBoundaryExtension : PublishedFiniteLoewnerBoundaryExtension := by
…
```
Mentions: OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension