StoppedInverseTestUniqueness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The original increment and the transported fresh mass have identical positive compact tests simultaneously at every finite future time.

lemma OAI.SLEExactGauge.Multipoint.CanonicalMass.stoppedFreshMass_test_indistinguishable line 37
theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.stoppedFreshMass_indistinguishable line 118
Source documentation
Equality of the actual measure increments on one event for every finite future time, with the unmodified raw fresh functional.
```
theorem CanonicalMass.stoppedFreshMass_indistinguishable
    (hpaths : ∀ᵐ ω ∂P, PositiveMassPaths
      (fun t => stoppedFreshMass B κ γ G F hw τ hc R t ω)
      (stoppedFreshTerminalMass B κ γ G F hw τ hc R ω)) :
    ∀ᵐ ω ∂P, ∀ t,
      C.process (τ ω+t) ω-C.process (τ ω) ω =
        stoppedFreshMass B κ γ G F hw τ hc R t ω := by
…
```
Mentions: OAI.SLEExactGauge.PositiveMassPaths, OAI.SLEExactGauge.Multipoint.stoppedFreshMass, OAI.SLEExactGauge.Multipoint.stoppedFreshTerminalMass