OAI/Probability/SLE/Geometry/CircleRadialFlux.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The ordinary angular integral of radial flux is a circle average of the derivative applied to the position vector.

  1. lemma OAI.SLEExactGauge.circleAverage_eq_neg_pi_integral line 13
  2. lemma OAI.SLEExactGauge.polar_integral_eq_circleAverage line 23
  3. lemma OAI.SLEExactGauge.radial_flux_eq_circleAverage line 29
  4. lemma OAI.SLEExactGauge.radial_flux_continuousOn line 41
  5. lemma OAI.SLEExactGauge.radial_flux_zero line 56