OAI/Probability/SLE/Geometry/FiniteEnergyArcExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

An angular section with finite derivative energy has a continuous extension to both endpoints. The construction is its actual integral primitive.

  1. lemma OAI.SLEExactGauge.finite_energy_angular_extension line 13
  2. lemma OAI.SLEExactGauge.continuous_angular_oscillation_on_endpoints line 35