OAI/Analysis/CircleDomains/Topology/MeanSigmaCompactPhysicalCount.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Differential-weighted mean intersection bounds on an open physical chart, exhausted by compact sets. The law may contain paths with repeats.

  1. theorem OAI.CircleDomainRigidity.mean_sigmaCompact_physical_chart_circle_count_le line 21