CartanGroupBoxes.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual group boxes for the Cartan word model

The finite Cartan construction supplies the bases, bracket bounds, nilpotence and support exponents used here. The only external group facts are the two explicit published exponential inputs. In particular no box multiplication or volume estimate is an assumption.

def OAI.PolycyclicRecognition.CartanWordModel.boxBasis line 29
Source documentation
The actual scaled word basis, selected before taking its exponential image.
```
def boxBasis (E : Set W) (β : M.Bases) (r : ℝ) :
    Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H) :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal
def OAI.PolycyclicRecognition.CartanWordModel.groupBox line 35
Source documentation
A Cartan group box is the exponential image of its scaled coordinate cube.
```
def groupBox {G : Type*} (Exp : cartanRootIdeal H → G)
    (E : Set W) (β : M.Bases) (r R : ℝ) : Set G :=
…
```
Mentions: OAI.PolycyclicRecognition.cartanRootIdeal

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_groupBox_product_bound line 49

Source documentation

A uniform product estimate for the actual Cartan boxes. No assumptions about compactness or convexity of the template are needed for this part.

theorem exists_groupBox_product_bound
    (dynkin : NilpotentDynkinExpansionInput EN N)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ r : ℝ, 0 ≤ r → ∀ n : ℕ, ∀ R : ℝ, 0 ≤ R → ∀ g : Fin n → N,
      (∀ i, g i ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R) →
      (List.ofFn g).prod ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r
        (C * (1 + (n : ℝ)) ^ M.bound * (1 + R) ^ M.bound) := by
…

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

theorem OAI.PolycyclicRecognition.CartanWordModel.groupBox_inv_mem line 66

Source documentation

Inversion requires no extra group input beyond the intrinsic exponential.

theorem groupBox_inv_mem (E : Set W) (β : M.Bases) (r R : ℝ) {g : N}
    (hg : g ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R) :
    g⁻¹ ∈ M.groupBox T hunimod eW (Exp ∘ eN) E β r R :=
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_groupBox_haar_volume line 75

Source documentation

Exact Haar volume in a maximizing actual word basis. All scaling and support factors have been derived from the Cartan model.

theorem exists_groupBox_haar_volume
    (haarInput : NilpotentExponentialHaarInput EN N)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ μ : Measure N, μ.IsHaarMeasure ∧
      ∀ (E : Set W) (β : M.Bases),
      columnBasisWeight (M.boxCost T hunimod eW E) β.val =
        (M.supportIn T hunimod eW).templateSupport E →
      ∀ (r R : ℝ), 0 ≤ R →
        μ (M.groupBox T hunimod eW (Exp ∘ eN) E β r R) =
          ENNReal.ofReal |(columnBasisMatrix (wordListCoordinates M.letter M.wordList b₀)
            β.val).det| *
          ENNReal.ofReal (Real.exp (r * (M.supportIn T hunimod eW).templateSupport E)) *
…

Mentions: OAI.PolycyclicRecognition.NilpotentExponentialHaarInput, OAI.PolycyclicRecognition.cartanRootIdeal, OAI.PolycyclicRecognition.columnBasisWeight, OAI.PolycyclicRecognition.columnBasisMatrix, OAI.PolycyclicRecognition.wordListCoordinates

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_groupBox_haar_bounds line 100

Source documentation

Uniform two-sided Haar estimates for all maximizing group boxes.

theorem exists_groupBox_haar_bounds
    (haarInput : NilpotentExponentialHaarInput EN N)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ (μ : Measure N) (c C : ℝ), μ.IsHaarMeasure ∧ 0 < c ∧ 0 < C ∧
      ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      ∀ (r R : ℝ), 0 ≤ R →
        ENNReal.ofReal c *
          ENNReal.ofReal (Real.exp (r * (M.supportIn T hunimod eW).templateSupport E)) *
          ENNReal.ofReal (2 * R) ^ finrank ℝ (cartanRootIdeal H) ≤
            μ (M.groupBox T hunimod eW (Exp ∘ eN) E β r R) ∧
…

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