OAI/Analysis/CircleDomains/Modulus/NormalStripRectangleGreen.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The rectangle identity on either side of a regular boundary arc. Three sides vanish for forms localized inside the normal chart.

  1. lemma OAI.CircleDomainRigidity.normal_strip_base_form line 14
  2. lemma OAI.CircleDomainRigidity.pulledPlanarForm_eq_zero line 21
  3. lemma OAI.CircleDomainRigidity.normal_strip_upper_green line 26
  4. lemma OAI.CircleDomainRigidity.normal_strip_lower_green line 74