OAI/Analysis/CircleDomains/Sobolev/ConfigurationHitIntegral.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Hit integrals against the actual mean configuration measure are precisely the expected weighted hit counts. This identifies the two sides of the finite split without replacing the configuration measure by abstract test data.

  1. theorem OAI.CircleDomainRigidity.weightedConfigurationHits_le_card line 24
  2. theorem OAI.CircleDomainRigidity.integral_meanConfigurationMeasure_hit line 35