OAI/Probability/SLE/Loewner/InitialChartIdentities.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Forward identities on the domain at the current time, rather than only on the common final domain.

  1. lemma OAI.SLEExactGauge.initialForwardChart_mem_upper line 12
  2. lemma OAI.SLEExactGauge.initialInverse_forward_at line 21