OAI/Analysis/CircleDomains/Sobolev/RealGradientNorm.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Exact L² preservation for each derivative component under the planar coordinate change used by finite transfer.

  1. theorem OAI.CircleDomainRigidity.real_chart_partial_eLpNorm line 14
  2. theorem OAI.CircleDomainRigidity.real_chart_zeroExtension_partial_eLpNorm line 37