OAI/Analysis/CircleDomains/Rigidity/MaskedStageEnergy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Integrability and full masked energy on the actual finite model. The geometric facts retained from construction justify comparison of ordinary integrals on all later subregions.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.integrable_energy line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.energy_lt line 36
  3. def OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.sourceMask line 44
  4. def OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.targetMask line 48
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.transported_energy_lt line 52
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.MaskedCoordinateStage.complex_energy_lt line 88