OAI/Analysis/CircleDomains/Sobolev/PatchBandPreservation.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Positive partition sums preserve every boundary band when all active sampling patches shrink towards that boundary point.

  1. def OAI.CircleDomainRigidity.LocalPatchSupport line 22
  2. theorem OAI.CircleDomainRigidity.positive_patch_eventual_bounds line 25
  3. theorem OAI.CircleDomainRigidity.band_inclusion_of_eventual_interval_preservation line 39
  4. theorem OAI.CircleDomainRigidity.positive_patch_band_inclusion line 70
  5. theorem OAI.CircleDomainRigidity.localPatchSupport_of_tendsto_radius line 87
  6. theorem OAI.CircleDomainRigidity.localPatchSupport_of_dust_distance line 103