Documentation

LeanCert.Core.TrigReduction

Shared Trigonometric Range Reduction #

Common rational π bounds and interval-shifting proofs used by IntervalRat and Taylor-model trigonometric evaluators.

Rational approximations of π and 2π #

source
def LeanCert.Core.TrigReduction.piRatLo :
ℚ

Lower bound for π: 314159265/100000000 < π

Equations
Instances For
    source
    def LeanCert.Core.TrigReduction.piRatHi :
    ℚ

    Upper bound for π: π < 355/113

    Equations
    Instances For
      source
      def LeanCert.Core.TrigReduction.twoPiRatLo :
      ℚ

      Lower bound for 2π

      Equations
      Instances For
        source
        def LeanCert.Core.TrigReduction.twoPiRatHi :
        ℚ

        Upper bound for 2π

        Equations
        Instances For
          source
          theorem LeanCert.Core.TrigReduction.piRatLo_lt_pi :
          ↑piRatLo < Real.pi

          piRatLo < π, proved from Mathlib's decimal π bounds.

          source
          theorem LeanCert.Core.TrigReduction.pi_lt_piRatHi :
          Real.pi < ↑piRatHi

          π < piRatHi, proved from Mathlib's decimal π bounds.

          source
          theorem LeanCert.Core.TrigReduction.twoPiRatLo_lt_two_pi :
          ↑twoPiRatLo < 2 * Real.pi

          twoPiRatLo < 2π

          source
          theorem LeanCert.Core.TrigReduction.two_pi_lt_twoPiRatHi :
          2 * Real.pi < ↑twoPiRatHi

          2π < twoPiRatHi

          source
          theorem LeanCert.Core.TrigReduction.twoPiRatLo_le_twoPiRatHi :
          twoPiRatLo ≤ twoPiRatHi

          twoPiRatLo ≤ twoPiRatHi

          Range reduction #

          source
          def LeanCert.Core.TrigReduction.computeShiftK (I : IntervalRat) :
          ℤ

          Compute the shift amount k such that I.midpoint - k * 2π is approximately in [-π, π].

          Equations
          Instances For
            source
            def LeanCert.Core.TrigReduction.shiftInterval (I : IntervalRat) (k : ℤ) :
            IntervalRat

            Shift an interval by subtracting k * 2π using rational bounds.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def LeanCert.Core.TrigReduction.reduceToMainPeriod (I : IntervalRat) :
              IntervalRat × ℤ

              Reduce interval to be approximately in [-π, π] by subtracting multiples of 2π.

              Equations
              Instances For

                Correctness of range reduction #

                source
                theorem LeanCert.Core.TrigReduction.mem_shiftInterval_of_mem {x : ℝ} {I : IntervalRat} {k : ℤ} (hx : x ∈ I) :
                x - 2 * Real.pi * ↑k ∈ shiftInterval I k

                If x ∈ I, then x - 2πk ∈ shiftInterval I k.

                source
                theorem LeanCert.Core.TrigReduction.mem_reduceToMainPeriod_of_mem {x : ℝ} {I : IntervalRat} (hx : x ∈ I) :
                x - 2 * Real.pi * ↑(reduceToMainPeriod I).2 ∈ (reduceToMainPeriod I).1

                Convenience form: if x ∈ I, then x - 2πk ∈ (reduceToMainPeriod I).1.