►Functions
Functions
1 Real functions of one variable
2 Derivatives
3 Finite difference operators

Functions

Konrad Hinsen

Context ℝ→ℝ
uses builtins/real-numbers

1 Real functions of one variable

The sort ℝ→ℝ describes real functions of one real variable. Function application is defined by ℝ→ℝ[ℝ] : ℝ. Note that this implies that the domain of the function is the full set of real numbers, which excludes functions with singularities as well as partial functions.

It is convenient to provide basic arithmetic on functions:

  • f:ℝ→ℝ + g:ℝ→ℝ : ℝ→ℝ with
    (f + g)[x] ⇒ f[x] + g[x]  ∀ x : ℝ

  • f:ℝ→ℝ - g:ℝ→ℝ : ℝ→ℝ with
    (f - g)[x] ⇒ f[x] - g[x]  ∀ x : ℝ

  • f:ℝ→ℝ × g:ℝ→ℝ : ℝ→ℝ with
    (f × g)[x] ⇒ f[x] × g[x]  ∀ x : ℝ

  • s:ℝ × g:ℝ→ℝ : ℝ→ℝ with
    (s × g)[x] ⇒ s × g[x]  ∀ x : ℝ

We do not define division as this requires more elaborate definitions to handle the case of functions with zeros.

Function composition is defined by

f:ℝ→ℝ ○ g:ℝ→ℝ : ℝ→ℝ with
(f ○ g)[x] ⇒ f[g[x]]  ∀ x : ℝ

Context derivatives-ℝ→ℝ
extends ℝ→ℝ

2 Derivatives

The derivative of a function is given by 𝒟(ℝ→ℝ) : ℝ→ℝ, which is a linear operator:

𝒟(f + g) ⇒ 𝒟(f) + 𝒟(g)
𝒟(f - g) ⇒ 𝒟(f) - 𝒟(g)
𝒟(s × f) ⇒ s × 𝒟(f)

The derivatives of products and compositions of two functions are given by:

𝒟(f × g) ⇒ (𝒟(f) × g) + (f × 𝒟(g))
𝒟(f ○ g) ⇒ (𝒟(f) ○ g) × 𝒟(g)

Context finite-differences-ℝ→ℝ
extends ℝ→ℝ

3 Finite difference operators

In numerical calculations, derivatives must often be approximated by finite differences. Since there are many possible schemes for computing finite differences, we define multiple finite-difference-operators with finite-difference-operator[fn:ℝ→ℝ, h:ℝ] : ℝ→ℝ, where h is the step size.

Next, we define Δ : finite-difference-family and finite-difference-scheme such that finite-difference-familyfinite-difference-scheme : finite-difference-operator.

With these definitions, the three most common finite-difference schemes are:

  • forward : finite-difference-scheme:
    Δforward[fn, h][x] ⇒ (fn[x + h] - fn[x]) ÷ h  ∀ x : ℝ

  • backward : finite-difference-scheme:
    Δbackward[fn, h][x] ⇒ (fn[x] - fn[x - h]) ÷ h  ∀ x : ℝ

  • central : finite-difference-scheme:
    Δcentral[fn, h][x] ⇒ (fn[x + (h ÷ 2)] - fn[x - (h ÷ 2)]) ÷ h  ∀ x : ℝ