OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanUnitarySublinear.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Unconditional sublinearity in an actual unimodular Cartan model

The nilpotent models' Haar charts, finite BCH identities and ambient faithful representation are supplied by their proved constructions.

  1. theorem OAI.PolycyclicRecognition.cartan_unitary_cocycle_sublinear line 38
  2. theorem OAI.PolycyclicRecognition.cartan_unitary_cocycle_sublinear_distance line 57