FiniteLabelTransport.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Measurable finite labels along converging measure-preserving maps

This is the local transport step in the profile affinity argument. A common finite-measure carrier lets continuity of measurable-set preimages control every label fiber. Relations between two transported labels then pass to the limit directly, without selecting pointwise values on exceptional sets.

theorem OAI.PolycyclicRecognition.finiteLabel_disagreement_tendsto line 22

theorem OAI.PolycyclicRecognition.relation_of_disagreement_tendsto line 62

Source documentation

Relations between finite transported labels survive the limit because the exceptional disagreement sets have vanishing measure.

theorem relation_of_disagreement_tendsto
    {X I J ι : Type*} [MeasurableSpace X]
    {μ : Measure X} {l : Filter ι} [l.NeBot]
    (f : ι → X → I) (g : ι → X → J) (f₀ : X → I) (g₀ : X → J)
    (R : I → J → Prop)
    (hR : ∀ᶠ n in l, ∀ᵐ x ∂μ, R (f n x) (g n x))
    (hf : Tendsto (fun n => μ {x | f n x ≠ f₀ x}) l (𝓝 0))
    (hg : Tendsto (fun n => μ {x | g n x ≠ g₀ x}) l (𝓝 0)) :
    ∀ᵐ x ∂μ, R (f₀ x) (g₀ x) := by
…

theorem OAI.PolycyclicRecognition.finiteLabel_relation_transport line 92

Source documentation

Local chamber relations pass to the limiting flow maps. The common carrier is needed only to localize the measurable finite label field.

theorem finiteLabel_relation_transport
    {X Y I ι : Type*}
    [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X]
    [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y]
    [Fintype I] [MeasurableSpace I] [MeasurableSingletonClass I]
    {μ : Measure X} {ν : Measure Y} [μ.InnerRegularCompactLTTop] [IsLocallyFiniteMeasure ν]
    (label : Y → I) (hlabel : Measurable label)
    {l : Filter ι} [l.NeBot] (φ ψ : ι → C(X, Y)) (φ₀ ψ₀ : C(X, Y))
    (hφ : Tendsto φ l (𝓝 φ₀)) (hψ : Tendsto ψ l (𝓝 ψ₀))
    (hφpres : ∀ᶠ n in l, MeasurePreserving (φ n) μ ν)
    (hψpres : ∀ᶠ n in l, MeasurePreserving (ψ n) μ ν)
    (hφpres₀ : MeasurePreserving φ₀ μ ν) (hψpres₀ : MeasurePreserving ψ₀ μ ν)
…