OAI/Analysis/CircleDomains/Rigidity/MaskedFilledEnergy.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Charging masked fillings to the original masked cost

Every added disk has zero pairwise wedge cost. Off the disks the intrinsic differentials agree locally with the retained coordinates. This proves the full cofinite masked energy estimate.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsMaskedFilledCircleFamily.integral_wedges_le_original line 21
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.IsMaskedFilledCircleFamily.exists_spherical_metric_of_original_cost line 73