OAI/Analysis/CircleDomains/Rigidity/RealBandTagNullTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Null free traces inside a tag: the local variation estimate and its finite physical-plus-visit payment measure are both constructed above.

  1. theorem OAI.CircleDomainRigidity.real_band_tag_null_trace line 17