Documentation

LeanPool.SumDifferenceExponent.Quantitative

A fully explicit 10⁻⁹⁹⁹ quantitative witness.

source
def SumDifferenceExponent.quantitativeScale :
ℕ

The reciprocal of the requested error tolerance.

Equations
Instances For
    source
    def SumDifferenceExponent.quantitativePower :
    ℕ

    An exponent large enough to force the logarithmic error below the tolerance.

    Equations
    Instances For
      source
      def SumDifferenceExponent.powerOfTwo (n : ℕ) :
      ℕ

      A power of two kept as a named definition in the quantitative witness.

      Equations
      Instances For
        source
        def SumDifferenceExponent.quantitativeIndex :
        ℕ

        The row parameter used for the explicit quantitative witness.

        Equations
        Instances For
          source
          @[reducible, inline]
          abbrev SumDifferenceExponent.quantitativeSet :
          Finset ℤ

          An explicit finite integer set whose growth exponent is within 10⁻⁹⁹⁹ of two.

          Equations
          Instances For
            source
            theorem SumDifferenceExponent.quantitativeScale_pos :
            0 < quantitativeScale
            source
            theorem SumDifferenceExponent.quantitativePower_pos :
            0 < quantitativePower
            source
            theorem SumDifferenceExponent.quantitativeIndex_two_le :
            2 ≤ quantitativeIndex
            source
            theorem SumDifferenceExponent.log_constant_lt_twenty_three :
            Real.log 2 + 2 * Real.log 12 < 23
            source
            theorem SumDifferenceExponent.quantitative_denominator_gt :
            ↑quantitativePower / 2 < Real.log ↑quantitativeIndex + Real.log 12
            source
            theorem SumDifferenceExponent.forty_six_div_quantitativePower_lt :
            46 / ↑quantitativePower < 10 ^ (-999)
            source
            theorem SumDifferenceExponent.exponentLower_quantitative :
            2 - 10 ^ (-999) < ColumnConstruction.exponentLower quantitativeIndex
            source
            theorem SumDifferenceExponent.quantitative_example :
            2 - 10 ^ (-999) < growthExponent quantitativeSet ∧ growthExponent quantitativeSet < 2