OAI/NumberTheory/DukePrimeDegree/Geometry/QuotientLogProper.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Compact logarithmic balls and a tempered exhaustion

Logarithmic matrix-length sublevels are compact. Their quotient images control closed logarithmic-distance balls. A rescaled distance from one fixed point then gives a proper measurable natural height with sublinear growth under a measure-preserving right translation.

  1. theorem OAI.DukePrimeDegree.isCompact_matrixLogLength_sublevel line 20
  2. theorem OAI.DukePrimeDegree.isCompact_quotientLogDistance_sublevel line 31
  3. theorem OAI.DukePrimeDegree.exists_compact_height_bounded_step line 42

    Source documentation

    A proper height with two-sided bounded increments under the fixed right translation.

    theorem exists_compact_height_bounded_step {n : ℕ} (a : G n) :
    ∃ H : X n → ℕ, Measurable H ∧ (∀ m, IsCompact {x | H x ≤ m}) ∧
      ∀ x, H (rightAction x a) ≤ H x+1 ∧ H x ≤ H (rightAction x a)+1 := by
…
  4. theorem OAI.DukePrimeDegree.exists_tempered_compact_exhaustion line 83