OAI/Analysis/CircleDomains/Sobolev/SmoothMeanBandWeight.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local branch widths are controlled by the actual masked-coordinate weights. Exact Haar length prevents a change of branch from weakening the weight used by subsequent code laws.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.branch_width_le_dustWeight line 18
  2. theorem OAI.CircleDomainRigidity.masked_singular_weight_ge_one line 56