OAI/Analysis/CircleDomains/Rigidity/MaskIndependentMeanLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The collar tolerance and depth are selected before a period mask is chosen. This follows from the same physical strict lower bound, whose estimates do not use the mask. It allows an inner mask to enclose the chosen integration curve.

  1. theorem OAI.CircleDomainRigidity.exists_smooth_mean_collar_lower_bound_all_masks line 18
  2. theorem OAI.CircleDomainRigidity.exists_gated_mean_collar_lower_bound_all_masks line 58