OAI/Analysis/CircleDomains/Rigidity/FiniteTraceMask.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual finite lower-envelope masks for the common-point trace argument. The variation is paid only on intervals in which the corresponding cutoff is active. These estimates precede the Sobolev and infinite-mask limits.

  1. def OAI.CircleDomainRigidity.finiteTraceMask line 16
  2. theorem OAI.CircleDomainRigidity.finiteTraceMask_bounds line 21
  3. theorem OAI.CircleDomainRigidity.finiteTraceMask_antitone line 35
  4. theorem OAI.CircleDomainRigidity.finiteTraceMask_eq_one line 41
  5. theorem OAI.CircleDomainRigidity.finiteTraceMask_le_active line 52
  6. theorem OAI.CircleDomainRigidity.finiteTraceMask_zero_of_active line 60
  7. theorem OAI.CircleDomainRigidity.finiteTraceMask_variation line 68
  8. theorem OAI.CircleDomainRigidity.finiteTraceMask_measurable line 91
  9. def OAI.CircleDomainRigidity.infiniteTraceMask line 99
  10. theorem OAI.CircleDomainRigidity.finiteTraceMask_tendsto line 102