OAI/Analysis/CircleDomains/Rigidity/AxialBandFlux.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Zero extension of each axial circle increment to all transverse lines. Its integral is exactly the corresponding circle flux.

  1. def OAI.CircleDomainRigidity.axialBandIncrement line 12
  2. theorem OAI.CircleDomainRigidity.axialCircleIncrement_measurable line 16
  3. theorem OAI.CircleDomainRigidity.axialBandIncrement_integrable line 28
  4. theorem OAI.CircleDomainRigidity.integral_axialBandIncrement line 42