OAI/Analysis/CircleDomains/Sobolev/L2WeightedErrorSeries.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summable L² errors give summable weighted integrals by the fixed L² gradient in scalar coarea.

  1. theorem OAI.CircleDomainRigidity.lintegral_norm_mul_le_L2 line 13
  2. theorem OAI.CircleDomainRigidity.weighted_L2_errors_summable line 31