OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanNeighborChainConcentration.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The original neighboring comparison along finite root chains

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.neighbor_chain_concentration line 43

    Source documentation

    The proved neighboring-sheet comparison propagates along a bounded root word. Its root index may change at each scale and each edge.

    theorem neighbor_chain_concentration
    (Z : Set (Fin (finrank ℝ H) → ℝ)) [CompactSpace Z]
    (hneighbor : ∀ row : NeighborSamplingRow T M F hunimod eW π bN cell β X βD
      haarN chartN hchartN pivot B δ Profiles (Λ := Λ),
…

    Mentions: OAI.PolycyclicRecognition.CartanWordModel.NeighborSamplingRow