OAI/Analysis/CircleDomains/Sobolev/ActualLocalIntegrability.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Local derivative integrability follows from the actual bounded image of each compact source disk. No boundary area or integrability premise is needed for the finite-hole estimate.

  1. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.finite_part_differentiableOn line 18
  2. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.selectedPlane_eq_finite_part line 25
  3. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.finite_part_injOn line 30
  4. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.actual_local_derivative_integrable line 41
  5. theorem OAI.CircleDomainRigidity.MatchedConformalEnds.exists_source_containment_radius line 63