Documentation

LeanCert.Core.IntervalRat.TrigReduced

Computable Range Reduction for Trigonometric Functions #

This file implements range reduction for sin and cos to improve Taylor series convergence for intervals far from 0.

Problem #

Standard Taylor series for sin/cos centered at 0 have remainder bounds of |x|^{n+1} / (n+1)!. For intervals far from 0 (e.g., [10, 11]), this remainder is huge even for moderate n.

Solution: Range Reduction #

Use the periodicity of sin/cos:

By choosing k to bring x - 2πk into [-π, π], the Taylor series converges much faster since |x - 2πk| ≤ π ≈ 3.14.

Main definitions #

Shared range-reduction API #

source
def LeanCert.Core.IntervalRat.piRatLo :
ℚ
Equations
Instances For
    source
    def LeanCert.Core.IntervalRat.piRatHi :
    ℚ
    Equations
    Instances For
      source
      def LeanCert.Core.IntervalRat.twoPiRatLo :
      ℚ
      Equations
      Instances For
        source
        def LeanCert.Core.IntervalRat.twoPiRatHi :
        ℚ
        Equations
        Instances For
          source
          def LeanCert.Core.IntervalRat.computeShiftK :
          IntervalRat → ℤ
          Equations
          Instances For
            source
            def LeanCert.Core.IntervalRat.shiftInterval :
            IntervalRat → ℤ → IntervalRat
            Equations
            Instances For
              source
              def LeanCert.Core.IntervalRat.reduceToMainPeriod :
              IntervalRat → IntervalRat × ℤ
              Equations
              Instances For
                source
                theorem LeanCert.Core.IntervalRat.piRatLo_lt_pi :
                ↑piRatLo < Real.pi
                source
                theorem LeanCert.Core.IntervalRat.pi_lt_piRatHi :
                Real.pi < ↑piRatHi
                source
                theorem LeanCert.Core.IntervalRat.twoPiRatLo_lt_two_pi :
                ↑twoPiRatLo < 2 * Real.pi
                source
                theorem LeanCert.Core.IntervalRat.two_pi_lt_twoPiRatHi :
                2 * Real.pi < ↑twoPiRatHi
                source
                theorem LeanCert.Core.IntervalRat.twoPiRatLo_le_twoPiRatHi :
                twoPiRatLo ≤ twoPiRatHi
                source
                theorem LeanCert.Core.IntervalRat.mem_shiftInterval_of_mem {x : ℝ} {I : IntervalRat} {k : ℤ} (hx : x ∈ I) :
                x - 2 * Real.pi * ↑k ∈ I.shiftInterval k

                Computable reduced evaluation #

                source
                def LeanCert.Core.IntervalRat.sinComputableReduced (I : IntervalRat) (n : ℕ := 10) :
                IntervalRat

                Computable sin evaluation with range reduction.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def LeanCert.Core.IntervalRat.cosComputableReduced (I : IntervalRat) (n : ℕ := 10) :
                  IntervalRat

                  Computable cos evaluation with range reduction.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem LeanCert.Core.IntervalRat.mem_sinComputableReduced {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ := 10) :
                    Real.sin x ∈ I.sinComputableReduced n

                    sin x ∈ sinComputableReduced I for all x ∈ I

                    source
                    theorem LeanCert.Core.IntervalRat.mem_cosComputableReduced {x : ℝ} {I : IntervalRat} (hx : x ∈ I) (n : ℕ := 10) :
                    Real.cos x ∈ I.cosComputableReduced n

                    cos x ∈ cosComputableReduced I for all x ∈ I