OAI/Analysis/CircleDomains/Sobolev/FiniteGreenAssembly.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite additivity of the actual boundary integral and curl integral, and assembly from a smooth partition on the closed Jordan disk.

  1. lemma OAI.CircleDomainRigidity.planarFormIntegral_finite_sum line 12
  2. lemma OAI.CircleDomainRigidity.integral_planar_curl_finite_sum line 24
  3. lemma OAI.CircleDomainRigidity.finite_green_assembly line 45