OAI/Analysis/CircleDomains/Sobolev/CircleSmoothingBands.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A smoothing discrepancy tending to zero leaves both endpoints of every bounded local real band unchanged.

  1. theorem OAI.CircleDomainRigidity.tendsto_zero_of_abs_le_tolerance line 15
  2. theorem OAI.CircleDomainRigidity.bounded_bands_eq_of_sub_tendsto_zero line 24
  3. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_sub line 51
  4. theorem OAI.CircleDomainRigidity.OpenPlanePartition.adjustedCircleMix_bands_eq line 60