OAI/Probability/SLE/Stochastic/WienerCoefficientLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Transfer of the exact fixed-angle coefficient limit to the Wiener integrals appearing in the prescribed deterministic gauge.

  1. lemma OAI.SLEExactGauge.Target.measurable_fixedLevelDensity line 15
  2. lemma OAI.SLEExactGauge.Target.measurable_fixedDiscreteMass line 22
  3. lemma OAI.SLEExactGauge.Target.measurable_fixedCoefficient line 31
  4. lemma OAI.SLEExactGauge.Target.levelDensity_nonneg_of_witness line 37
  5. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.wiener_clipped_coefficient_limit line 57
  6. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.wiener_clipped_coefficient_bound line 82