Documentation

LeanCert.Examples.Calculus

Calculus Examples #

This file demonstrates automatic differentiation and derivative bounds using LeanCert.

Verified AD Examples #

The evalDual_val_correct theorem is FULLY PROVED for the supported expression subset {const, var, add, mul, neg, sin, cos}. This demonstrates verified forward-mode automatic differentiation with interval bounds.

Supported expressions for AD #

source
def LeanCert.Examples.Calculus.exprXSquared :
Core.Expr

The expression x²

Equations
Instances For
    source
    def LeanCert.Examples.Calculus.exprXSquared_supported :
    Core.ExprSupported exprXSquared

    Proof that x² is in the supported subset

    Equations
    Instances For
      source
      def LeanCert.Examples.Calculus.exprXCubed :
      Core.Expr

      The expression x³ = x * x * x

      Equations
      Instances For
        source
        def LeanCert.Examples.Calculus.exprXCubed_supported :
        Core.ExprSupported exprXCubed

        Proof that x³ is supported

        Equations
        Instances For
          source
          def LeanCert.Examples.Calculus.exprSinCos :
          Core.Expr

          The expression sin(x) * cos(x)

          Equations
          Instances For
            source
            def LeanCert.Examples.Calculus.exprSinCos_supported :
            Core.ExprSupported exprSinCos

            Proof that sin(x)*cos(x) is supported

            Equations
            Instances For

              Interval environments for AD #

              source
              def LeanCert.Examples.Calculus.I01 :
              Core.IntervalRat

              Unit interval [0, 1]

              Equations
              Instances For
                source
                def LeanCert.Examples.Calculus.dualEnv01 :
                Engine.DualEnv

                Create a dual environment for differentiating with respect to x

                Equations
                Instances For

                  Verified value computation #

                  source
                  theorem LeanCert.Examples.Calculus.xSquared_dual_val_correct (x : ℝ) (hx : x ∈ I01) :
                  Core.Expr.eval (fun (x_1 : ℕ) => x) exprXSquared ∈ (Engine.evalDual exprXSquared dualEnv01).val

                  Verified: the value component of dual evaluation is correct. For any x ∈ [0,1], the value of x² lies in the computed interval. This theorem has NO SORRY.

                  source
                  theorem LeanCert.Examples.Calculus.xCubed_dual_val_correct (x : ℝ) (hx : x ∈ I01) :
                  Core.Expr.eval (fun (x_1 : ℕ) => x) exprXCubed ∈ (Engine.evalDual exprXCubed dualEnv01).val

                  Verified: the value component for x³ is correct

                  source
                  theorem LeanCert.Examples.Calculus.sinCos_dual_val_correct (x : ℝ) (hx : x ∈ I01) :
                  Core.Expr.eval (fun (x_1 : ℕ) => x) exprSinCos ∈ (Engine.evalDual exprSinCos dualEnv01).val

                  Verified: the value component for sin(x)*cos(x) is correct

                  Point evaluation examples #

                  source
                  noncomputable def LeanCert.Examples.Calculus.evalXSquaredAt (q : ℚ) :
                  Engine.DualInterval

                  Evaluate x² at a point with its derivative

                  Equations
                  Instances For

                    Verified exp support via IntervalReal #

                    With the new IntervalReal (real-endpoint intervals) and ExprSupportedExt, we can now prove facts about expressions containing exp!

                    source
                    def LeanCert.Examples.Calculus.exprExp :
                    Core.Expr

                    The expression exp(x)

                    Equations
                    Instances For
                      source
                      def LeanCert.Examples.Calculus.exprExpXSquared :
                      Core.Expr

                      The expression exp(x²)

                      Equations
                      Instances For
                        source
                        def LeanCert.Examples.Calculus.exprExp_supportedExt :
                        Engine.ExprSupportedExt exprExp

                        Proof that exp(x) is in the extended supported subset

                        Equations
                        Instances For
                          source
                          def LeanCert.Examples.Calculus.exprExpXSquared_supportedExt :
                          Engine.ExprSupportedExt exprExpXSquared

                          Proof that exp(x²) is in the extended supported subset

                          Equations
                          Instances For
                            source
                            noncomputable def LeanCert.Examples.Calculus.I01Real :
                            Core.IntervalReal

                            Real-endpoint unit interval [0, 1]

                            Equations
                            Instances For
                              source
                              theorem LeanCert.Examples.Calculus.exp_interval_correct (x : ℝ) (hx : x ∈ I01Real) :
                              Core.Expr.eval (fun (x_1 : ℕ) => x) exprExp ∈ Engine.evalIntervalReal1 exprExp I01Real

                              Verified: exp(x) on [0, 1] gives a value in the computed interval. This theorem has NO SORRY - exp is now fully supported!

                              source
                              theorem LeanCert.Examples.Calculus.expXSquared_interval_correct (x : ℝ) (hx : x ∈ I01Real) :
                              Core.Expr.eval (fun (x_1 : ℕ) => x) exprExpXSquared ∈ Engine.evalIntervalReal1 exprExpXSquared I01Real

                              Verified: exp(x²) on [0, 1] gives a value in the computed interval. This demonstrates chained exp support!