Documentation

LeanPool.MarkoffModP.BGS.Markoff.Core.Statements

Formal statements of the main results #

This file fixes the logical meaning of the two main theorems before their proofs are attempted. In particular, the threshold in the giant-orbit assertion may depend on epsilon, while the constant in the lower bound for every orbit is absolute.

source
def BGS.Markoff.PuncturedMarkoffTransitiveAt (p : ℕ) :
Prop

Punctured Markoff transitivity at a prime p: the Markoff group has one orbit on the nonzero solutions modulo p.

Equations
Instances For
    source
    noncomputable def BGS.Markoff.orbitComplementCard {p : ℕ} (x : PuncturedMarkoffSurface (ZMod p)) :
    ℕ

    The complement size of the orbit of x inside the punctured surface over ZMod p.

    Equations
    Instances For
      source
      def BGS.Markoff.HasGiantOrbitAt (p : ℕ) (epsilon : ℝ) :
      Prop

      At p, there is an orbit whose complement has at most p ^ epsilon points.

      Equations
      Instances For
        source
        theorem BGS.Markoff.orbitComplementCard_le_finset_of_subset {p : ℕ} [Fact (Nat.Prime p)] (x : PuncturedMarkoffSurface (ZMod p)) (bad : Finset (PuncturedMarkoffSurface (ZMod p))) (hbad : Set.univ \ puncturedGammaOrbit x ⊆ ↑bad) :
        orbitComplementCard x ≤ bad.card

        A finite set containing an orbit complement bounds that complement's cardinality.

        source
        theorem BGS.Markoff.hasGiantOrbitAt_of_complement_subset_finset (p : ℕ) (hp : Nat.Prime p) (epsilon : ℝ) (x : PuncturedMarkoffSurface (ZMod p)) (bad : Finset (PuncturedMarkoffSurface (ZMod p))) (hbad : Set.univ \ puncturedGammaOrbit x ⊆ ↑bad) (hcard : ↑bad.card ≤ (↑p).rpow epsilon) :
        HasGiantOrbitAt p epsilon

        The final giant-orbit conclusion once the complement has been put inside a counted set.

        source
        def BGS.Markoff.EveryOrbitLargeAt (p : ℕ) (c : ℝ) :
        Prop

        At p, every punctured Markoff orbit has the asserted logarithmic lower bound.

        Equations
        Instances For
          source
          def BGS.Markoff.TheoremOneStatement :
          Prop

          The exact quantifier structure of Theorem 1 in arXiv:1607.01530v1.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def BGS.Markoff.IsExceptionalPrime (p : ℕ) :
            Prop

            A prime is exceptional when strong approximation fails at that prime.

            Equations
            Instances For
              source
              noncomputable def BGS.Markoff.exceptionalPrimeCount (T : ℕ) :
              ℕ

              The number of exceptional primes at most T.

              Equations
              Instances For
                source
                def BGS.Markoff.TheoremTwoStatement :
                Prop

                The exact quantifier structure of Theorem 2 in arXiv:1607.01530v1.

                Equations
                Instances For