OAI/Probability/SLE/Loewner/InitialCapacity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A monotone positive capacity parameter on the exact initial subarcs.

  1. structure OAI.SLEExactGauge.SimpleSlitChart line 12
  2. lemma OAI.SLEExactGauge.exists_simpleSlitChart line 28
  3. def OAI.SLEExactGauge.initialSlitChart line 34
  4. lemma OAI.SLEExactGauge.SimpleSlitChart.capacity_le_of_range_subset line 40
  5. def OAI.SLEExactGauge.initialCapacity line 50
  6. lemma OAI.SLEExactGauge.initialCapacity_zero line 54
  7. lemma OAI.SLEExactGauge.initialCapacity_pos line 58
  8. lemma OAI.SLEExactGauge.initialCapacity_nonneg line 64
  9. theorem OAI.SLEExactGauge.initialCapacity_monotone line 71