OAI/Analysis/CircleDomains/Sobolev/CoareaZeroProduct.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Coarea transfers a zero weighted Jacobian to zero length on almost every full level; either vanishing gradient may supply the product zero.

  1. theorem OAI.CircleDomainRigidity.sobolev_level_integral_zero_of_product_zero line 12
  2. theorem OAI.CircleDomainRigidity.complex_coarea_zero_product line 27