OAI/Probability/SLE/Angle/TargetPotentialIncrement.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exact fresh-driver average in the source's potential difference is a conditional expectation, including its finite-value convention.

  1. lemma OAI.SLEExactGauge.Target.mesh_eq_compensatorMeshTime line 16
  2. lemma OAI.SLEExactGauge.Target.potentialDifference_eq_current_sub_condExp line 20
  3. theorem OAI.SLEExactGauge.Target.potentialDifference_eq_mass_increment line 41