OAI/Probability/SLE/Loewner/FutureCapacityAdditive.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing an initial slit and its exact mapped future adds the two hydrodynamic capacities. The composed chart is the later normalized chart, including when the initial time is zero.

  1. def OAI.SLEExactGauge.composedFutureSlitChart line 20
  2. theorem OAI.SLEExactGauge.futureSlitChart_capacity_eq line 56
  3. theorem OAI.SLEExactGauge.futureComposedForward_eq line 67
  4. theorem OAI.SLEExactGauge.futureComposedInverse_eq line 75