OAI/Analysis/CircleDomains/Selection/RealStageEstimates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Analytic and geometric consequences of an actual real transfer stage.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.source_infty line 23
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.prescribed_core_model line 26
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.prescribed_core_conformal line 29
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.functions_smooth_source line 32
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.functions_integrable_source line 38
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.source_energy_lt line 44
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.retained_on_core line 56
  8. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTransferStage.terminal_frontier_extension line 60