OAI/Analysis/CircleDomains/Sobolev/MeanSmoothPhysicalCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mean distinct intersections with a smooth circle-valued coordinate on a compact physical chart. The bound is against the actual mean occupation of the original quotient-path law.

  1. theorem OAI.CircleDomainRigidity.mean_smooth_physical_chart_circle_count_le line 22