OAI/Probability/SLE/Loewner/InverseRectangleEnergy.lean
1 declarations, 0 contain sorry, 0 declared as axioms
Fubini transfers the common inverse-chart Dirichlet bound to vertical sections over a bounded real interval.
- theorem
OAI.SLEExactGauge.initialInverse_rectangle_energyline 13