OAI/Probability/SLE/Mass/TargetDiscreteMassRecovery.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The exact finite sum in the prescribed coefficient formula agrees with the stopped predictable compensator once its potential increments have been identified. The endpoint is allowed to be infinite.

  1. lemma OAI.SLEExactGauge.compensator_before_extended_sum line 16
  2. lemma OAI.SLEExactGauge.target_mesh_time line 27
  3. lemma OAI.SLEExactGauge.target_discreteMass_eq_sum line 34
  4. theorem OAI.SLEExactGauge.target_discreteMass_tendstoInMeasure line 43