OAI/Analysis/CircleDomains/Sobolev/LocalizedJordanIntegral.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A form supported in one small normal chart contributes exactly the integral over that parameter arc of the full periodic Jordan circuit.

  1. lemma OAI.CircleDomainRigidity.periodic_deriv_of_periodic line 14
  2. lemma OAI.CircleDomainRigidity.planarFormIntegrand_continuous line 21
  3. lemma OAI.CircleDomainRigidity.planarFormIntegral_eq_shifted line 28
  4. lemma OAI.CircleDomainRigidity.normal_box_parameter_mem line 42
  5. lemma OAI.CircleDomainRigidity.planarFormIntegral_localized line 60