CartanMixedScaleBoxes.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The exact box inclusions needed for adjacent-scale comparisons

theorem OAI.PolycyclicRecognition.CartanWordModel.groupBox_subset_of_exponent_le line 22

Source documentation

Pointwise comparison of actual exponent widths gives inclusion of exponential boxes, without an additional geometric assumption.

theorem groupBox_subset_of_exponent_le
    (E E' : Set W) (β : M.Bases) (r t R : ℝ)
    (h : ∀ w : M.wordList, r * M.boxCost T hunimod eW E w ≤
      t * M.boxCost T hunimod eW E' w) :
    M.groupBox T hunimod eW Exp E β r R ⊆
      M.groupBox T hunimod eW Exp E' β t R := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.groupBox_mono_scale line 35

theorem OAI.PolycyclicRecognition.CartanWordModel.groupBox_scale_le_enlargement line 45

Source documentation

Every nearby larger scale fits inside the fixed strict enlargement at the smaller scale. The coordinate radius is unchanged.

theorem groupBox_scale_le_enlargement
    [FiniteDimensional ℝ W] {E : Set W} (hE : IsCompact E) (hne : E.Nonempty)
    (hcost : ∀ w : M.wordList, 0 ≤ M.boxCost T hunimod eW E w)
    (β : M.Bases) {r t δ R : ℝ} (hδ : 0 ≤ δ) (hrt : t ≤ (1 + δ) * r) :
    M.groupBox T hunimod eW Exp E β t R ⊆
      M.groupBox T hunimod eW Exp ((fun w => (1 + δ) • w) '' E) β r R := by
…

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_mixed_scale_box_difference_cover line 67

Source documentation

One radius covers the differences of a smaller-scale sample and a larger-scale sample, uniformly in both scales.

theorem exists_mixed_scale_box_difference_cover
    (eN : cartanRootIdeal H ≃ₗ⁅ℝ⁆ GroupLieAlgebra (𝓘(ℝ, EN)) N)
    (ExpN : GroupLieAlgebra (𝓘(ℝ, EN)) N → N) (hExp : IsGroupExponential ExpN)
    (dynkin : NilpotentDynkinExpansionInput EN N)
    (b₀ : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H)) :
    ∃ D : ℝ, 1 ≤ D ∧ ∀ (E : Set W) (β : M.Bases),
      IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
        (M.boxCost T hunimod eW E) β.val →
      (∀ w : M.wordList, 0 ≤ M.boxCost T hunimod eW E w) →
      ∀ r t : ℝ, 0 ≤ t → r ≤ t →
      ∀ x ∈ M.groupBox T hunimod eW (ExpN ∘ eN) E β r 1,
      ∀ y ∈ M.groupBox T hunimod eW (ExpN ∘ eN) E β t 1,
…

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