OAI/Analysis/CircleDomains/Rigidity/TraceCompressionPayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

An inactive prefix lets scalar tail compression be compared with the actual infinite mask. The spatial payment is valid across all component types; continuity of the unmasked scalar is not required.

  1. theorem OAI.CircleDomainRigidity.infiniteTraceMask_eq_one line 14
  2. theorem OAI.CircleDomainRigidity.traceCompression_increment_le line 21
  3. theorem OAI.CircleDomainRigidity.masked_trace_compression_payment line 42