{"size": 2700, "ext": "scrbl", "max_stars_repo_path": "examples/functions.scrbl", "max_stars_repo_name": "khinsen/leibniz-examples", "max_stars_repo_stars_event_min_datetime": "2017-03-22T08:37:51.000Z", "max_stars_repo_stars_event_max_datetime": "2020-10-12T22:58:00.000Z", "max_issues_repo_path": "examples/functions.scrbl", "max_issues_repo_name": "khinsen/leibniz-examples", "max_issues_repo_issues_event_min_datetime": null, "max_issues_repo_issues_event_max_datetime": null, "max_forks_repo_path": "examples/functions.scrbl", "max_forks_repo_name": "khinsen/leibniz-examples", "max_forks_repo_forks_event_min_datetime": "2018-02-05T07:35:03.000Z", "max_forks_repo_forks_event_max_datetime": "2020-10-12T22:58:02.000Z"}
{"max_stars_count": 2, "max_issues_count": null, "max_forks_count": 3, "avg_line_length": 36.4864864865, "max_line_length": 96, "alphanum_fraction": 0.6222222222}
#lang leibniz

@title{Functions}
@author{Konrad Hinsen}

@context["ℝ→ℝ"
         #:use "builtins/real-numbers"]{

@section{Real functions of one variable}

The sort @sort{ℝ→ℝ} describes real functions of one real variable.
Function application is defined by @op{ℝ→ℝ[ℝ] : ℝ}. 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:
@itemlist[
  @item{@op{f:ℝ→ℝ + g:ℝ→ℝ : ℝ→ℝ} with @linebreak[]
        @rule{(f + g)[x] ⇒ f[x] + g[x] ∀ x:ℝ}}
  @item{@op{f:ℝ→ℝ - g:ℝ→ℝ : ℝ→ℝ} with @linebreak[]
        @rule{(f - g)[x] ⇒ f[x] - g[x] ∀ x:ℝ}}
  @item{@op{f:ℝ→ℝ × g:ℝ→ℝ : ℝ→ℝ} with @linebreak[]
        @rule{(f × g)[x] ⇒ f[x] × g[x] ∀ x:ℝ}}
  @item{@op{s:ℝ × g:ℝ→ℝ : ℝ→ℝ} with @linebreak[]
        @rule{(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
  @inset{@op{f:ℝ→ℝ ○ g:ℝ→ℝ : ℝ→ℝ} with
         @rule{(f ○ g)[x] ⇒ f[g[x]] ∀ x:ℝ}}
}

@context["derivatives-ℝ→ℝ"
         #:extend "ℝ→ℝ"]{

@section{Derivatives}

The derivative of a function is given by @op{𝒟(ℝ→ℝ) : ℝ→ℝ}, which is
a linear operator:
  @inset{@rule{𝒟(f + g) ⇒ 𝒟(f) + 𝒟(g)}
         @rule{𝒟(f - g) ⇒ 𝒟(f) - 𝒟(g)}
         @rule{𝒟(s × f) ⇒ s × 𝒟(f)}}

The derivatives of products and compositions of two functions are given by:
  @inset{@rule{𝒟(f × g) ⇒ (𝒟(f) × g) + (f × 𝒟(g))}
         @rule{𝒟(f ○ g) ⇒ (𝒟(f) ○ g) × 𝒟(g)}}

}

@context["finite-differences-ℝ→ℝ"
         #:extend "ℝ→ℝ"]{

@section{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 @sort{finite-difference-operator}s with
@op{finite-difference-operator[fn:ℝ→ℝ, h:ℝ] : ℝ→ℝ}, where @term{h} is the step size.

Next, we define @op{Δ : finite-difference-family} and @sort{finite-difference-scheme}
such that @op{finite-difference-family_{finite-difference-scheme} : finite-difference-operator}.

With these definitions, the three most common finite-difference schemes are:
@itemlist[
    @item{@op{forward : finite-difference-scheme}: @linebreak[]
          @rule{Δ_{forward}[fn, h][x] ⇒ (fn[x + h] - fn[x]) ÷ h  ∀ x:ℝ}}
    @item{@op{backward : finite-difference-scheme}: @linebreak[]
          @rule{Δ_{backward}[fn, h][x] ⇒ (fn[x] - fn[x - h]) ÷ h  ∀ x:ℝ}}
    @item{@op{central : finite-difference-scheme}: @linebreak[]
          @rule{Δ_{central}[fn, h][x] ⇒ (fn[x + (h ÷ 2)] - fn[x - (h ÷ 2)]) ÷ h  ∀ x:ℝ}}]
}