SequenceConeIdealFlowTiling.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Strict-width tilings on the actual profile scales

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_strict_width_sequence_tiling_with_anchors line 31

Source documentation

Actual flow tilings along any strictly increasing profile scale sequence, with the same threshold, cardinality and reverse-anchor estimates.

theorem exists_strict_width_sequence_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 < δ → δ ≤ δ₀ →
      ∀ (scale : ℕ → ℝ), StrictMono scale → Tendsto scale atTop atTop →
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput