Maximal-divisor trace covers after inversion pairing

This module applies the abstract involution estimate to every maximal cyclic subgroup in the low-order cover. The resulting inequality is kept division-free:

2 * |trace values| ≤ (bound + 1) * |maximal divisors|.

def BGS.Markoff.maximalDivisorTraceCover {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] (trace : G → T) (bound : ℕ) : Finset T

The trace values covered by cyclic elements whose orders divide a maximal divisor below the bound.

Equations

• One or more equations did not get rendered due to their size.

theorem BGS.Markoff.boundedOrderTraceSet_subset_maximalDivisorTraceCover {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] (trace : G → T) (bound : ℕ) : boundedOrderTraceSet trace bound ⊆ maximalDivisorTraceCover trace bound

theorem BGS.Markoff.two_mul_maximalDivisorTraceCover_card_le {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) (htraceInv : ∀ (x : G), trace x⁻¹ = trace x) : 2 * (maximalDivisorTraceCover trace bound).card ≤ (bound + 1) * (NumberTheory.maximalDivisorsBelow (Fintype.card G) bound).card

theorem BGS.Markoff.two_mul_boundedOrderTraceSet_card_le_maximalDivisors {G : Type u_1} {T : Type u_2} [Group G] [Fintype G] [DecidableEq T] [IsCyclic G] (trace : G → T) (bound : ℕ) (htraceInv : ∀ (x : G), trace x⁻¹ = trace x) : 2 * (boundedOrderTraceSet trace bound).card ≤ (bound + 1) * (NumberTheory.maximalDivisorsBelow (Fintype.card G) bound).card

theorem BGS.Markoff.splitTorusTrace_inv (F : Type u_1) [Field F] (x : Fˣ) : splitTorusTrace x⁻¹ = splitTorusTrace x

theorem BGS.Markoff.quadraticNormOneTrace_inv (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(quadraticNormOneTorus p)) : quadraticNormOneTrace p x⁻¹ = quadraticNormOneTrace p x