OAI/Probability/SLE/Mass/CanonicalMassUniqueness.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The constructed canonical mass does not depend on the convex extraction. The uniqueness argument uses only integrable terminal compact tests and the conditional remainder kernel, rather than second moments of a competitor.

  1. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_process_mean_le line 25
  2. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_terminal_mean_le line 33
  3. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_test_integrable line 39
  4. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_terminal_test_integrable line 50
  5. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_test_adapted line 59
  6. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_cross_mean line 70
  7. lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.uniqueness_test_terminal_mean line 105
  8. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.process_indistinguishable line 141

    Source documentation

    Two canonical mass constructions for the same trace have identical finite time measures on one full-measure event.

    theorem process_indistinguishable (D : CanonicalMass P κ B hBm γ G) :
    ∀ᵐ ω ∂P, ∀ t, C.process t ω = D.process t ω := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.CanonicalMass

  9. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.terminal_ae_eq line 169

    Source documentation

    The locally exhausted terminal measures also agree.

    theorem terminal_ae_eq (D : CanonicalMass P κ B hBm γ G) :
    C.rational.terminal =ᵐ[P] D.rational.terminal := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.CanonicalMass