OAI/Probability/SLE/Multipoint/MultipointDiscountedField.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The smooth discounted product used between consecutive switches.

  1. def OAI.SLEExactGauge.Multipoint.discountedProduct line 11
  2. lemma OAI.SLEExactGauge.Multipoint.discountedProduct_contDiff line 15
  3. lemma OAI.SLEExactGauge.Multipoint.discountedProduct_directional line 23
  4. lemma OAI.SLEExactGauge.Multipoint.discountedProduct_spatial_second line 41
  5. lemma OAI.SLEExactGauge.Multipoint.discountedProduct_directional_congr line 49
  6. theorem OAI.SLEExactGauge.Multipoint.discountedProduct_generator_nonpos line 57