OAI/Analysis/CircleDomains/Rigidity/TraceCompression.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The scalar tail compression used for common-point traces. The null-image recovery works for arbitrary subsets of the line, by applying the monotone area formula to a measurable envelope. No analyticity premise is needed.

  1. theorem OAI.CircleDomainRigidity.null_outside_of_compressed_image_null line 15
  2. def OAI.CircleDomainRigidity.traceCompression line 46
  3. theorem OAI.CircleDomainRigidity.traceCompression_intervalIntegrable line 49
  4. theorem OAI.CircleDomainRigidity.traceCompression_sub line 55
  5. theorem OAI.CircleDomainRigidity.traceCompression_monotone line 61
  6. theorem OAI.CircleDomainRigidity.traceCompression_lipschitz line 69
  7. theorem OAI.CircleDomainRigidity.traceCompression_ae_deriv line 79
  8. theorem OAI.CircleDomainRigidity.traceCompression_null_recovery line 89
  9. theorem OAI.CircleDomainRigidity.null_of_tail_compressions line 94