OAI/NumberTheory/DukePrimeDegree/Dynamics/TransferredVelocity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Changing coordinates in the actual velocity space

Distances may be measured in any finite-dimensional real model of the matrix space. This allows the subsequent measurable projection argument to use Euclidean coordinates while the power estimates use an operator norm. Every subspace here remains the actual stabilizer velocity space.

  1. theorem OAI.DukePrimeDegree.lowerSemicontinuous_subspace_distance line 21
  2. def OAI.DukePrimeDegree.transferredVelocitySpace line 50
  3. theorem OAI.DukePrimeDegree.isClosed_transferredVelocity_graph line 55
  4. theorem OAI.DukePrimeDegree.lowerSemicontinuous_transferredVelocity_distance line 63
  5. theorem OAI.DukePrimeDegree.measurable_kernel_transferredVelocity_distance line 73