CartanNeighborRowBasis.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed maximizing bases for affine neighboring rows

def OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.fixedBasis line 48
Source documentation
Replace the row's varying bases by the fixed maximizing cell basis. The original samples, profiles, law and supported affine pair are preserved.
```
def AffineNeighborRow.fixedBasis
    (hcell : IsCompact cell) (hne : cell.Nonempty)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW cell) βcell.val)
    (hδ : 0 ≤ δ) (hs : ∀ n, 0 ≤ D.scale n) :
    AffineNeighborRow T M F hunimod eW π b₀ cell βcell X βD
      haarN chartN hchartN pivot shrink B δ S (Λ := Λ) := by
…
```
Mentions: OAI.PolycyclicRecognition.IsMaximizingColumnBasis, OAI.PolycyclicRecognition.wordListCoordinates, OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow

theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.exists_fixed_basis_radius line 82

Source documentation

The original row has a common subexponential radius in the fixed maximizing basis, without changing any of its sampled group elements.

theorem AffineNeighborRow.exists_fixed_basis_radius
    (hcell : IsCompact cell) (hne : cell.Nonempty)
    (hβ : IsMaximizingColumnBasis (wordListCoordinates M.letter M.wordList b₀)
      (M.boxCost T hunimod eW cell) βcell.val)
    (hδ : 0 ≤ δ) (hs : ∀ n, 0 ≤ D.scale n) :
    ∃ R : ℕ → ℝ, (∀ n, 0 ≤ R n) ∧ HasSubexponentialUpperBoundSeq D.scale R ∧
      (∀ n, D.base n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv)
        ((fun w => (1 + δ) • w) '' cell) βcell (D.scale n) (R n)) ∧
      (∀ n, D.step n ∈ M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv)
        ((fun w => (1 + δ) • w) '' cell) βcell (D.scale n) (R n)) := by
…

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