OAI/Analysis/CircleDomains/Modulus/ConfigurationAtomicNorm.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The mean measure of separated unit-square-norm configurations has atomic square norm at most one. Separation makes the point assignment injective; Cauchy--Schwarz then passes the finite-dimensional bound through averaging.

  1. theorem OAI.CircleDomainRigidity.sum_sq_fibers_le line 17
  2. theorem OAI.CircleDomainRigidity.sum_sq_integrals_le_one line 41
  3. theorem OAI.CircleDomainRigidity.HitConfiguration.points_injective line 73
  4. theorem OAI.CircleDomainRigidity.configurationMeasure_atom_real line 81
  5. theorem OAI.CircleDomainRigidity.configurationMeasure_hasAtomicSquareBound line 93
  6. instance OAI.CircleDomainRigidity.(instance at line 101) line 101
  7. theorem OAI.CircleDomainRigidity.meanConfigurationMeasure_atom_real line 104
  8. theorem OAI.CircleDomainRigidity.integrable_configuration_atom line 115
  9. theorem OAI.CircleDomainRigidity.meanConfigurationMeasure_hasAtomicSquareBound line 130