OAI/Analysis/CircleDomains/Rigidity/MaskedWedgeCost.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Random wedge cost on different coordinate masks

Each pair is integrated on the intersection of its two masks. Thus the original fields need square-integrable norm only on their own masks. The same independent-shift estimate controls this actual masked cost.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.maskedStaircaseCost line 20
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.abs_wedge_indicators line 27
  3. theorem OAI.CircleDomainRigidity.FiniteTransfer.integral_abs_wedge_indicators line 33
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.maskedStaircaseCost_nonneg line 40
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.integrable_maskedStaircaseCost_and_mean_le line 48