OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborRowChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.gluedProfile_chart line 51

   Source documentation

   At scales at least one, the glued original profile is precisely the chart profile required by the polar source comparison.

   theorem AffineNeighborRow.gluedProfile_chart
       (hs : ∀ n, 1 ≤ D.scale n) :
       (∀ n, Measurable (profile n)) ∧
       (∀ n q, q ∈ (fun v => v * D.base n) ''
           M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) cell βcell (D.scale n) 1 ∪
         (fun v => v * D.base n * D.step n) ''
           M.groupBox T hunimod eW (F.ExpN ∘ F.N.equiv) cell βcell (D.scale n) 1 → ∀ z,
         (profile n q).val z = rescaledMapProfile
           (fun g => (π ((D.pair n).val.1 g)).toAdd) (D.center n) (F.inclusionN q)
           (max (Real.log (D.scale n)) 0)
           (F.profileChart (exponentialRescaleBasis
             (WordBasisSelections.basis X (boundedBracketWords d) βD)
   …

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

2. theorem OAI.PolycyclicRecognition.CartanWordModel.AffineNeighborRow.common_affine_on line 93

   Source documentation

   Restrict two identically labelled affine profiles to the common inner height domain, retaining their respective original offsets.

   theorem AffineNeighborRow.common_affine_on
       {V : Set W} (hV : V ⊆ (fun w => (1 - shrink * δ) • w) '' interior cell)
       (hlabels : D.label₂ = D.label₁) :
       ∀ (s : Bool) z,
         eW (heightProjection T.character
           ((WordBasisSelections.basis X (boundedBracketWords d) βD).equivFun.symm z :
             GroupLieAlgebra (𝓘(ℝ, EG)) G)) ∈ V →
         (if s then D.point.2 else D.point.1).val z = D.label₁.val
           (eW (heightProjection T.character
             ((WordBasisSelections.basis X (boundedBracketWords d) βD).equivFun.symm z :
               GroupLieAlgebra (𝓘(ℝ, EG)) G))) + (if s then D.offset₂ else D.offset₁) := by
   …

   Mentions: OAI.PolycyclicRecognition.heightProjection, OAI.PolycyclicRecognition.WordBasisSelections.basis, OAI.PolycyclicRecognition.boundedBracketWords