OAI/Analysis/CircleDomains/Selection/CodeBarycenterDensities.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The three components of a coding barycenter have the restrictions of its density. Their square energies are bounded by the total energy.

  1. theorem OAI.CircleDomainRigidity.withDensity_map_comp line 15
  2. theorem OAI.CircleDomainRigidity.withDensity_sumCostMeasures line 27
  3. theorem OAI.CircleDomainRigidity.sumCostMeasures_injective line 37
  4. theorem OAI.CircleDomainRigidity.codeLaw_component_densities line 56
  5. theorem OAI.CircleDomainRigidity.codeReference_component_energies line 73