OAI/Probability/SLE/PhysicalTransport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Physical Transport for chordal SLE.

  1. def OAI.SLEExactGauge.SourceInteriorTraceDensityTarget line 16
  2. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.survivingDomain_injective line 21
  3. theorem OAI.SLEExactGauge.sourceInteriorTraceDensity_proved line 34
  4. lemma OAI.SLEExactGauge.source_flow_fence line 67
  5. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.short_flow_bound line 118
  6. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.short_reverse_bound line 138
  7. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.earlier_tip_bound line 181
  8. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.fresh_tip_chart_tendsto line 209
  9. def OAI.SLEExactGauge.SourceFirstHitPhysicalAccessTarget line 255
  10. lemma OAI.SLEExactGauge.disk_distance_gt_before_first_hit line 265
  11. lemma OAI.SLEExactGauge.radialAccess_mem_ball line 284
  12. theorem OAI.SLEExactGauge.sourceFirstHitPhysicalAccess line 292
  13. def OAI.SLEExactGauge.SourceFirstHitChartAccessTarget line 329
  14. lemma OAI.SLEExactGauge.first_hit_tip_survives_earlier line 345
  15. theorem OAI.SLEExactGauge.sourceFirstHitChartAccess_proved line 366