OAI/Analysis/CircleDomains/Sobolev/ComplexCoareaControls.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The scalar coarea estimates transported to full complex-plane levels.

  1. theorem OAI.CircleDomainRigidity.physical_complex_level_integral line 12
  2. theorem OAI.CircleDomainRigidity.complex_coarea_finite_levels line 19
  3. theorem OAI.CircleDomainRigidity.complex_coarea_L2_weight_finite line 34
  4. theorem OAI.CircleDomainRigidity.complex_coarea_L2_errors line 52
  5. theorem OAI.CircleDomainRigidity.complex_coarea_zero_weight line 72