OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanDensityOccupation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.cartan_density_occupation_error_tendsto_zero line 30

   Source documentation

   Every fixed second-factor move changes the actual joint chart law by a vanishing amount. The first-factor sampling and deterministic suffix may vary arbitrarily through their coordinate chart and basepoint.

   theorem cartan_density_occupation_error_tendsto_zero
       (haarN : NilpotentExponentialHaarInput F.N.modelSpace F.N.carrier)
       (haarD : NilpotentExponentialHaarInput F.D.modelSpace F.D.carrier)
       (X : I → H) {k c : ℕ} (hk : lowerCentralSeries ℝ H H k = ⊥)
       (hletters : ∀ i : I, FreeMagma.of i ∈ boundedBracketWords k)
       (b₀ : Basis (Fin (finrank ℝ H)) ℝ H)
       (β : WordBasisSelections X (boundedBracketWords k))
       (hβ : IsMaximizingColumnBasis (wordListCoordinates X (boundedBracketWords k) b₀)
         (fun w => bracketWordExponent (fun _ : I => 1) w) β.val)
       (aD : DynkinCoefficients c 2)
       (hm : ∀ x y, F.ExpD (finiteDynkinPolynomial aD ![x, y]) = F.ExpD x * F.ExpD y)
       {m : ℕ} (bN : ℝ → Basis (Fin m) ℝ (cartanRootIdeal H))
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.WordBasisSelections, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.bracketWordExponent, OAI.PolycyclicRecognition.DynkinCoefficients, OAI.PolycyclicRecognition.finiteDynkinPolynomial, OAI.PolycyclicRecognition.cartanRootIdeal