OAI/Analysis/CircleDomains/Modulus/ConcatenatedIncidenceBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countable concatenation preserves each residual incidence inequality. Only the complement of the open pieces must be countable; the pieces' images may overlap and every parameter visit is still charged.

  1. theorem OAI.CircleDomainRigidity.concatenated_piece_incidence_bound line 19
  2. theorem OAI.CircleDomainRigidity.residualIncidenceBound_concatenated_open line 44
  3. theorem OAI.CircleDomainRigidity.residualConstraintFamily_concatenated line 84