ProfileIncrementLimits.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Supported increment constraints from actual converging chart flows

def OAI.PolycyclicRecognition.profileIncrementMap line 20
Source documentation
A normalized increment of a profile between two coordinate maps.
```
def profileIncrementMap (S : Set C(V, W)) (K : Set U) (q : ℝ)
    (A T : C(U, V)) : C(S × K, W) :=
…
```
theorem OAI.PolycyclicRecognition.continuous_profileIncrementMap line 25
Source documentation
The increment observable is continuous in the endpoint map.
```
theorem continuous_profileIncrementMap (S : Set C(V, W)) (K : Set U) (q : ℝ)
    (A : C(U, V)) : Continuous (profileIncrementMap S K q A) := by
…
```
Mentions: OAI.PolycyclicRecognition.profileIncrementMap

theorem OAI.PolycyclicRecognition.profileIncrementMap_tendstoUniformly line 32

Source documentation

Varying endpoint maps give uniformly convergent increment observables on a compact profile family and compact starting-point set.

theorem profileIncrementMap_tendstoUniformly
    (S : Set C(V, W)) (hS : IsCompact S) (K : Set U) (hK : IsCompact K)
    (q : ℝ) (A : C(U, V)) {ι : Type*} {l : Filter ι}
    {T : ι → C(U, V)} {T₀ : C(U, V)} (hT : Tendsto T l (𝓝 T₀)) :
    TendstoUniformly (fun i p => profileIncrementMap S K q A (T i) p)
      (profileIncrementMap S K q A T₀) l := by
…

Mentions: OAI.PolycyclicRecognition.profileIncrementMap

theorem OAI.PolycyclicRecognition.profile_increment_mem_on_support line 50

Source documentation

A vanishing expected distance for the actual scaled endpoints forces the limiting segment increment to satisfy the constraint at every supported profile and starting point.

theorem profile_increment_mem_on_support
    (S : Set C(V, W)) (hS : IsCompact S) (K : Set U) (hK : IsCompact K)
    [MeasurableSpace (S × K)] [BorelSpace (S × K)]
    (q : ℝ) (A : C(U, V)) {ι : Type*} {l : Filter ι} [l.NeBot]
    {T : ι → C(U, V)} {T₀ : C(U, V)} (hT : Tendsto T l (𝓝 T₀))
    (μs : ι → ProbabilityMeasure (S × K)) (μ : ProbabilityMeasure (S × K))
    (hμ : Tendsto μs l (𝓝 μ)) {C : Set W} (hC : IsClosed C) (hne : C.Nonempty)
    (herr : Tendsto (fun i => ∫ p, Metric.infDist
      (profileIncrementMap S K q A (T i) p) C ∂(μs i : Measure (S × K))) l (𝓝 0))
    {p : S × K} (hp : p ∈ (μ : Measure (S × K)).support) :
    q • (p.1.val (T₀ p.2.val) - p.1.val (A p.2.val)) ∈ C := by
…

Mentions: OAI.PolycyclicRecognition.profileIncrementMap