ConeAdaptedPathBasis.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One adapted basis for path lifting and ideal bridge absorption

The maximizing ambient word basis and the ideal/quotient basis describe exactly the same boxes. Keeping this identification prevents a change of coordinates from introducing an extra exponential error in the bridge.

theorem OAI.PolycyclicRecognition.norm_basis_equivFun_reindex line 21
Source documentation
Reindexing a finite basis preserves its coordinate supremum norm.
```
theorem norm_basis_equivFun_reindex (b : Basis I ℝ V) (e : I ≃ J) (v : V) :
    ‖(b.reindex e).equivFun v‖ = ‖b.equivFun v‖ := by
…
```
theorem OAI.PolycyclicRecognition.exponentialCoordinateBox_reindex line 35
Source documentation
Consequently the actual exponential coordinate boxes are unchanged.
```
theorem exponentialCoordinateBox_reindex {N : Type*} (Exp : V → N)
    (b : Basis I ℝ V) (e : I ≃ J) (R : ℝ) :
    exponentialCoordinateBox Exp (b.reindex e) R = exponentialCoordinateBox Exp b R := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialCoordinateBox

theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cone_adapted_path_basis line 53

Source documentation

The same ideal-maximizing choice supplies an ambient path box, an exact ideal/quotient coordinate identification and a uniform bracket bound.

theorem exists_cone_adapted_path_basis
    (bN : Basis (Fin (finrank ℝ (cartanRootIdeal H))) ℝ (cartanRootIdeal H))
    (bI : Basis (Fin (finrank ℝ (M.coneWordIdeal C))) ℝ (M.coneWordIdeal C))
    (E : Set W)
    (hs : ∀ i, 0 ≤ (M.supportIn T hunimod eW).weightSupport E i)
    (hzero : ∀ i, (M.weight i : H →ₗ[ℝ] ℝ) ∈ C →
      (M.supportIn T hunimod eW).weightSupport E i = 0)
    (β : M.ConeIdealBases C)
    (hβ : M.IsMaximizingConeIdealBasis C bI
      ((M.supportIn T hunimod eW).weightSupport E) β) :
    ∃ (bQ : Basis (Fin (finrank ℝ (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule)))
        ℝ (cartanRootIdeal H ⧸ (M.coneWordIdeal C).toSubmodule))
…

Mentions: OAI.PolycyclicRecognition.cartanRootIdeal