CartanBasepointBoxes.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The two strict box margins in a change of basepoint

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_basepoint_box_product_cover line 30

Source documentation

One fixed radius contains the three factors in the inverse-image cover used by the changed-center Haar law.

theorem exists_basepoint_box_product_cover
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ R : ℝ, 1 ≤ R ∧ ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ x u a : N,
      x ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r 1 →
      u ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r 1 →
      a ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r 1 →
      x⁻¹ * u⁻¹ * a ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R := by
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_small_height_two_scale_inclusions line 61

Source documentation

A fixed small height fraction preserves both strict scale margins. The logarithmic bound and the larger radius may be any subexponential sequences; the permitted height fraction is chosen before those sequences.

theorem exists_small_height_two_scale_inclusions
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    {E : Set W} (hE : IsCompact E) (hne : E.Nonempty) (β : M.Bases)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW E) β.val)
    {lo α βscale : ℝ} (hlo : 0 < lo)
    (hcost : ∀ w : M.wordList, lo ≤ M.boxCost T hunimod eW E w)
    (hα : 0 < α) (hα1 : α < 1) (hβscale : 1 < βscale) :
    ∃ η : ℝ, 0 < η ∧ ∀ scale RH R : ℕ → ℝ,
      Tendsto scale atTop atTop → (∀ n, 0 ≤ RH n) → (∀ n, 0 ≤ R n) →
      HasSubexponentialUpperBoundSeq scale RH → HasSubexponentialUpperBoundSeq scale R →
      ∀ᶠ n in atTop, ∀ h : H,
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.HasSubexponentialUpperBoundSeq