OAI/Analysis/CircleDomains/Topology/CompactSourceCutoff.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A compact source cutoff turns local differential energy into a compact continuous Sobolev test without making any boundary extension assumption.

  1. theorem OAI.CircleDomainRigidity.scalar_times_cutoff_derivative_memLp line 14
  2. theorem OAI.CircleDomainRigidity.cutoff_times_local_derivative_memLp line 22
  3. theorem OAI.CircleDomainRigidity.compact_source_cutoff_gradient_memLp_on line 50
  4. theorem OAI.CircleDomainRigidity.compact_source_cutoff_gradient_memLp line 70