CartanNeighborRowProfile.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One actual profile map for both cells of an affine neighboring row

def OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.reindex line 47
Source documentation
Restricting to a cofinal subsequence keeps the original neighboring law, affine profiles and offsets.
```
def AffineNeighborRow.reindex (u : ℕ → ℕ) (hu : StrictMono u) :
    AffineNeighborRow T M F hunimod eW π b₀ cell βcell X βD
      haarN chartN hchartN pivot shrink B δ S (Λ := Λ) where
…
```
Mentions: OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow
def OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.gluedProfile line 84
Source documentation
Glue the row's two actual profiles using their agreement on overlap.
```
def AffineNeighborRow.gluedProfile (n : ℕ) : F.N.carrier → S :=
…
```

theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.gluedProfile_properties line 89

Source documentation

Gluing preserves the joint law and the actual rescaled formula on both translated cells. In particular it introduces no new profile hypothesis.

theorem AffineNeighborRow.gluedProfile_properties :
    (∀ n, Measurable (D.gluedProfile T M F hunimod eW π b₀ cell βcell X βD
      haarN chartN hchartN pivot shrink B δ S n)) ∧
    (∀ n q, q ∈ Q n ∪ (fun y => y * D.step n) '' Q n → ∀ z,
      (D.gluedProfile T M F hunimod eW π b₀ cell βcell X βD
        haarN chartN hchartN pivot shrink B δ S n q).val z =
      rescaledMapProfile (fun g => (π ((D.pair n).val.1 g)).toAdd)
        (D.center n) (F.inclusionN q) (Real.log (D.scale n))
        (fun z => ExpG ((exponentialRescaleBasis
          (WordBasisSelections.basis X (boundedBracketWords d) βD)
          (fun j => bracketWordExponent (fun _ : I => 1) (βD.val j))
          (Real.log (D.scale n))).equivFun.symm z)) z) ∧
…

Mentions: OAI.PolycyclicRecognition.rescaledMapProfile, OAI.PolycyclicRecognition.exponentialRescaleBasis, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.boundedBracketWords, OAI.PolycyclicRecognition.bracketWordExponent