OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanBasepointAffineComparison.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Continuity in the nilpotent sample, including restriction to any compact chart. This supplies all measurable bad sets below.

   theorem continuous_realScaleProfile_restrict
       (hD : Continuous F.ExpD) (J : G → W) (hJ : Continuous J) (x : G)
       (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       (r : ℝ) (Z : Set (Fin (finrank ℝ H) → ℝ)) :
       Continuous (fun k => (F.realScaleProfile hD J hJ x X S β r k).restrict Z) :=
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections

2. theorem OAI.PolycyclicRecognition.CartanFactorModel.basepoint_affine_labels_of_sampling line 42

   Source documentation

   The actual chart and group identities turn affine concentration into agreement of finite labels and a sublinear center-height error. The sampling and concentration assumptions are supplied by the preceding proved bridges.

   theorem basepoint_affine_labels_of_sampling
       (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)
       (X : I → H) (S : Finset (FreeMagma I)) (β : WordBasisSelections X S)
       {R R' t : ℝ} (hR : 0 < R) (hR' : 0 < R') (ht : 0 < t)
       (r : ℕ → ℝ) (hr : ∀ n, 1 ≤ r n) (htr : ∀ᶠ n in atTop, 1 ≤ t * r n)
   …

   Mentions: OAI.PolycyclicRecognition.WordBasisSelections