OAI/Probability/SLE/Multipoint/MultipointDiscountProcess.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The compact discounted product along adapted Loewner states. The discount rate may jump at stopping times.

  1. theorem OAI.SLEExactGauge.Multipoint.exists_bounded_discount_cost_process line 17
  2. theorem OAI.SLEExactGauge.Multipoint.compact_discounted_smooth_field line 51
  3. lemma OAI.SLEExactGauge.Multipoint.compact_discounted_process_drift_nonpos line 121