OAI/Analysis/CircleDomains/Modulus/LocalBandIncidence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Local real trace estimates remove circle-level incidences. Their assembly uses outer measure only, so the free set need not be Borel.

  1. theorem OAI.CircleDomainRigidity.local_level_incidence_null_of_real_trace line 15
  2. theorem OAI.CircleDomainRigidity.level_incidence_null_of_countable_cover line 36
  3. theorem OAI.CircleDomainRigidity.ae_code_free_incidence_null_of_local_real_traces line 52