a filter semantics for ∞

Michael Beeson San José State University

Freek Wiedijk University of Nijmegen

Calculemus 2002 Marseille, France 2002-07-03, 14:00

infinity

∞ in high school calculus

lim_{x→∞} \frac{1}{x + 1} = \frac{1}{lim_{x→∞}(x + 1)} = \frac{1}{lim_{x→∞} x + lim_{x→∞} 1} = \frac{1}{∞ + lim_{x→∞} 1}

= \frac{1}{∞ + 1} = \frac{1}{∞} = 0

calculus textbooks

– avoid this kind of calculation in the explanations – need this kind of calculation for the exercises

the symbol ∞ is confusing to the student:

infinite limits are … undefined? defined with value ∞?

∞ in MathXpert

MathXpert: computer algebra for high school students written by Michael Beeson as a three year research project followed by four years of commercial development

graphs, algebra, trigonometry, limits, differentiation, integration presentation looks exactly like in calculus textbooks correctness through non-standard analysis: completely hidden from user

\frac{1}{∞ + 1}  …
\frac{1}{∞}  lim u + v = ∞ if u → ∞ and lim v is finite
0  lim(u/v) = 0 if lim u ≠ 0, lim v = ±∞

Input: 1/(infinity + 1)

Error: Input not acceptable: you entered an undefined expression correctness of computer algebra

tension: mathematical correctness ⟷ doing useful calculations

‘too eager’ calculations are ‘repaired’ in later versions on an ad hoc basis, to shut up the most blatant criticism

main cause of problems: assumptions are not tracked systematically

                   Sqrt[x^{2}] = Sqrt[x^{2}]
      PowerExpand[Sqrt[x^{2}]] = x

Use PowerExpand with caution because PowerExpand disregards issues of branches of multi-valued functions.

  Integrate[Integrate[Sqrt[(x-y)^{2}],{x,0,1}],{y,0,1}] = 0

interfacing TPS with CAS:

correctness of TPS proofs will be tainted by CAS calculations semantics of computer algebra

semantics of CAS terms:

necessary to meaningfully interface CAS and TPS

           Integrate[1/x, x] = Log[x]

no clear semantics for this Integrate on the functional level

– is 1/x a number or a function?

– where is the constant of integration?

wanted: uniform semantics for CAS terms difficult because of feature interaction:

functional expressions, constants of integration, big-Oh notation, ∞, undefinedness, vectors and matrices, … ∞ and interval arithmetic in computer algebra

        1/(Infinity + 1) = O
          Sqrt[Infinity] = ∞
     Infinity - Infinity = Indeterminate
           Sin[Infinity] = Interval[{-1,1}]
      1/Interval[{-1,1}] = Interval[{-∞,-1},{1,∞}]
Infinity/Interval[{-1,1}] = Interval[{-∞,-∞},{∞,∞}]

Mathematica contains a calculus of three symbols:

Infinity
Indeterminate
Interval

filters

a filter semantics for ∞

limit values: filter on ℝ ← underlying topological space

≡ collection of open subsets of ℝ closed under finite ∩ closed under supersets

filter ∞ ≡ the set of all U such that U contains a neighborhood of ∞

U ∈ ∞ ⟺ ∃ a ∈ ℝ : (a, ∞) ⊆ U

• for us filters are collections of open sets only

• the two extreme filters are not excluded – set of all subsets: ‘improper’ filter

– empty set of subsets: ‘empty’ filter examples of filters

principal(a) ≡ ā ≡ {U | a ∈ U}

embeds ℝ in the space of filters

punctured(a) ≡ a^{±} ≡ {U | ∃ ε : (a − ε, a) ∪ (a, a + ε) ⊆ U}
left(a) ≡ a^{−} ≡ {U | ∃ ε : (a − ε, a) ⊆ U}
right(a) ≡ a^{+} ≡ {U | ∃ ε : (a, a + ε) ⊆ U}

corresponds to ‘normal’ and ‘one-sided’ limits

bi-infinity ≡ ±∞ ≡ {U | ∃ ε : (−∞, −1/ε) ∪ (1/ε, ∞) ⊆ U}

the filter value of lim_{x→0} 1/x

error filters

indeterminate ≡ ↔ ≡ {ℝ}
domain-error ≡ ⊥ ≡ ∅
improper ≡ † ≡ {U | U ⊆ ℝ}

lifting functions to filters

sum of two filters A and B ≡ filter generated by all X + Y where X ∈ A and Y ∈ B

X + Y = {x + y | x ∈ X, y ∈ Y }

the filter generated by a collection of sets A is {U | ∃ X ∈ A : X ⊆ U}

lifting functions f to filter versions f̄ definition of f̄ is analogous to that of + above

term language of CAS also makes sense for filter expressions refinement isn’t an infinite limit undefined? solution: the filter infinity refines the filter indeterminate:

∞ ⊑ ↔

definition of refinement: A ⊑ B ⟺ B ⊆ A as a set of subsets examples:

lim_{x→∞} sin x = [−1, 1] ⊑ ↔

lim_{x→0} x^{2} = 0^{+} ⊑ 0^{±} ⊑ ¯0

lim_{x→0} \frac{1}{x^{2}} = \frac{1}{0^{+}} = ∞ ⊑ \frac{1}{0^{±}} = ±∞ ⊑ \frac{1}{¯0} = ⊥

limits to a filter two kinds of limit notation:

lim_{x→a} for limits to real numbers Lim_{x→A} for ‘limits to filters’

correspondence theorem:

lim_{x→a} f(x) = b ⟺ Lim_{x→a^{±}} f(x) ⊑ b̄

use filters to calculate normal limits rigorously!

Lim_{x→0^{±}} x sin \frac{1}{x} ⊑ 0^{±} sin \frac{1}{0^{±}} = 0^{±} sin(±∞) = 0^{±}[−1, 1] = ¯0

⇒ lim_{x→0} x sin \frac{1}{x} = 0

interval filters as a uniform notation ‘interval filters’

\{ \begin{matrix}(a, b) & (a, b] \\ [a, b) & [a, b] \end{matrix} with \begin{matrix}a, b ∈ \{−∞\} ∪ ℝ ∪ \{∞\} \\ a ≤ b \end{matrix} \}

= ‘connected filters’: filters generated by a set of connected sets uniform way to write many filters

\begin{matrix}ā = [a, a] \\ a^{−} = [a, a) \\ a^{+} = (a, a] \\ a^{±} = [a, a) ∨ (a, a] \end{matrix}  \begin{matrix}∞ = [∞, ∞) \\ −∞ = (−∞, −∞] \\ ↔ = (−∞, ∞) \\ ±∞ = (−∞, −∞] ∨ [∞, ∞) \end{matrix}

A ∨ B is the join of two filters A and B: the set of filters is a lattice

outlook

filters versus Mathematica correspondence to Mathematica is not perfect different treatment of domain errors

Lim_{x→∞} \frac{1}{sin x} = \frac{1}{[−1, 1]} = (−∞, −1] ∨ [1, ∞) ← Mathematica
= \frac{1}{[−1, 1]} = ⊥  ← our definitions

\frac{1}{sin x} undefined at multiples of π filters versus non-standard analysis non-standard analysis:

another ‘calculus with first class infinity’

∞  ω
canonical  not canonical
∞ + 1 = ∞  ω + 1 ≠ ω
the set of filters  ultrapower model
set of filters  only one filter
arbitrary filter  ultrafilter
filter of open sets  filter of arbitrary sets

filters and ℂ Mathematica expressions are not real valued but complex valued

           PowerExpand[Log[-x]] = I π + Log[x]

filter approach works just as well for complex numbers examples of complex filters:

• complex infinity

• infinity along the positive x-axis

• limit inside an angular sector |θ| < π/4