OAI/Analysis/CircleDomains/Sobolev/CircleFilledEnergy.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Charging circle fillings to the original domain

The smooth circle fillings preserve differentials off the disks and have rank at most one inside them. Thus their cost is charged entirely to the original domain, and one common spherical metric controls the actual transferred circle energies.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.eventuallyEq_outside line 22
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.circleWedges_eq_zero line 41
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.circleWedges_eq_outside line 50
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.circleWedges_nonneg line 61
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.continuousOn_circleWedges line 66
  6. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.integral_wedges_le_original line 81
  7. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsFilledCircleFamily.exists_spherical_metric_of_original_cost line 118