OAI/Probability/SLE/Loewner/ReverseBoundarySquare.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Squared centered reverse coordinates have a regular derivative even when the initial point is the boundary tip.

  1. lemma OAI.SLEExactGauge.reverse_centered_square_derivative line 13
  2. lemma OAI.SLEExactGauge.reverse_boundary_square_estimate line 31