OAI/GroupTheory/PolycyclicRecognition/Analysis/DominatedAffineLabels.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.affine_labels_center_error_of_dominated_transport line 17

   Source documentation

   The density bound, the two concentration statements and the exact chart identities give both eventual equality of labels and a vanishing center error. No height conclusion is assumed.

   theorem affine_labels_center_error_of_dominated_transport
       {X V W L : Type*} [MeasurableSpace X]
       [NormedAddCommGroup V] [NormedSpace ℝ V] [ProperSpace V]
       [NormedAddCommGroup W] [NormedSpace ℝ W] [Fintype L] [Nonempty L]
       (q : V →L[ℝ] W) (hq : Function.Surjective q)
       (A : L → W →L[ℝ] W) (hA : Function.Injective A)
       {R S : ℝ} (hR : 0 < R) (hS : 0 < S)
       (ξ μ ν : ℕ → ProbabilityMeasure X)
       (a a' : ℕ → L) (b b' c v : ℕ → W) {t : ℝ} (ht : 0 < t)
       (φ : ℕ → C(closedBall (0 : V) R, closedBall (0 : V) S))
       (ψ : ℕ → X → X) (m : ℕ → X → X → X)
       (f : ℕ → X → C(closedBall (0 : V) R, W))
   …