OAI/Analysis/CircleDomains/Probability/ConfigurationMeasures.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Actual finite atomic measures associated to weighted configurations, and their probability barycenters. Integrals against the barycenter are exactly the expected weighted configuration integrals.

  1. def OAI.CircleDomainRigidity.configurationMeasure line 20
  2. theorem OAI.CircleDomainRigidity.measurable_configurationMeasure line 23
  3. theorem OAI.CircleDomainRigidity.lintegral_configurationMeasure line 37
  4. theorem OAI.CircleDomainRigidity.configurationMeasure_mass_le line 47
  5. def OAI.CircleDomainRigidity.meanConfigurationMeasure line 59
  6. theorem OAI.CircleDomainRigidity.lintegral_meanConfigurationMeasure line 62
  7. instance OAI.CircleDomainRigidity.(instance at line 71) line 71