OccupationCompactRestriction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Compactly supported starting densities in the profile argument

theorem OAI.PolycyclicRecognition.productOccupationLaw_map_right line 15

theorem OAI.PolycyclicRecognition.productOccupationLaw_supportedRestriction line 33

Source documentation

Restricting the starting probability to a compact carrying set does not change the occupation law.

theorem productOccupationLaw_supportedRestriction
    {A V X : Type*} [MeasurableSpace A] [MeasurableSpace V] [MeasurableSpace X]
    (μ : ProbabilityMeasure A) (η : ProbabilityMeasure V) (K : Set V)
    (hK : MeasurableSet K) (hfull : ∀ᵐ z ∂(η : Measure V), z ∈ K)
    (p : A × V → X) (hp : Measurable p) :
    productOccupationLaw μ (supportedProbabilityRestriction η K hK hfull)
      (fun z => p (z.1, z.2.val)) = productOccupationLaw μ η p := by
…

Mentions: OAI.PolycyclicRecognition.productOccupationLaw, OAI.PolycyclicRecognition.supportedProbabilityRestriction

def OAI.PolycyclicRecognition.flowTimeSlice line 48
Source documentation
Evaluation at a fixed time is continuous in the topology of uniform convergence on compact sets.
```
def flowTimeSlice {V : Type*} [TopologicalSpace V]
    (F : C(V × ℝ, V)) (T : ℝ) : C(V, V) :=
…
```
theorem OAI.PolycyclicRecognition.flowTimeSlice_tendsto line 52