OAI/Probability/SLE/Angle/AngleStationaryFlux.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The stationary angular weight puts the cosine generator in divergence form. Its flux vanishes at both endpoints of the actual angle interval.

  1. def OAI.SLEExactGauge.anglePolynomialFlux line 13
  2. lemma OAI.SLEExactGauge.anglePolynomialFlux_hasDerivAt line 16
  3. lemma OAI.SLEExactGauge.anglePolynomialGenerator_stationary_integral line 40