OAI/Probability/SLE/Angle/AngleLogCosineDerivatives.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Brownian second derivative and physical Loewner directional derivative of the actual cosine coordinate.

  1. lemma OAI.SLEExactGauge.logCosine_spatial_second line 11
  2. lemma OAI.SLEExactGauge.logInverseNorm_directional line 37
  3. lemma OAI.SLEExactGauge.logCosine_directional line 71
  4. lemma OAI.SLEExactGauge.logCosine_physical_direction line 90