OAI/Analysis/CircleDomains/Rigidity/CircleProjectionFlux.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The sum of the two axial endpoint integrals is exactly circle flux for bounded measurable boundary values.

  1. def OAI.CircleDomainRigidity.horizontalCircleIncrement line 12
  2. def OAI.CircleDomainRigidity.verticalCircleIncrement line 14
  3. def OAI.CircleDomainRigidity.horizontalCircleFlux line 16
  4. def OAI.CircleDomainRigidity.verticalCircleFlux line 18
  5. theorem OAI.CircleDomainRigidity.circle_projection_flux line 21