PathHitLaws.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Closed path-hit relations and the joint upper semicontinuity of their probabilities. The time interval is compact, so projection of the closed incidence relation is closed. Weak convergence and the existing Portmanteau theorem then apply to the product with the moving point mass. This supplies the actual hit function used in law fusion.

abbrev OAI.CircleDomainRigidity.PathTime line 24
theorem OAI.CircleDomainRigidity.product_dirac_closed_section line 35
theorem OAI.CircleDomainRigidity.closed_section_probability_upperSemicontinuous line 46
Source documentation
Closed incidence has jointly upper semicontinuous hit probability in the weak law and the tested point. No regularity of individual path lengths is involved.
```
theorem closed_section_probability_upperSemicontinuous {H : Set (Ω × X)}
    (hH : IsClosed H) :
    UpperSemicontinuous (fun p : ProbabilityMeasure Ω × X =>
      (p.1 : Measure Ω) {ω | (ω, p.2) ∈ H}) := by
…
```
def OAI.CircleDomainRigidity.pathHitSet line 64
theorem OAI.CircleDomainRigidity.isClosed_pathHitSet line 67
theorem OAI.CircleDomainRigidity.isClosed_paths_hitting line 83
def OAI.CircleDomainRigidity.pathHitProbability line 90
theorem OAI.CircleDomainRigidity.pathHitProbability_upperSemicontinuous line 93
theorem OAI.CircleDomainRigidity.measurable_pathHitProbability_point line 98
theorem OAI.CircleDomainRigidity.pathHitProbability_le_one line 105
theorem OAI.CircleDomainRigidity.pathHitProbability_comp_upperSemicontinuous line 110
Source documentation
A continuously varying untagged path law retains joint upper semicontinuity. This also applies after a Borel-preserving Polish refinement of the code-law space.
```
theorem pathHitProbability_comp_upperSemicontinuous
    {Z : Type*} [TopologicalSpace Z] {law : Z → ProbabilityMeasure C(PathTime, X)}
    (hlaw : Continuous law) :
    UpperSemicontinuous (fun p : Z × X => pathHitProbability (law p.1) p.2) :=
…
```
Mentions: OAI.CircleDomainRigidity.PathTime, OAI.CircleDomainRigidity.pathHitProbability