OAI/Analysis/CircleDomains/Rigidity/TraceMaskAEPayment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial payment needs only an almost-everywhere density bound. This version applies to the actual L² sum furnished by ball synthesis.

  1. theorem OAI.CircleDomainRigidity.trace_primitive_line_payment_ae line 12
  2. theorem OAI.CircleDomainRigidity.masked_scalar_ACL_of_line_payment_ae line 48
  3. theorem OAI.CircleDomainRigidity.masked_scalar_derivative_of_line_payment_ae line 70