OAI/Probability/SLE/Gauge/CanonicalCoverExpectation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Applying the actual finite-cover reduction to canonical terminal mass leaves precisely the expected missed-cell error to be estimated.

  1. theorem OAI.SLEExactGauge.Multipoint.RationalCanonicalMass.prescribed_cover_finite_expectation line 16