OAI/Probability/SLE/Multipoint/MultipointRegularizedField.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual smooth factor on either side of a regulator midpoint. Its only parameters are the constant and logarithmic slope of that branch.

  1. def OAI.SLEExactGauge.Multipoint.regularizedLogFactor line 12
  2. def OAI.SLEExactGauge.Multipoint.branchRegulator line 17
  3. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_contDiff line 20
  4. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_eq line 25
  5. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_pos line 39
  6. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_spatial line 45
  7. def OAI.SLEExactGauge.Multipoint.logGenerator line 68
  8. lemma OAI.SLEExactGauge.Multipoint.logGenerator_add line 72
  9. lemma OAI.SLEExactGauge.Multipoint.logGenerator_const_mul line 92
  10. theorem OAI.SLEExactGauge.Multipoint.regularizedLogFactor_generator line 106