OAI/Probability/SLE/Gauge/CenteredMomentJensen.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Jensen inequalities for the exact stopped coefficients and their prescribed limit. No law after the centered terminal time is used.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.centered_diskScalar_integrable_eq line 20
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.levelCoefficient_jensen line 64
  3. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.finiteMoment_jensen line 96
  4. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.moment_jensen line 124