OAI/Analysis/CircleDomains/Modulus/MarkedConfigurationNorm.lean

GitHub source file

7 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. def OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound line 22

    Source documentation

    The square norm is tested only on the marked compact space.

    def HasHitNormBound (B : ℝ) : Prop :=
…
  2. theorem OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound.summable_sq line 25
  3. theorem OAI.CircleDomainRigidity.MarkedHit.HasHitNormBound.countable_positive_support line 29
  4. def OAI.CircleDomainRigidity.MarkedHit.HasConfigurationBounds line 39

    Source documentation

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

    def HasConfigurationBounds (B : ℝ) : Prop :=
…
  5. theorem OAI.CircleDomainRigidity.MarkedHit.configuration_bound_of_injective line 43
  6. theorem OAI.CircleDomainRigidity.MarkedHit.configuration_square_sum_le line 50
  7. theorem OAI.CircleDomainRigidity.MarkedHit.hasHitNormBound_of_configuration_bounds line 90