OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasepointConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanFactorModel.nearby_labels_of_concentration line 27

   Source documentation

   The deterministic conclusion of the basepoint argument, keeping the already proved sampling geometry and concentration estimates separate.

   theorem nearby_labels_of_concentration
       (hD : Continuous F.ExpD)
       (chartD : GroupLieAlgebra (𝓘(ℝ, F.D.modelSpace)) F.D.carrier ≃ₜ F.D.carrier)
       (hchartD : ∀ v, chartD v = F.ExpD v)
       (π : G →* Multiplicative W) (height : H →ₗ[ℝ] W)
       (hheight : Function.Surjective height)
       (hchartheight : ∀ v, (π (F.inclusionD (chartD (F.D.equiv v)))).toAdd = height v)
       (hkill : ∀ u v : H, height ⁅u, v⁆ = 0)
       (A : L → W →L[ℝ] W) (hA : Function.Injective A)
       (J : P → G → W) (hJ : ∀ p, Continuous (J p))
       (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       {ρ R η t : ℝ} (hρ : 0 < ρ) (hR : 0 < R) (hρR : ρ ≤ R) (ht : 0 < t)
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections