OAI/Analysis/CircleDomains/Sobolev/SmoothMeanGraphGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual smoothed mean has the local real-band width and free-fiber properties used by mixed grid geometry. These are derived from its retained correction and the original arc law.

  1. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.branch_width_le_hit line 19
  2. theorem OAI.CircleDomainRigidity.SmoothMeanPeriodData.free_fiber_subsingleton line 57