OAI/Analysis/CircleDomains/Topology/CountableBallSynthesis.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Monotone convergence completes ball synthesis for the countable balloon family. The density is the actual sum of weighted indicators.

  1. def OAI.CircleDomainRigidity.countableBallDensity line 13
  2. theorem OAI.CircleDomainRigidity.exists_countable_ball_synthesis_constant line 16