Density exponents of dyadic Jordan data

The ranks and parity types of the nonzero constituents in a dyadic Jordan splitting determine three natural numbers used in the local density formula. This file packages exactly that finite data in TauCeti.DyadicJordanProfile, defines Cho's exponents nM, nQ, and densityExponent, and proves the identity nQ = nM + densityExponent.

The profile records a finitely supported family of constituent ranks and the subset having type I. Thus a nonzero constituent outside typeI has type II, while an empty constituent is never type I. As for an actual splitting, every constituent outside typeI has even rank. A constituent is bound when an adjacent constituent has type I, and free otherwise. The definitions also expose the three statistics used in the closed formula: the number of type-I constituents, the number of adjacent type-I pairs, and the sum of the ranks of type-II constituents.

References

• S. Cho, Group schemes and local densities of quadratic lattices in residue characteristic 2, Compositio Math. 151 (2015), Definition 2.1, Section 2.3, and Lemma 5.1.

structure TauCeti.DyadicJordanProfile : Type

The finite rank and parity data of a dyadic Jordan splitting.

The value ranks i is the rank of the constituent of scale 2 ^ i. The finset typeI consists of the scales of the type-I constituents. The containment condition enforces the convention that an empty constituent is not of type I; every nonempty constituent at a scale outside typeI is of type II, and so has even rank.

• ranks : ℕ →₀ ℕ

  The finitely supported ranks of the Jordan constituents.

• typeI : Finset ℕ

  The scales whose nonempty constituents have type I.

• typeI_subset_support : self.typeI ⊆ self.ranks.support

  A type-I constituent is nonempty.

• even_rank_of_notMem_typeI (i : ℕ) : i ∉ self.typeI → Even (self.ranks i)

  A constituent that is not of type I has even rank.

theorem TauCeti.DyadicJordanProfile.ext_iff {x y : DyadicJordanProfile} : x = y ↔ x.ranks = y.ranks ∧ x.typeI = y.typeI

theorem TauCeti.DyadicJordanProfile.ext {x y : DyadicJordanProfile} (ranks : x.ranks = y.ranks) (typeI : x.typeI = y.typeI) : x = y

def TauCeti.DyadicJordanProfile.IsBound (P : DyadicJordanProfile) (i : ℕ) : Prop

The constituent of scale 2 ^ i is bound if a constituent of an adjacent scale 2 ^ (i - 1) or 2 ^ (i + 1) has type I.

def TauCeti.DyadicJordanProfile.IsFree (P : DyadicJordanProfile) (i : ℕ) : Prop

The constituent of scale 2 ^ i is free if it is not bound, that is, both adjacent constituents have type II.

@[simp]

theorem TauCeti.DyadicJordanProfile.isBound_zero_iff (P : DyadicJordanProfile) : P.IsBound 0 ↔ 1 ∈ P.typeI

The constituent of scale 1 is bound exactly when the one of scale 2 has type I.

@[simp]

theorem TauCeti.DyadicJordanProfile.isBound_succ_iff (P : DyadicJordanProfile) (i : ℕ) : P.IsBound (i + 1) ↔ i + 2 ∈ P.typeI ∨ i ∈ P.typeI

The constituent of scale 2 ^ (i + 1) is bound exactly when one of the constituents of scales 2 ^ i and 2 ^ (i + 2) has type I.

@[simp]

theorem TauCeti.DyadicJordanProfile.isFree_iff_not_isBound (P : DyadicJordanProfile) (i : ℕ) : P.IsFree i ↔ ¬P.IsBound i

A constituent is free exactly when it is not bound.

@[instance_reducible]

instance TauCeti.DyadicJordanProfile.instDecidablePredNatIsBound (P : DyadicJordanProfile) : DecidablePred P.IsBound

@[instance_reducible]

instance TauCeti.DyadicJordanProfile.instDecidablePredNatIsFree (P : DyadicJordanProfile) : DecidablePred P.IsFree

def TauCeti.DyadicJordanProfile.typeICount (P : DyadicJordanProfile) : ℕ

The number t of type-I constituents.

theorem TauCeti.DyadicJordanProfile.typeICount_def (P : DyadicJordanProfile) : P.typeICount = P.typeI.card

The number of type-I constituents is the cardinality of the type-I scale set.

def TauCeti.DyadicJordanProfile.adjacentTypeICount (P : DyadicJordanProfile) : ℕ

The number b of adjacent pairs of type-I constituents.

theorem TauCeti.DyadicJordanProfile.adjacentTypeICount_def (P : DyadicJordanProfile) : P.adjacentTypeICount = {i ∈ P.typeI | i + 1 ∈ P.typeI}.card

The adjacent type-I count is the number of type-I scales whose successor is type I.

def TauCeti.DyadicJordanProfile.typeIIRank (P : DyadicJordanProfile) : ℕ

The number c, the sum of the ranks of the nonempty type-II constituents.

theorem TauCeti.DyadicJordanProfile.typeIIRank_def (P : DyadicJordanProfile) : P.typeIIRank = ∑ i ∈ P.ranks.support with i ∉ P.typeI, P.ranks i

The total type-II rank is the sum of the ranks at non-type-I scales in the support.

def TauCeti.DyadicJordanProfile.diagonalExponent (P : DyadicJordanProfile) : ℕ

The sum ∑ i * n_i * (n_i + 1) / 2 of the diagonal contributions d_i.

theorem TauCeti.DyadicJordanProfile.diagonalExponent_def (P : DyadicJordanProfile) : P.diagonalExponent = ∑ i ∈ P.ranks.support, i * (P.ranks i * (P.ranks i + 1) / 2)

The diagonal exponent is the weighted sum of the triangular constituent ranks.

def TauCeti.DyadicJordanProfile.distanceCrossExponent (P : DyadicJordanProfile) : ℕ

The cross term ∑_{i < j} (j - i) * n_i * n_j occurring in N_M.

theorem TauCeti.DyadicJordanProfile.distanceCrossExponent_def (P : DyadicJordanProfile) : P.distanceCrossExponent = ∑ i ∈ P.ranks.support, ∑ j ∈ P.ranks.support with i < j, (j - i) * P.ranks i * P.ranks j

The distance cross exponent is the pairwise rank product weighted by the scale gap.

def TauCeti.DyadicJordanProfile.upperCrossExponent (P : DyadicJordanProfile) : ℕ

The cross term ∑_{i < j} j * n_i * n_j occurring in N_Q.

theorem TauCeti.DyadicJordanProfile.upperCrossExponent_def (P : DyadicJordanProfile) : P.upperCrossExponent = ∑ i ∈ P.ranks.support, ∑ j ∈ P.ranks.support with i < j, j * P.ranks i * P.ranks j

The upper cross exponent weights each pairwise rank product by its larger scale index.

def TauCeti.DyadicJordanProfile.lowerCrossExponent (P : DyadicJordanProfile) : ℕ

The cross term ∑_{i < j} i * n_i * n_j occurring in Cho's formula for N.

theorem TauCeti.DyadicJordanProfile.lowerCrossExponent_def (P : DyadicJordanProfile) : P.lowerCrossExponent = ∑ i ∈ P.ranks.support, ∑ j ∈ P.ranks.support with i < j, i * P.ranks i * P.ranks j

The lower cross exponent weights each pairwise rank product by its smaller scale index.

def TauCeti.DyadicJordanProfile.nM (P : DyadicJordanProfile) : ℕ

Cho's exponent N_M attached to dyadic Jordan data.

theorem TauCeti.DyadicJordanProfile.nM_def (P : DyadicJordanProfile) : P.nM = ∑ i ∈ P.typeI, (2 * P.ranks i - 1) + P.distanceCrossExponent + 2 * P.adjacentTypeICount

Cho's exponent N_M in terms of the type-I, distance, and adjacency contributions.

def TauCeti.DyadicJordanProfile.nQ (P : DyadicJordanProfile) : ℕ

Cho's exponent N_Q attached to dyadic Jordan data.

theorem TauCeti.DyadicJordanProfile.nQ_def (P : DyadicJordanProfile) : P.nQ = ∑ i ∈ P.typeI, 2 * P.ranks i + P.upperCrossExponent + P.diagonalExponent + P.adjacentTypeICount + P.typeIIRank

Cho's exponent N_Q in terms of its constituent-rank and parity statistics.

def TauCeti.DyadicJordanProfile.densityExponent (P : DyadicJordanProfile) : ℕ

The density exponent N = N_Q - N_M attached to dyadic Jordan data.

The subtraction is placed between typeICount and adjacentTypeICount; the latter never exceeds the former. The theorem densityExponent_eq gives Cho's displayed order of terms, and nQ_sub_nM_eq_densityExponent proves that this is exactly N_Q - N_M.

theorem TauCeti.DyadicJordanProfile.densityExponent_def (P : DyadicJordanProfile) : P.densityExponent = P.typeICount - P.adjacentTypeICount + P.lowerCrossExponent + P.diagonalExponent + P.typeIIRank

Cho's density exponent in terms of the type, cross, diagonal, and adjacency statistics.

theorem TauCeti.DyadicJordanProfile.rank_pos_of_mem_typeI (P : DyadicJordanProfile) {i : ℕ} (hi : i ∈ P.typeI) : 0 < P.ranks i

A scale declared to have type I has positive rank.

theorem TauCeti.DyadicJordanProfile.adjacentTypeICount_le_typeICount (P : DyadicJordanProfile) : P.adjacentTypeICount ≤ P.typeICount

The number of adjacent type-I pairs is at most the number of type-I constituents.

theorem TauCeti.DyadicJordanProfile.densityExponent_eq (P : DyadicJordanProfile) : P.densityExponent = P.typeICount + P.lowerCrossExponent + P.diagonalExponent - P.adjacentTypeICount + P.typeIIRank

Cho's displayed expression N = t + ∑_{i < j} i n_i n_j + ∑_i d_i - b + c.

theorem TauCeti.DyadicJordanProfile.nQ_eq_nM_add_densityExponent (P : DyadicJordanProfile) : P.nQ = P.nM + P.densityExponent

Cho's exponent identity. The two deformation exponents differ by the density exponent: N_Q = N_M + N.

theorem TauCeti.DyadicJordanProfile.nQ_sub_nM_eq_densityExponent (P : DyadicJordanProfile) : P.nQ - P.nM = P.densityExponent

The density exponent is the natural-number difference N_Q - N_M.

def TauCeti.DyadicJordanProfile.empty : DyadicJordanProfile

The empty dyadic Jordan profile.

noncomputable def TauCeti.DyadicJordanProfile.unimodularTypeII (n : ℕ) (hn : Even n) : DyadicJordanProfile

A single type-II unimodular constituent of even rank n. At n = 0 this is the empty profile.

noncomputable def TauCeti.DyadicJordanProfile.unaryTypeI (i : ℕ) : DyadicJordanProfile

A unary type-I constituent at scale 2 ^ i.

noncomputable def TauCeti.DyadicJordanProfile.adjacentUnaryTypeI : DyadicJordanProfile

Two unary type-I constituents at the adjacent scales 1 and 2.

@[simp]

theorem TauCeti.DyadicJordanProfile.empty_ranks : empty.ranks = 0

The empty profile has no nonzero ranks.

@[simp]

theorem TauCeti.DyadicJordanProfile.empty_typeI : empty.typeI = ∅

The empty profile has no type-I constituents.

@[simp]

theorem TauCeti.DyadicJordanProfile.unimodularTypeII_ranks (n : ℕ) (hn : Even n) : (unimodularTypeII n hn).ranks = Finsupp.single 0 n

The unimodular type-II profile has one possibly nonzero rank at scale zero.

@[simp]

theorem TauCeti.DyadicJordanProfile.unimodularTypeII_typeI (n : ℕ) (hn : Even n) : (unimodularTypeII n hn).typeI = ∅

The unimodular type-II profile has no type-I constituents.

@[simp]

theorem TauCeti.DyadicJordanProfile.unaryTypeI_ranks (i : ℕ) : (unaryTypeI i).ranks = Finsupp.single i 1

A unary type-I profile has rank one at its given scale.

@[simp]

theorem TauCeti.DyadicJordanProfile.unaryTypeI_typeI (i : ℕ) : (unaryTypeI i).typeI = {i}

A unary type-I profile has exactly its given scale of type I.

@[simp]

theorem TauCeti.DyadicJordanProfile.adjacentUnaryTypeI_ranks : adjacentUnaryTypeI.ranks = Finsupp.single 0 1 + Finsupp.single 1 1

The adjacent unary profile has rank one at scales zero and one.

@[simp]

theorem TauCeti.DyadicJordanProfile.adjacentUnaryTypeI_typeI : adjacentUnaryTypeI.typeI = {0, 1}

The adjacent unary profile has type I at scales zero and one.

@[simp]

theorem TauCeti.DyadicJordanProfile.densityExponent_empty : empty.densityExponent = 0

The empty profile has density exponent zero.

@[simp]

theorem TauCeti.DyadicJordanProfile.densityExponent_unimodularTypeII (n : ℕ) (hn : Even n) : (unimodularTypeII n hn).densityExponent = n

A unimodular type-II constituent of even rank n has density exponent n.

@[simp]

theorem TauCeti.DyadicJordanProfile.densityExponent_unaryTypeI (i : ℕ) : (unaryTypeI i).densityExponent = i + 1

A unary type-I constituent at scale 2 ^ i has density exponent i + 1.

@[simp]

theorem TauCeti.DyadicJordanProfile.densityExponent_adjacentUnaryTypeI : adjacentUnaryTypeI.densityExponent = 2

Two adjacent unary type-I constituents at scales 1 and 2 have density exponent 2.