OAI/Analysis/CircleDomains/Modulus/ConfigurationNorm.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Testing all sizes and reciprocal separation scales is sufficient to control the full square norm of the point-hit probabilities.

  1. theorem OAI.CircleDomainRigidity.exists_reciprocal_separation line 16
  2. def OAI.CircleDomainRigidity.HasConfigurationBounds line 35

    Source documentation

    This hypothesis runs over a countable list of compact configuration spaces.

    def HasConfigurationBounds (B : ℝ) : Prop :=
…
  3. theorem OAI.CircleDomainRigidity.configuration_bound_of_injective line 39
  4. theorem OAI.CircleDomainRigidity.configuration_square_sum_le line 46
  5. theorem OAI.CircleDomainRigidity.hasHitNormBound_of_configuration_bounds line 86