OAI/NumberTheory/DukePrimeDegree/Geometry/UpperRootUniformContraction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform contraction of bounded upper-root boxes

Strictly contracting root weights shrink every bounded root cube into any prescribed identity neighborhood, uniformly over the cube. This is the geometric control used by the unstable conditional entropy argument.

  1. lemma OAI.DukePrimeDegree.mem_upperRootCube_iff_size_lt line 20
  2. theorem OAI.DukePrimeDegree.upperRootCube_uniform_contraction line 25