OAI/Analysis/CircleDomains/Rigidity/EnclosedFluxIntegration.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integrating the finite-circle slice inequality. Both the exact axial circle flux and the area integral are retained.

  1. theorem OAI.CircleDomainRigidity.enclosed_band_subset line 14
  2. theorem OAI.CircleDomainRigidity.enclosed_flux_integration line 25