OAI/GroupTheory/PolycyclicRecognition/Geometry/ConeIdealFlowTiling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAutomorphism line 27
2. theorem OAI.PolycyclicRecognition.CartanWordModel.coneIdealLetterAutomorphism_apply_exp line 31
3. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_coneIdealLetterAutomorphism_threshold line 41

   Source documentation

   The smallness threshold comes from the positive mixed-word widths. No image inclusion is assumed for the automorphism used in the tiling.

   theorem exists_coneIdealLetterAutomorphism_threshold
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (s : Fin M.letterCount → ℝ) (hs : ∀ i, 0 ≤ s i)
       (hpos : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → 0 < s i)
       (β : M.ConeIdealBases C) (hβ : M.IsMaximizingConeIdealBasis C b₀ s β)
       (i : Fin M.letterCount) (hi : s i = 0)
       {a b U : ℝ} (ha : 0 ≤ a) (hab : a < b) (hU : 0 < U) :
       ∃ δ₀ : ℝ, 0 < δ₀ ∧ ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
         ∀ t ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
         (∀ᶠ r in atTop, |t r| ≤ Real.exp ((U * δ + ε r) * r)) →
         ∀ᶠ r in atTop,
           (M.coneIdealLetterAutomorphism C e Exp hExp hbij chart hchart dynkin i (t r)) ''
   …

4. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_strict_width_coneIdeal_tiling line 84

   Source documentation

   Strict width gives measurable tilings for the actual integrated letter flow, with the exact exponential cardinality bound. The small-box inclusion is derived from the nilpotent flow estimate.

   theorem exists_strict_width_coneIdeal_tiling
       (haar : NilpotentExponentialHaarInput E G)
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (s : Fin M.letterCount → ℝ) (hs : ∀ i, 0 ≤ s i)
       (hpos : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → 0 < s i)
       (β : M.ConeIdealBases C) (hβ : M.IsMaximizingConeIdealBasis C b₀ s β)
       (i : Fin M.letterCount) (hi : s i = 0)
       {a b U : ℝ} (ha : 0 ≤ a) (hab : a < b) (hU : 0 < U) :
       ∃ (μ : Measure G) (hbij : Function.Bijective Exp) (R δ₀ : ℝ),
         μ.IsHaarMeasure ∧ 0 < R ∧ 0 < δ₀ ∧
         ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
         ∀ t ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput

5. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_strict_width_tiling_with_anchors line 127

   Source documentation

   The same tiling also bounds every anchor after conjugating back by the inside-letter flow. Both strict width gaps use one positive threshold.

   theorem exists_strict_width_tiling_with_anchors
       (haar : NilpotentExponentialHaarInput E G)
       (b₀ : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
       (s : Fin M.letterCount → ℝ) (hs : ∀ i, 0 ≤ s i)
       (hpos : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∉ C → 0 < s i)
       (β : M.ConeIdealBases C) (hβ : M.IsMaximizingConeIdealBasis C b₀ s β)
       (i : Fin M.letterCount) (hi : s i = 0)
       {a b c U : ℝ} (ha : 0 ≤ a) (hab : a < b) (hbc : b < c) (hU : 0 < U) :
       ∃ (μ : Measure G) (hbij : Function.Bijective Exp) (R δ₀ : ℝ),
         μ.IsHaarMeasure ∧ 0 < R ∧ 0 < δ₀ ∧
         ∀ δ : ℝ, 0 < δ → δ ≤ δ₀ →
         ∀ t ε : ℝ → ℝ, Tendsto ε atTop (𝓝 0) →
   …

   Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput