## Functions

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.

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.

f:ℝ→ℝ ○ g:ℝ→ℝ : ℝ→ℝ with

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

Context derivatives-ℝ→ℝ

extends ℝ→ℝ

### 2` `Derivatives

𝒟(f + g) ⇒ 𝒟(f) + 𝒟(g)

𝒟(f - g) ⇒ 𝒟(f) - 𝒟(g)

𝒟(s × f) ⇒ s × 𝒟(f)

𝒟(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.

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 : ℝ