Finite counts in normalized Markoff coordinates

This module transports the canonical two-point bound for a fixed pair of original Markoff coordinates across normalizationEquiv. It then sums that bound over a finite set of possible first and second normalized coordinates.

def BGS.Markoff.originalCoordinateOfNormalized {F : Type u} [Field F] [Invertible 3] (a : F) : F

The original coordinate whose normalized value is a.

Equations

• BGS.Markoff.originalCoordinateOfNormalized a = ⅟3 * a

noncomputable def BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinates {F : Type u} [Field F] [Fintype F] [Invertible 3] (a b : F) : Finset (NormalizedPoint F)

Normalized Markoff points with prescribed first and second coordinates, obtained by mapping the canonical original-coordinate fiber through the normalization equivalence.

Equations

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

@[simp]

theorem BGS.Markoff.mem_normalizedMarkoffPointsWithFirstTwoCoordinates_iff {F : Type u} [Field F] [Fintype F] [Invertible 3] {a b : F} {x : NormalizedPoint F} : x ∈ normalizedMarkoffPointsWithFirstTwoCoordinates a b ↔ IsNormalizedMarkoff x ∧ x.u1 = a ∧ x.u2 = b

theorem BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinates_card_eq_original {F : Type u} [Field F] [Fintype F] [Invertible 3] (a b : F) : (normalizedMarkoffPointsWithFirstTwoCoordinates a b).card = (markoffPointsWithFirstTwoCoordinates (originalCoordinateOfNormalized a) (originalCoordinateOfNormalized b)).card

Mapping through normalization preserves the exact cardinality of a fixed-coordinate fiber.

theorem BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinates_card_le_two {F : Type u} [Field F] [Fintype F] [Invertible 3] (a b : F) : (normalizedMarkoffPointsWithFirstTwoCoordinates a b).card ≤ 2

Fixing the first two normalized coordinates leaves at most two normalized Markoff points.

noncomputable def BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinatesIn {F : Type u} [Field F] [Fintype F] [Invertible 3] (S : Finset F) : Finset (NormalizedPoint F)

Normalized Markoff points whose first two coordinates both lie in S.

Equations

• BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinatesIn S = (S.product S).biUnion fun (ab : F × F) => BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinates ab.1 ab.2

@[simp]

theorem BGS.Markoff.mem_normalizedMarkoffPointsWithFirstTwoCoordinatesIn_iff {F : Type u} [Field F] [Fintype F] [Invertible 3] {S : Finset F} {x : NormalizedPoint F} : x ∈ normalizedMarkoffPointsWithFirstTwoCoordinatesIn S ↔ IsNormalizedMarkoff x ∧ x.u1 ∈ S ∧ x.u2 ∈ S

theorem BGS.Markoff.normalizedMarkoffPointsWithFirstTwoCoordinatesIn_card_le {F : Type u} [Field F] [Fintype F] [Invertible 3] (S : Finset F) : (normalizedMarkoffPointsWithFirstTwoCoordinatesIn S).card ≤ 2 * S.card ^ 2

If both of the first two normalized coordinates lie in a finite set S, there are at most 2 * |S|^2 normalized Markoff points.