OAI/Probability/SLE/Loewner/TargetContinuationPullback.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The prescribed fresh-driver average pulled back to a regular Brownian presentation, retaining its full natural past.

  1. theorem OAI.SLEExactGauge.Target.continuationMean_comp_condLExp line 18
  2. theorem OAI.SLEExactGauge.Target.continuationMean_comp_finite_condExp line 47
  3. theorem OAI.SLEExactGauge.Target.potentialDifference_comp_eq_current_sub_condExp line 67