Documentation

ISAR.HolonomicInstances

Concrete holonomic certificates (Python self-test parity) #

Real.exp #

source
theorem ISAR.exp_holonomic :
satisfiesODE (orderOneCert (-1) 1 ⋯) Real.exp
source
theorem ISAR.exp_multiplicative :
satisfiesOrderOneMultiplicative 1 Real.exp
source
theorem ISAR.exp_differentiable :
Differentiable ℝ Real.exp
source
theorem ISAR.exp_isHolonomic :
IsHolonomic Real.exp

Gaussian exp(-x²) #

source
noncomputable def ISAR.gaussian :
ℝ → ℝ
Equations
Instances For
    source
    theorem ISAR.hasDerivAt_gaussian (x : ℝ) :
    HasDerivAt gaussian (gaussian x * -(2 * x)) x
    source
    theorem ISAR.deriv_gaussian (x : ℝ) :
    deriv gaussian x = -(2 * x) * gaussian x
    source
    theorem ISAR.gaussian_differentiable :
    Differentiable ℝ gaussian
    source
    theorem ISAR.gaussian_holonomic :
    satisfiesODE (orderOneCert (Polynomial.C 2 * Polynomial.X) 1 ⋯) gaussian
    source
    theorem ISAR.gaussian_multiplicative :
    satisfiesOrderOneMultiplicative (-(Polynomial.C 2 * Polynomial.X)) gaussian
    source
    theorem ISAR.gaussian_isHolonomic :
    IsHolonomic gaussian
    source
    theorem ISAR.deriv_deriv_gaussian (x : ℝ) :
    deriv (deriv gaussian) x = (-2 + 4 * x ^ 2) * gaussian x

    Second derivative of the gaussian, used by sum/product residuals.

    Product exp * gaussian #

    source
    theorem ISAR.exp_mul_gaussian_holonomic :
    satisfiesODE (orderOneCert (-(1 + -(Polynomial.C 2 * Polynomial.X))) 1 ⋯) (Real.exp * gaussian)
    source
    theorem ISAR.exp_mul_gaussian_isHolonomic :
    IsHolonomic (Real.exp * gaussian)
    source
    theorem ISAR.exp_mul_gaussian_order_bound :
    (orderOneCert (-(1 + -(Polynomial.C 2 * Polynomial.X))) 1 ⋯).order ≤ 1 * 1

    Sum (constant-rate + variable-rate) #

    source
    theorem ISAR.exp_add_exp_holonomic :
    satisfiesODE (orderTwoCert (Polynomial.C (1 * 1)) (Polynomial.C (-(1 + 1))) 1 ⋯) (Real.exp + Real.exp)
    source
    theorem ISAR.exp_add_exp_isHolonomic :
    IsHolonomic (Real.exp + Real.exp)
    source
    theorem ISAR.one_add_two_X_ne :
    1 + Polynomial.C 2 * Polynomial.X ≠ 0
    source
    theorem ISAR.exp_add_gaussian_holonomic :
    satisfiesODE (orderTwoCert (Polynomial.C 2 - Polynomial.C 2 * Polynomial.X - Polynomial.C 4 * Polynomial.X ^ 2) (Polynomial.C (-3) + Polynomial.C 4 * Polynomial.X ^ 2) (1 + Polynomial.C 2 * Polynomial.X) one_add_two_X_ne) (Real.exp + gaussian)

    Python TEST 4 sum residual: exp + exp(-x²).

    source
    theorem ISAR.exp_add_gaussian_isHolonomic :
    IsHolonomic (Real.exp + gaussian)

    Double-integral chain #

    source
    noncomputable def ISAR.gaussianCert :
    HolonomicCertificate
    Equations
    Instances For
      source
      noncomputable def ISAR.gaussianDoubleIntegralCert :
      HolonomicCertificate
      Equations
      Instances For
        source
        theorem ISAR.gaussian_double_integral_closure (H : ℝ → ℝ) (hH : deriv (deriv H) = gaussian) :
        satisfiesODE gaussianDoubleIntegralCert H
        source
        theorem ISAR.gaussianDoubleIntegralCert_order :
        gaussianDoubleIntegralCert.order = 3

        sin(x²) #

        source
        noncomputable def ISAR.fresnelSin :
        ℝ → ℝ
        Equations
        Instances For
          source
          theorem ISAR.hasDerivAt_fresnelSin (x : ℝ) :
          HasDerivAt fresnelSin (Real.cos (x ^ 2) * (2 * x)) x
          source
          theorem ISAR.deriv_fresnelSin (x : ℝ) :
          deriv fresnelSin x = 2 * x * Real.cos (x ^ 2)
          source
          theorem ISAR.fresnelSin_differentiable :
          Differentiable ℝ fresnelSin
          source
          theorem ISAR.X_ne_zero :
          Polynomial.X ≠ 0
          source
          theorem ISAR.hasDerivAt_deriv_fresnelSin (x : ℝ) :
          HasDerivAt (deriv fresnelSin) (2 * Real.cos (x ^ 2) + 2 * x * (-Real.sin (x ^ 2) * (2 * x))) x
          source
          theorem ISAR.deriv_deriv_fresnelSin (x : ℝ) :
          deriv (deriv fresnelSin) x = 2 * Real.cos (x ^ 2) - 4 * x ^ 2 * Real.sin (x ^ 2)
          source
          theorem ISAR.fresnelSin_holonomic :
          satisfiesODE (orderTwoCert (Polynomial.C 4 * Polynomial.X ^ 3) (-1) Polynomial.X X_ne_zero) fresnelSin
          source
          theorem ISAR.fresnelSin_isHolonomic :
          IsHolonomic fresnelSin

          Mixed product sin(x²)·exp(-x²) (Python TEST 4b) #

          source
          theorem ISAR.fresnel_gaussian_tensor_bound :
          (orderTwoCert (Polynomial.C 8 * Polynomial.X ^ 3) (Polynomial.C 4 * Polynomial.X ^ 2 - 1) Polynomial.X X_ne_zero).order = 2 * 1
          source
          theorem ISAR.fresnelSin_mul_gaussian_factors_holonomic :
          IsHolonomic fresnelSin ∧ IsHolonomic gaussian
          source
          theorem ISAR.deriv_fresnel_mul_gaussian (x : ℝ) :
          deriv (fresnelSin * gaussian) x = 2 * x * Real.cos (x ^ 2) * gaussian x + Real.sin (x ^ 2) * (-(2 * x) * gaussian x)

          First derivative of the mixed product.

          source
          theorem ISAR.deriv_deriv_fresnel_mul_gaussian (x : ℝ) :
          deriv (deriv (fresnelSin * gaussian)) x = (2 * Real.cos (x ^ 2) - 4 * x ^ 2 * Real.sin (x ^ 2)) * gaussian x + 2 * x * Real.cos (x ^ 2) * (-(2 * x) * gaussian x) + (2 * x * Real.cos (x ^ 2) * (-(2 * x) * gaussian x) + Real.sin (x ^ 2) * ((-2 + 4 * x ^ 2) * gaussian x))

          Second derivative of the mixed product via product rule on the first derivative.

          source
          theorem ISAR.fresnelSin_mul_gaussian_holonomic :
          satisfiesODE (orderTwoCert (Polynomial.C 8 * Polynomial.X ^ 3) (Polynomial.C 4 * Polynomial.X ^ 2 - 1) Polynomial.X X_ne_zero) (fresnelSin * gaussian)

          Python TEST 4b: 8x³ h + (4x²-1) h' + x h'' = 0.

          source
          theorem ISAR.fresnelSin_mul_gaussian_isHolonomic :
          IsHolonomic (fresnelSin * gaussian)