OAI/GroupTheory/PolycyclicRecognition/Analysis/AffineScaleStabilization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.affine_scale_labels_and_offsets line 16

   Source documentation

   Mixed concentration and the exact chart transition stabilize the finite labels. The offsets are compared in the physical source-scale normalization.

   theorem affine_scale_labels_and_offsets
       {X Z W L : Type*} [TopologicalSpace X] [T2Space X]
       [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Z] [CompactSpace Z]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [Fintype L] [Nonempty L]
       (μ ν : ℕ → ProbabilityMeasure X) (C D : ℕ → Set X)
       (hC : ∀ n, IsCompact (C n)) (hD : ∀ n, IsCompact (D n))
       (hμ : ∀ n, ∀ᵐ x ∂(μ n : Measure X), x ∈ C n)
       (hν : ∀ n, ∀ᵐ x ∂(ν n : Measure X), x ∈ D n)
       (f g : ℕ → X → C(Z, W)) (hf : ∀ n, Continuous (f n)) (hg : ∀ n, Continuous (g n))
       (t : ℕ → ℝ) (φ : ℕ → C(Z, Z)) {K : ℝ} (hK : 0 < K)
       (ht : ∀ n, |t n| ≤ K)
       (hmatch : ∀ n x, f n x = rescaleCompactProfile (t n) (φ n) (g n x))
   …

   Mentions: OAI.PolycyclicRecognition.rescaleCompactProfile