OAI/Analysis/CircleDomains/Rigidity/TraceMaskPrimitive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Integral primitives of the actual finite and infinite trace masks. The finite spatial variation is bounded by interval lengths times cutoff variation, while endpoint changes are always one-Lipschitz.

  1. def OAI.CircleDomainRigidity.finiteTracePrimitive line 15
  2. def OAI.CircleDomainRigidity.infiniteTracePrimitive line 19
  3. theorem OAI.CircleDomainRigidity.finiteTraceMask_norm_le line 23
  4. theorem OAI.CircleDomainRigidity.finiteTraceMask_intervalIntegrable line 29
  5. theorem OAI.CircleDomainRigidity.finiteTracePrimitive_sub line 38
  6. theorem OAI.CircleDomainRigidity.finiteTracePrimitive_lipschitz line 47
  7. theorem OAI.CircleDomainRigidity.finiteTracePrimitive_variation line 58
  8. theorem OAI.CircleDomainRigidity.infiniteTraceMask_bounds line 87
  9. theorem OAI.CircleDomainRigidity.finiteTracePrimitive_tendsto line 93