OAI/Analysis/CircleDomains/Sobolev/PeriodBranchPhysicalEnergy.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Local branches of the constructed circle stream satisfy the exact physical regularity hypotheses of the period generic-level theorem.

  1. theorem OAI.CircleDomainRigidity.period_branch_physical_energy line 18