OAI/Analysis/CircleDomains/Selection/HitConfigurations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Compact spaces of separated weighted point configurations, and the actual uniform-neighborhood estimate for weighted hit probabilities over each such space.

  1. abbrev OAI.CircleDomainRigidity.HitConfigurationAmbient line 15
  2. def OAI.CircleDomainRigidity.hitConfigurationSet line 18
  3. theorem OAI.CircleDomainRigidity.isClosed_hitConfigurationSet line 23
  4. abbrev OAI.CircleDomainRigidity.HitConfiguration line 34
  5. instance OAI.CircleDomainRigidity.(instance at line 37) line 37
  6. def OAI.CircleDomainRigidity.weightedConfigurationHits line 41
  7. theorem OAI.CircleDomainRigidity.weightedConfigurationHits_nonneg line 46
  8. theorem OAI.CircleDomainRigidity.weightedConfigurationHits_upperSemicontinuous line 52
  9. theorem OAI.CircleDomainRigidity.exists_open_uniform_configuration_bound line 73

    Source documentation

    A uniform strict configuration bound at a center holds throughout some open neighborhood of that center. No continuity of the individual hit functions is assumed.

    theorem exists_open_uniform_configuration_bound
    {X Z : Type*} [MetricSpace X] [CompactSpace X] [SecondCountableTopology X]
    [MeasurableSpace X] [BorelSpace X]
    [MeasurableSpace C(PathTime, X)] [BorelSpace C(PathTime, X)]
    [TopologicalSpace Z] {law : Z → ProbabilityMeasure C(PathTime, X)}
    (hlaw : Continuous law) {n : ℕ} {r c : ℝ} {z : Z}
    (hz : ∀ p : HitConfiguration X n r, weightedConfigurationHits law z p < c) :
    ∃ U : Set Z, IsOpen U ∧ z ∈ U ∧
      ∀ y ∈ U, ∀ p : HitConfiguration X n r, weightedConfigurationHits law y p < c := by
…

    Mentions: OAI.CircleDomainRigidity.PathTime, OAI.CircleDomainRigidity.HitConfiguration, OAI.CircleDomainRigidity.weightedConfigurationHits