Definition: Legendre
Legendre(n;x) ==
if (n =z 0) then r1
if (n =z 1) then x
else ((2 * n) - 1 * x * Legendre(n - 1;x) - n - 1 * Legendre(n - 2;x))/n
fi
Lemma: Legendre_wf
∀[n:ℕ]. ∀[x:ℝ]. (Legendre(n;x) ∈ ℝ)
Lemma: Legendre_functionality
∀[n:ℕ]. ∀[x,y:ℝ]. Legendre(n;x) = Legendre(n;y) supposing x = y
Lemma: Legendre_0_lemma
∀x:Top. (Legendre(0;x) ~ r1)
Lemma: Legendre_1_lemma
∀x:Top. (Legendre(1;x) ~ x)
Lemma: Legendre-differential-equation
∀n:ℕ
∃f,g:(-∞, ∞) ⟶ℝ
((∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y))))
∧ (∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y))))
∧ d(g[x])/dx = λx.f[x] on (-∞, ∞)
∧ d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
∧ (∀x:ℝ. (((((r1 - x * x) * (f x)) - (r(2) * x) * (g x)) + (r(n * (n + 1)) * Legendre(n;x))) = r0))
∧ (0 < n ⇒ (∀x:ℝ. (((r1 - x * x) * (g x)) = ((r(n) * Legendre(n - 1;x)) - (r(n) * x) * Legendre(n;x))))))
Lemma: Legendre-1
∀n:ℕ. (Legendre(n;r1) = r1)
Lemma: Legendre-rminus
∀n:ℕ. ∀x:ℝ. (Legendre(n;-(x)) = (r(-1)^n * Legendre(n;x)))
Lemma: Legendre-minus-1
∀n:ℕ. (Legendre(n;r(-1)) = r((-1)^n))
Lemma: Legendre-zero-odd
∀n:ℕ. Legendre(n;r0) = r0 supposing (n rem 2) = 1 ∈ ℤ
Lemma: Legendre-roots-symmetric
∀[n:ℕ]. ∀[x:ℝ]. uiff(Legendre(n;-(x)) = r0;Legendre(n;x) = r0)
Lemma: Legendre-deriv-equation1
∀n:ℕ+
∃g:(-∞, ∞) ⟶ℝ
((∀x,y:ℝ. ((x = y) ⇒ ((g x) = (g y))))
∧ d(Legendre(n;x))/dx = λx.g[x] on (-∞, ∞)
∧ (∀x:ℝ. ((x * Legendre(n;x)) = (Legendre(n - 1;x) + ((x^2 - r1/r(n)) * (g x))))))
Lemma: Legendre-rpolynomial
∀n:ℕ. ∃a:ℕn + 1 ⟶ ℝ. ((∀x:ℝ. (Legendre(n;x) = (Σi≤n. a_i * x^i))) ∧ ((a n) = (r(doublefact((2 * n) - 1))/r((n)!))))
Definition: ratLegendre-aux
ratLegendre-aux(n;x;tr) ==
let k,a,b = tr in
if k=n
then a
else eval k' = k + 1 in
eval a' = rat-nat-div(ratadd(int-rat-mul((2 * k) + 1;ratmul(x;a));int-rat-mul(-k;b));k') in
ratLegendre-aux(n;x;<k', a', a>)
Lemma: ratLegendre-aux_wf
∀[x:ℤ × ℕ+]. ∀[n:ℕ+]. ∀[tr:k:ℕ+n + 1
× {a:ℤ × ℕ+| ratreal(a) = Legendre(k;ratreal(x))}
× {b:ℤ × ℕ+| ratreal(b) = Legendre(k - 1;ratreal(x))} ].
(ratLegendre-aux(n;x;tr) ∈ {y:ℤ × ℕ+| ratreal(y) = Legendre(n;ratreal(x))} )
Definition: ratLegendre
ratLegendre(n;x) == if (n =z 0) then <1, 1> else ratLegendre-aux(n;x;<1, x, 1, 1>) fi
Lemma: ratLegendre_wf
∀[x:ℤ × ℕ+]. ∀[n:ℕ]. (ratLegendre(n;x) ∈ {y:ℤ × ℕ+| ratreal(y) = Legendre(n;ratreal(x))} )
Lemma: ratreal-ratLegendre
∀[x:ℤ × ℕ+]. ∀[n:ℕ]. (ratreal(ratLegendre(n;x)) = Legendre(n;ratreal(x)))
Lemma: partition-refinement-sum
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀q:partition(I). ∀n:ℕ+.
((partition-mesh(I;q) ≤ (mc 1 n))
⇒ frs-increasing(q)
⇒ (∀p:partition(I). ∀x:partition-choice(full-partition(I;p)). ∀y:partition-choice(full-partition(I;q)).
(p refines q ⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ ((r1/r(n)) * |I|)))))))
Definition: default-partition-choice
default-partition-choice(p) == λi.p[i]
Lemma: default-partition-choice_wf
∀[p:ℝ List]. default-partition-choice(p) ∈ partition-choice(p) supposing frs-non-dec(p)
Lemma: separated-partition-sum
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀q:partition(I). ∀n:ℕ+.
((partition-mesh(I;q) ≤ (mc 1 n))
⇒ (∀p:partition(I). ∀m:ℕ+.
((partition-mesh(I;p) ≤ (mc 1 m))
⇒ separated-partitions(p;q)
⇒ (∀x:partition-choice(full-partition(I;p)). ∀y:partition-choice(full-partition(I;q)).
(|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (((r1/r(n)) + (r1/r(m))) * |I|))))))))
Lemma: nearby-partition-sum
∀I:Interval
(icompact(I)
⇒ iproper(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀p:partition(I). ∀x:partition-choice(full-partition(I;p)).
∀alpha:{a:ℝ| r0 < a} .
∃e:{e:ℝ| r0 < e}
∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ alpha))))
Lemma: nearby-partition-sum-ext
∀I:Interval
(icompact(I)
⇒ iproper(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀p:partition(I). ∀x:partition-choice(full-partition(I;p)).
∀alpha:{a:ℝ| r0 < a} .
∃e:{e:ℝ| r0 < e}
∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ alpha))))
Lemma: nearby-partition-sum-no-mc
∀I:Interval
(icompact(I)
⇒ iproper(I)
⇒ (∀f:{f:I ⟶ℝ| ifun(f;I)} . ∀p:partition(I). ∀x:partition-choice(full-partition(I;p)). ∀alpha:{a:ℝ| r0 < a} .
∃e:{e:ℝ| r0 < e}
∀q:partition(I). ∀y:partition-choice(full-partition(I;q)).
(nearby-partitions(e;p;q)
⇒ (∀i:ℕ||p|| + 1. (|x[i] - y[i]| ≤ e))
⇒ (|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ alpha))))
Lemma: nearby-partition-mesh
∀I:Interval
(icompact(I)
⇒ (∀e:{e:ℝ| r0 < e} . ∀p,p':partition(I).
(nearby-partitions((e/r(2));p;p') ⇒ (partition-mesh(I;p') ≤ (partition-mesh(I;p) + e)))))
Lemma: nearby-separated-partition-sum
∀I:Interval
(icompact(I)
⇒ iproper(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀alpha,e:{e:ℝ| r0 < e} . ∀p,q:partition(I).
∀x:partition-choice(full-partition(I;p)). ∀y:partition-choice(full-partition(I;q)).
∃p':partition(I)
∃x':partition-choice(full-partition(I;p'))
((partition-mesh(I;p') ≤ (partition-mesh(I;p) + e))
∧ (∃q':partition(I)
∃y':partition-choice(full-partition(I;q'))
(separated-partitions(p';q')
∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p'))
- S(f;full-partition(I;q'))|
+ alpha)))))))
Lemma: nearby-separated-partition-sum-no-mc
∀I:Interval
(icompact(I)
⇒ iproper(I)
⇒ (∀f:{f:I ⟶ℝ| ifun(f;I)} . ∀alpha,e:{e:ℝ| r0 < e} . ∀p,q:partition(I). ∀x:partition-choice(full-partition(I;p)).
∀y:partition-choice(full-partition(I;q)).
∃p':partition(I)
∃x':partition-choice(full-partition(I;p'))
((partition-mesh(I;p') ≤ (partition-mesh(I;p) + e))
∧ (∃q':partition(I)
∃y':partition-choice(full-partition(I;q'))
(separated-partitions(p';q')
∧ (partition-mesh(I;q') ≤ (partition-mesh(I;q) + e))
∧ (|S(f;full-partition(I;p)) - S(f;full-partition(I;q))| ≤ (|S(f;full-partition(I;p'))
- S(f;full-partition(I;q'))|
+ alpha)))))))
Lemma: partition-sum-bound
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
(|S(f;full-partition(I;p))| ≤ (||f[x]||_I * |I|))))
Lemma: partition-sum-bound-no-mc
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀b:{b:ℝ| (r0 ≤ b) ∧ (∀x:ℝ. ((x ∈ I) ⇒ (|f x| ≤ b)))} . ∀p:partition(I).
∀y:partition-choice(full-partition(I;p)).
(|S(f;full-partition(I;p))| ≤ (b * |I|))))
Lemma: general-partition-sum
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀e:{e:ℝ| r0 < e} .
∃d:{d:ℝ| r0 < d}
∀p,q:{p:partition(I)| partition-mesh(I;p) ≤ d} . ∀x:partition-choice(full-partition(I;p)).
∀y:partition-choice(full-partition(I;q)).
(|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (e * |I|))))
Lemma: general-partition-sum-ext
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀mc:f[x] continuous for x ∈ I. ∀e:{e:ℝ| r0 < e} .
∃d:{d:ℝ| r0 < d}
∀p,q:{p:partition(I)| partition-mesh(I;p) ≤ d} . ∀x:partition-choice(full-partition(I;p)).
∀y:partition-choice(full-partition(I;q)).
(|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ (e * |I|))))
Lemma: general-partition-sum-from-bound
∀I:Interval
(icompact(I)
⇒ (∀f:{f:I ⟶ℝ| ifun(f;I)} . ∀b:{b:ℝ| (r0 ≤ b) ∧ (∀x:ℝ. ((x ∈ I) ⇒ (|f x| ≤ b)))} . ∀e:{e:ℝ| r0 < e} .
∃d:{d:ℝ| r0 < d}
∀p,q:{p:partition(I)| partition-mesh(I;p) ≤ d} . ∀x:partition-choice(full-partition(I;p)).
∀y:partition-choice(full-partition(I;q)).
(|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ e)))
Lemma: general-partition-sum-no-mc
∀I:Interval
(icompact(I)
⇒ (∀f:{f:I ⟶ℝ| ifun(f;I)} . ∀e:{e:ℝ| r0 < e} .
∃d:{d:ℝ| r0 < d}
∀p,q:{p:partition(I)| partition-mesh(I;p) ≤ d} . ∀x:partition-choice(full-partition(I;p)).
∀y:partition-choice(full-partition(I;q)).
(|S(f;full-partition(I;q)) - S(f;full-partition(I;p))| ≤ e)))
Lemma: partition-sum-constant
∀I:Interval
(icompact(I)
⇒ (∀c:ℝ. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)). (S(λx.c;full-partition(I;p)) = (c * |I|))))
Lemma: partition-sum-radd
∀I:Interval
(icompact(I)
⇒ (∀f,g:I ⟶ℝ. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
(S(λx.((f x) + (g x));full-partition(I;p)) = (S(f;full-partition(I;p)) + S(g;full-partition(I;p))))))
Lemma: partition-sum-rmul-const
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀c:ℝ. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
(S(λx.(c * (f x));full-partition(I;p)) = (c * S(f;full-partition(I;p))))))
Lemma: partition-sum-rleq
∀I:Interval
(icompact(I)
⇒ (∀f,g:I ⟶ℝ.
∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
(S(f;full-partition(I;p)) ≤ S(g;full-partition(I;p)))
supposing ∀x:ℝ. ((x ∈ I) ⇒ ((f x) ≤ (g x)))))
Lemma: rabs-partition-sum
∀I:Interval
(icompact(I)
⇒ (∀f:I ⟶ℝ. ∀p:partition(I). ∀y:partition-choice(full-partition(I;p)).
(|S(f;full-partition(I;p))| ≤ S(λx.|f x|;full-partition(I;p)))))
Definition: Riemann-sum
Riemann-sum(f;a;b;k) == let p = full-partition([a, b];uniform-partition([a, b];k)) in S(f;p)
Lemma: Riemann-sum_wf
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[k:ℕ+]. (Riemann-sum(f;a;b;k) ∈ ℝ)
Lemma: Riemann-sums-converge
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:[a, b] ⟶ℝ. ∀mc:f[x] continuous for x ∈ [a, b]. Riemann-sum(f;a;b;k + 1)↓ as k→∞
Lemma: Riemann-sums-converge-no-mc
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} . Riemann-sum(f;a;b;k + 1)↓ as k→∞
Definition: Riemann-integral
∫ f[x] dx on [a, b] == fst((TERMOF{Riemann-sums-converge-no-mc:o, 1:l} a b (λx.f[x])))
Lemma: Riemann-integral_wf
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ]. (∫ f[x] dx on [a, b] ∈ ℝ)
Lemma: Riemann-sums-converge-to
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} . lim k→∞.Riemann-sum(λx.f[x];a;b;k + 1) = ∫ f[x] dx on [a, b\000C]
Lemma: partition-sums-converge
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} . ∀e:{e:ℝ| r0 < e} .
∃d:{d:ℝ| r0 < d}
∀p:partition([a, b])
((partition-mesh([a, b];p) ≤ d)
⇒ (∀y:partition-choice(full-partition([a, b];p))
(|S(λx.f[x];full-partition([a, b];p)) - ∫ f[x] dx on [a, b]| ≤ e)))
Lemma: Riemann-sum-constant
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[c:ℝ]. ∀[k:ℕ+]. (Riemann-sum(λx.c;a;b;k) = (c * (b - a)))
Lemma: Riemann-sum-radd
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
(Riemann-sum(λx.((f x) + (g x));a;b;k) = (Riemann-sum(f;a;b;k) + Riemann-sum(g;a;b;k)))
Lemma: Riemann-sum-rmul-constant
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[c:ℝ]. ∀[k:ℕ+].
(Riemann-sum(λx.(c * (f x));a;b;k) = (c * Riemann-sum(λx.(f x);a;b;k)))
Lemma: Riemann-sum-rleq
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:[a, b] ⟶ℝ]. ∀[k:ℕ+].
Riemann-sum(f;a;b;k) ≤ Riemann-sum(g;a;b;k) supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((f x) ≤ (g x)))
Lemma: rabs-Riemann-sum
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:[a, b] ⟶ℝ]. ∀[k:ℕ+]. (|Riemann-sum(f;a;b;k)| ≤ Riemann-sum(λx.|f x|;a;b;k))
Lemma: Riemann-integral-radd
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
(∫ f[x] + g[x] dx on [a, b] = (∫ f[x] dx on [a, b] + ∫ g[x] dx on [a, b]))
Lemma: Riemann-integral-rmul-const
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ]. ∀[c:ℝ].
(∫ c * f[x] dx on [a, b] = (c * ∫ f[x] dx on [a, b]))
Lemma: Riemann-integral-const
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[c:ℝ]. (∫ c dx on [a, b] = (c * (b - a)))
Lemma: Riemann-integral-rleq
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∫ f[x] dx on [a, b] ≤ ∫ g[x] dx on [a, b] supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ (f[x] ≤ g[x]))
Lemma: Riemann-integral-upper-bound
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∀c:ℝ. ∫ f[x] dx on [a, b] ≤ (c * (b - a)) supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ (f[x] ≤ c))
Lemma: Riemann-integral-lower-bound
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∀c:ℝ. (c * (b - a)) ≤ ∫ f[x] dx on [a, b] supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ (c ≤ f[x]))
Lemma: Riemann-integral-nonneg
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
r0 ≤ ∫ f[x] dx on [a, b] supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ (r0 ≤ f[x]))
Lemma: Riemann-integral-bounds
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∀c1,c2:ℝ.
((c1 * (b - a)) ≤ ∫ f[x] dx on [a, b]) ∧ (∫ f[x] dx on [a, b] ≤ (c2 * (b - a)))
supposing ∀x:ℝ. ((x ∈ [a, b]) ⇒ ((c1 ≤ f[x]) ∧ (f[x] ≤ c2)))
Lemma: rabs-Riemann-integral
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ]. (|∫ f[x] dx on [a, b]| ≤ (||f[x]||_x:[a, b] * (b - a)\000C))
Lemma: Riemann-integral-single
∀[a,b:ℝ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ]. (∫ f[x] dx on [a, b] = r0) supposing a = b
Lemma: Riemann-integral-same-endpoints
∀[a:ℝ]. ∀[f:{f:[a, a] ⟶ℝ| ifun(f;[a, a])} ]. (∫ f[x] dx on [a, a] = r0)
Lemma: Riemann-integral-additive
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∀c:ℝ. ∫ f[x] dx on [a, b] = (∫ f[x] dx on [a, c] + ∫ f[x] dx on [c, b]) supposing (a ≤ c) ∧ (c ≤ b)
Lemma: Riemann-integral_functionality_endpoints
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∀a',b':ℝ. (∫ f[x] dx on [a, b] = ∫ f[x] dx on [a', b']) supposing ((a = a') and (b = b'))
Lemma: Riemann-integral_functionality
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
∫ f[x] dx on [a, b] = ∫ g[x] dx on [a, b] supposing ∀x:ℝ. (((a ≤ x) ∧ (x ≤ b)) ⇒ (f[x] = g[x]))
Lemma: Riemann-integral-rminus
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ]. (∫ -(f[x]) dx on [a, b] = -(∫ f[x] dx on [a, b]))
Lemma: Riemann-integral-rsub
∀[a:ℝ]. ∀[b:{b:ℝ| a ≤ b} ]. ∀[f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} ].
(∫ f[x] - g[x] dx on [a, b] = (∫ f[x] dx on [a, b] - ∫ g[x] dx on [a, b]))
Lemma: Riemann-integral-rless
∀a:ℝ. ∀b:{b:ℝ| a < b} . ∀f:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} . ∀c:ℝ.
(((∀x:ℝ. ((x ∈ [a, b]) ⇒ (f[x] ≤ c))) ∧ (∃x:ℝ. ((x ∈ [a, b]) ∧ (f[x] < c))))
⇒ (∫ f[x] dx on [a, b] < (c * (b - a))))
Definition: integral
a_∫-b f[x] dx == ∫ f[x] dx on [rmin(a;b), b] - ∫ f[x] dx on [rmin(a;b), a]
Lemma: integral_wf
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ]. (a_∫-b f[x] dx ∈ ℝ)
Lemma: integral-is-Riemann
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
a_∫-b f[x] dx = ∫ f[x] dx on [a, b] supposing a ≤ b
Lemma: integral-is-Riemann-on-interval
∀I:Interval
∀[f:{f:I ⟶ℝ| ∀a,b:{x:ℝ| x ∈ I} . ((a = b) ⇒ (f[a] = f[b]))} ]. ∀[a,b:{x:ℝ| x ∈ I} ].
a_∫-b f[x] dx = ∫ f[x] dx on [a, b] supposing a ≤ b
Lemma: integral-single
∀[a:ℝ]. ∀[f:{f:[a, a] ⟶ℝ| ifun(f;[a, a])} ]. (a_∫-a f[x] dx = r0)
Lemma: integral-radd
∀[a,b:ℝ]. ∀[f,g:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
(a_∫-b f[x] + g[x] dx = (a_∫-b f[x] dx + a_∫-b g[x] dx))
Lemma: integral-rmul-const
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ]. ∀[c:ℝ].
(a_∫-b c * f[x] dx = (c * a_∫-b f[x] dx))
Lemma: integral-const
∀[a,b,c:ℝ]. (a_∫-b c dx = (c * (b - a)))
Lemma: integral-zero
∀[a,b:ℝ]. (a_∫-b r0 dx = r0)
Lemma: integral-additive-lemma
∀[m,M:ℝ].
∀[f:{f:[m, M] ⟶ℝ| ifun(f;[m, M])} ]. ∀[a,b:{x:ℝ| x ∈ [m, M]} ].
(a_∫-b f[x] dx = (∫ f[x] dx on [m, b] - ∫ f[x] dx on [m, a]))
supposing m ≤ M
Lemma: integral-additive
∀[a,b,c:ℝ]. ∀[f:{f:[rmin(a;rmin(b;c)), rmax(a;rmax(b;c))] ⟶ℝ| ifun(f;[rmin(a;rmin(b;c)), rmax(a;rmax(b;c))])} ].
(a_∫-b f[x] dx = (a_∫-c f[x] dx + c_∫-b f[x] dx))
Lemma: integral-reverse
∀[a,c:ℝ]. ∀[f:{f:[rmin(a;c), rmax(a;c)] ⟶ℝ| ifun(f;[rmin(a;c), rmax(a;c)])} ]. (a_∫-c f[x] dx = -(c_∫-a f[x] dx))
Lemma: integral_functionality_endpoints
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
∀a',b':ℝ. (a_∫-b f[x] dx = a'_∫-b' f[x] dx) supposing ((a = a') and (b = b'))
Lemma: integral_functionality
∀[a,b:ℝ]. ∀[f,g:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
a_∫-b f[x] dx = a_∫-b g[x] dx supposing ∀x:ℝ. (((rmin(a;b) ≤ x) ∧ (x ≤ rmax(a;b))) ⇒ (f[x] = g[x]))
Lemma: integral-int-rmul
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ]. ∀[c:ℤ].
(a_∫-b c * f[x] dx = c * a_∫-b f[x] dx)
Lemma: integral-int-rdiv
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ]. ∀[c:ℤ-o].
(a_∫-b (f[x])/c dx = (a_∫-b f[x] dx)/c)
Lemma: integral-rsum
∀[n,m:ℤ]. ∀[a,b:ℝ]. ∀[f:{f:{n..m + 1-} ⟶ [rmin(a;b), rmax(a;b)] ⟶ℝ|
∀i:{n..m + 1-}. ifun(λx.f[i;x];[rmin(a;b), rmax(a;b)])} ].
(a_∫-b Σ{f[i;x] | n≤i≤m} dx = Σ{a_∫-b f[i;x] dx | n≤i≤m})
Definition: integrate
a_∫- f[t] dt == λx.a_∫-x f[t] dt
Lemma: integrate_wf
∀[I:Interval]. ∀[a:{a:ℝ| a ∈ I} ]. ∀[f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} ].
(a_∫- f[t] dt ∈ {f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} )
Lemma: integral-same-endpoints
∀I:Interval. ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} . ∀a:{a:ℝ| a ∈ I} . (a_∫-a f[t] dt = r0)
Lemma: integral-equal-endpoints
∀I:Interval. ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} . ∀a,b:{a:ℝ| a ∈ I} .
((a = b) ⇒ (a_∫-b f[t] dt = r0))
Lemma: integral-rsub
∀[a,b:ℝ]. ∀[f,g:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
(a_∫-b f[x] - g[x] dx = (a_∫-b f[x] dx - a_∫-b g[x] dx))
Lemma: rabs-integral
∀[a,b:ℝ]. ∀[f:{f:[rmin(a;b), rmax(a;b)] ⟶ℝ| ifun(f;[rmin(a;b), rmax(a;b)])} ].
(|a_∫-b f[x] dx| ≤ (||f[x]||_x:[rmin(a;b), rmax(a;b)] * |a - b|))
Lemma: derivative-of-integral
∀I:Interval. ∀a:{a:ℝ| a ∈ I} . ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} .
d(a_∫-x f[t] dt)/dx = λt.f[t] on I
Lemma: fund-theorem-of-calculus
∀I:Interval
(iproper(I)
⇒ (∀a:{a:ℝ| a ∈ I} . ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} . ∀g:I ⟶ℝ.
(d(g[x])/dx = λx.f[x] on I ⇒ (∃c:ℝ. ∀x:{a:ℝ| a ∈ I} . (a_∫-x f[t] dt = (g[x] + c))))))
Lemma: fun-converges-to-integral
∀I:Interval. ∀f:ℕ ⟶ I ⟶ℝ. ∀F:I ⟶ℝ.
(lim n→∞.f[n;x] = λy.F[y] for x ∈ I
⇒ (∀n:ℕ. ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ (f[n;x] = f[n;y])))
⇒ (∀a:{a:ℝ| a ∈ I} . lim n→∞.a_∫-x f[n;t] dt = λx.a_∫-x F[t] dt for x ∈ I))
Lemma: fun-converges-to-derivative
∀I:Interval
(iproper(I)
⇒ (∀f,f':ℕ ⟶ I ⟶ℝ. ∀F,G:I ⟶ℝ.
((∀n:ℕ. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (f'[n;x] = f'[n;y])))
⇒ lim n→∞.f[n;x] = λy.F[y] for x ∈ I
⇒ lim n→∞.f'[n;x] = λy.G[y] for x ∈ I
⇒ (∀n:ℕ. d(f[n;x])/dx = λx.f'[n;x] on I)
⇒ d(F[x])/dx = λx.G[x] on I)))
Lemma: ftc-integral
∀I:Interval
(iproper(I)
⇒ (∀a,b:{a:ℝ| a ∈ I} . ∀f:{f:I ⟶ℝ| ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ ((f x) = (f y)))} . ∀g:I ⟶ℝ.
(d(g[x])/dx = λx.f[x] on I ⇒ (a_∫-b f[t] dt = (g[b] - g[a])))))
Lemma: ftc-total-integral
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f[x] = f[y])))
⇒ d(g[x])/dx = λx.f[x] on (-∞, ∞)
⇒ (∀a,b:ℝ. (a_∫-b f[t] dt = (g[b] - g[a]))))
Lemma: integral-rnexp
∀[a,b:ℝ]. ∀[m:ℕ]. (a_∫-b x^m dx = (b^m + 1 - a^m + 1/r(m + 1)))
Lemma: integral-rnexp-from-0
∀[b:ℝ]. ∀[m:ℕ]. (r0_∫-b x^m dx = (b^m + 1/r(m + 1)))
Lemma: integral-from-Taylor-1
∀a:ℝ. ∀t:{t:ℝ| r0 < t} . ∀F:ℕ ⟶ (a - t, a + t) ⟶ℝ.
((∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} . ((x = y) ⇒ (F[k;x] = F[k;y])))
⇒ infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
⇒ (∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t))
⇒ (∀b:{b:ℝ| b ∈ (a - t, a + t)}
lim n→∞.b_∫-x Σ{(F[i;a]/r((i)!)) * t - a^i | 0≤i≤n} dt = λx.b_∫-x F[0;t] dt for x ∈ (a - t, a + t)))
Lemma: integral-from-Taylor
∀a:ℝ. ∀t:{t:ℝ| r0 < t} . ∀F:ℕ ⟶ (a - t, a + t) ⟶ℝ.
((∀k:ℕ. ∀x,y:{x:ℝ| x ∈ (a - t, a + t)} . ((x = y) ⇒ (F[k;x] = F[k;y])))
⇒ infinite-deriv-seq((a - t, a + t);i,x.F[i;x])
⇒ (∀r:{r:ℝ| (r0 ≤ r) ∧ (r < t)} . lim k→∞.r^k * (F[k + 1;x]/r((k)!)) = λx.r0 for x ∈ (a - t, a + t))
⇒ (∀b:{b:ℝ| b ∈ (a - t, a + t)}
lim n→∞.Σ{(F[i;a]/r((i)!)) * (x - a^i + 1 - b - a^i + 1/r(i + 1)) | 0≤i≤n} = λx.b_∫-x F[0;t] dt for x ∈ (a
- t, a + t)))
Lemma: derivative-rexp
d(e^x)/dx = λx.e^x on (-∞, ∞)
Lemma: rexp-unique
∀f:ℝ ⟶ ℝ
((∀x,y:ℝ. ((x = y) ⇒ (f[x] = f[y]))) ⇒ (f[r0] = r1) ⇒ d(f[x])/dx = λx.f[x] on (-∞, ∞) ⇒ (∀x:ℝ. (f[x] = e^x)))
Lemma: rexp-radd
∀[x,y:ℝ]. (e^x + y = (e^x * e^y))
Lemma: rnexp-rexp
∀[x:ℝ]. ∀[N:ℕ]. (e^x^N = e^r(N) * x)
Lemma: rexp-positive
∀y:ℝ. (r0 < e^y)
Lemma: rexp-non-decreasing
∀[a,b:ℝ]. e^a ≤ e^b supposing a ≤ b
Lemma: rexp-increasing
∀a,b:ℝ. ((a < b) ⇒ (e^a < e^b))
Lemma: rexp_functionality_wrt_rless
∀x,y:ℝ. ((x < y) ⇒ (e^x < e^y))
Lemma: rexp_functionality_wrt_rleq
∀x,y:ℝ. ((x ≤ y) ⇒ (e^x ≤ e^y))
Lemma: rexp-rminus
∀[x:ℝ]. (e^-(x) = (r1/e^x))
Lemma: rexp-difference-bound
∀x,y:ℝ. ((x < y) ⇒ ((e^y - e^x) ≤ (e^y * (y - x))))
Lemma: derivative-rexp-fun
∀I:Interval. ∀f,f':I ⟶ℝ.
(iproper(I)
⇒ (∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on I
⇒ d(e^f[x])/dx = λx.e^f[x] * f'[x] on I)
Lemma: derivative-rexp-fun2
∀f,f':ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on (-∞, ∞)
⇒ d(e^f[x])/dx = λx.e^f[x] * f'[x] on (-∞, ∞))
Lemma: small-rexp-remainder
∀[x:{x:ℝ| |x| ≤ (r1/r(4))} ]. ∀[n:ℕ]. (|e^x - Σ{(x^k/r((k)!)) | 0≤k≤n}| ≤ (r1/r(4^n * 3 * (n)!)))
Lemma: rexp-poly-approx
∀[x:{x:ℝ| |x| ≤ (r1/r(4))} ]. ∀[k:ℕ]. ∀[N:ℕ+].
(|e^x - (r(rexp-approx(x;k;N))/r(2 * N))| ≤ ((r1/r(4^k * 3 * (k)!)) + (r1/r(N))))
Lemma: rexp-approx-lemma
∀N:ℕ+. (∃k:ℕ [(N ≤ (4^k * 3 * (k)!))])
Lemma: rexp-approx-lemma-ext
∀N:ℕ+. (∃k:ℕ [(N ≤ (4^k * 3 * (k)!))])
Lemma: rexp-approx-for-small
∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(4))} . (∃z:ℤ [(|e^x - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
Lemma: rexp-approx-for-small-ext
∀N:ℕ+. ∀x:{x:ℝ| |x| ≤ (r1/r(4))} . (∃z:ℤ [(|e^x - (r(z)/r(2 * N))| ≤ (r(2)/r(N)))])
Definition: rexp-small
rexp-small(x) == accelerate(2;λN.rexp-approx(x;genfact-inv(N;3;m.4 * m);N))
Lemma: rexp-small_wf
∀[x:{x:ℝ| |x| ≤ (r1/r(4))} ]. (rexp-small(x) ∈ {y:ℝ| y = e^x} )
Definition: real_exp
real_exp(x) ==
case rless-case((r1)/5;(r1)/4;42;x)
of inl(_) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)^N
| inr(_) =>
case rless-case((r(-1))/4;(r(-1))/5;42;x)
of inl(_) =>
rexp-small(x)
| inr(_) =>
eval N = canonical-bound(|4 * x|) in
rexp-small((x)/N)^N
Lemma: real_exp_wf
∀[x:ℝ]. (real_exp(x) ∈ {y:ℝ| y = e^x} )
Lemma: real_exp-req
∀[x:ℝ]. (real_exp(x) = e^x)
Lemma: derivative-sine
d(sine(x))/dx = λx.cosine(x) on (-∞, ∞)
Lemma: derivative-cosine
d(cosine(x))/dx = λx.-(sine(x)) on (-∞, ∞)
Lemma: sine-cosine-pythag
∀x:ℝ. ((sine(x)^2 + cosine(x)^2) = r1)
Lemma: rabs-sine-rleq
∀x:ℝ. (|sine(x)| ≤ r1)
Lemma: rabs-cosine-rleq
∀x:ℝ. (|cosine(x)| ≤ r1)
Lemma: rabs-difference-sine-rleq
∀x,y:ℝ. (|sine(x) - sine(y)| ≤ |x - y|)
Lemma: rabs-difference-cosine-rleq
∀x,y:ℝ. (|cosine(x) - cosine(y)| ≤ |x - y|)
Lemma: converges-to-sine
∀x:ℝ. lim n→∞.if n=0 then r0 else (sine((x within 1/n)) within 1/n) = sine(x)
Lemma: converges-to-sine-ext
∀x:ℝ. lim n→∞.if n=0 then r0 else (sine((x within 1/n)) within 1/n) = sine(x)
Lemma: converges-to-cosine
∀x:ℝ. lim n→∞.if n=0 then r0 else (cosine((x within 1/n)) within 1/n) = cosine(x)
Lemma: converges-to-cosine-ext
∀x:ℝ. lim n→∞.if n=0 then r0 else (cosine((x within 1/n)) within 1/n) = cosine(x)
Definition: rsin
rsin(x) == approx-arg(λx.sine(x);1;x)
Lemma: rsin_wf1
∀[x:ℝ]. (rsin(x) ∈ {y:ℝ| sine(x) = y} )
Lemma: rsin_wf
∀[x:ℝ]. (rsin(x) ∈ ℝ)
Lemma: rsin-is-sine
∀[x:ℝ]. (rsin(x) = sine(x))
Lemma: rsin0
rsin(r0) = r0
Lemma: rsin_functionality
∀[x,y:ℝ]. rsin(x) = rsin(y) supposing x = y
Definition: rcos
rcos(x) == approx-arg(λx.cosine(x);1;x)
Lemma: rcos_wf1
∀[x:ℝ]. (rcos(x) ∈ {y:ℝ| cosine(x) = y} )
Lemma: rcos_wf
∀[x:ℝ]. (rcos(x) ∈ ℝ)
Lemma: rcos-is-cosine
∀[x:ℝ]. (rcos(x) = cosine(x))
Lemma: rcos0
rcos(r0) = r1
Lemma: rcos-rminus
∀x:ℝ. (rcos(-(x)) = rcos(x))
Lemma: rcos_functionality
∀[x,y:ℝ]. rcos(x) = rcos(y) supposing x = y
Lemma: rcos-rabs
∀x:ℝ. (rcos(|x|) = rcos(x))
Lemma: derivative-rsin
d(rsin(x))/dx = λx.rcos(x) on (-∞, ∞)
Lemma: derivative-rcos
d(rcos(x))/dx = λx.-(rsin(x)) on (-∞, ∞)
Lemma: rsin-rcos-pythag
∀x:ℝ. ((rsin(x)^2 + rcos(x)^2) = r1)
Lemma: rsin-rminus
∀x:ℝ. (rsin(-(x)) = -(rsin(x)))
Lemma: rabs-rsin-rleq
∀x:ℝ. (|rsin(x)| ≤ r1)
Lemma: rsin-bounds
∀x:ℝ. (rsin(x) ∈ [r(-1), r1])
Lemma: rabs-rcos-rleq
∀x:ℝ. (|rcos(x)| ≤ r1)
Lemma: rcos-bounds
∀x:ℝ. (rcos(x) ∈ [r(-1), r1])
Lemma: rabs-difference-rsin-rleq
∀x,y:ℝ. (|rsin(x) - rsin(y)| ≤ |x - y|)
Lemma: rabs-difference-rcos-rleq
∀x,y:ℝ. (|rcos(x) - rcos(y)| ≤ |x - y|)
Lemma: rsin-radd
∀[x,y:ℝ]. (rsin(x + y) = ((rsin(x) * rcos(y)) + (rcos(x) * rsin(y))))
Lemma: rsin-rsub
∀[x,y:ℝ]. (rsin(x - y) = ((rsin(x) * rcos(y)) - rcos(x) * rsin(y)))
Lemma: rsin-reduce2
∀[x:ℝ]. (rsin(x) = 2 * rsin((x)/2) * rcos((x)/2))
Lemma: rcos-radd
∀[x,y:ℝ]. (rcos(x + y) = ((rcos(x) * rcos(y)) - rsin(x) * rsin(y)))
Lemma: rcos-reduce2
∀[x:ℝ]. (rcos(x) = (rcos((x)/2)^2 - rsin((x)/2)^2))
Lemma: rsin-reduce4
∀[x:ℝ]. (rsin(x) = 4 * rcos((x)/4) * (rsin((x)/4) - 2 * rsin((x)/4)^3))
Lemma: rcos-reduce4
∀[x:ℝ]. (rcos(x) = (r1 - 8 * rsin((x)/4)^2 * rcos((x)/4)^2))
Definition: sine-medium
sine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl(_) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)^3)
| inr(_) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl(_) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr(_) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl(_) =>
sine-small(x)
| inr(_) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl(_) =>
2 * sine-small((x)/2) * cosine-small((x)/2)
| inr(_) =>
4 * cosine-small((x)/4) * (sine-small((x)/4) - 2 * sine-small((x)/4)^3)
Lemma: sine-medium_wf
∀[x:{x:ℝ| x ∈ [r(-2), r(2)]} ]. (sine-medium(x) ∈ {y:ℝ| y = sine(x)} )
Definition: cosine-medium
cosine-medium(x) ==
case rless-case((r(99))/100;r1;250;x)
of inl(_) =>
r1 - 8 * sine-small((x)/4)^2 * cosine-small((x)/4)^2
| inr(_) =>
case rless-case((r(49))/100;(r1)/2;250;x)
of inl(_) =>
cosine-small((x)/2)^2 - sine-small((x)/2)^2
| inr(_) =>
case rless-case((r(-1))/2;(r(-49))/100;250;x)
of inl(_) =>
cosine-small(x)
| inr(_) =>
case rless-case(r(-1);(r(-99))/100;250;x)
of inl(_) =>
cosine-small((x)/2)^2 - sine-small((x)/2)^2
| inr(_) =>
r1 - 8 * sine-small((x)/4)^2 * cosine-small((x)/4)^2
Lemma: cosine-medium_wf
∀[x:{x:ℝ| x ∈ [r(-2), r(2)]} ]. (cosine-medium(x) ∈ {y:ℝ| y = cosine(x)} )
Lemma: rcos-rsub
∀[x,y:ℝ]. (rcos(x - y) = ((rcos(x) * rcos(y)) + (rsin(x) * rsin(y))))
Lemma: rsin-positive-near-11/7
∀x:{x:ℝ| x ∈ ((r(41)/r(70)), (r(179)/r(70)))} . (r0 < rsin(x))
Lemma: rcos-positive-near-0
∀x:{x:ℝ| x ∈ (r(-1), r1)} . (r0 < rcos(x))
Lemma: rcos-positive-initially
∀x:{x:ℝ| x ∈ [r0, (r(1570796326)/r(1000000000))]} . (r0 < rcos(x))
Definition: addrcos
addrcos(x) ==
λn.eval m = 16 * n in
eval xm = x m in
eval z = cosine((r(xm))/2 * m) m in
(((m * z) ÷ 4 * m) + (xm ÷ 4)) ÷ 4
Lemma: addrcos_wf
∀[x:ℝ]. (addrcos(x) ∈ ℕ+ ⟶ ℤ)
Lemma: addrcos_wf2
∀[x:ℝ]. (addrcos(x) ∈ {f:ℕ+ ⟶ ℤ| f = (x + rcos(x))} )
Definition: radd_rcos
radd_rcos(x) == accelerate(3;addrcos(x))
Lemma: radd_rcos_wf
∀[x:ℝ]. (radd_rcos(x) ∈ {y:ℝ| y = (x + rcos(x))} )
Lemma: radd_rcos_functionality
∀[x,y:ℝ]. radd_rcos(x) = radd_rcos(y) supposing x = y
Lemma: derivative-radd_rcos
d(radd_rcos(x))/dx = λx.r1 - rsin(x) on (-∞, ∞)
Lemma: radd_rcos-deriv-seq
finite-deriv-seq((-∞, ∞);3;i,x.if (i =z 0) then radd_rcos(x)
if (i =z 1) then r1 - rsin(x)
if (i =z 2) then -(rcos(x))
else rsin(x)
fi )
Definition: rcos-seq
rcos-seq(n) == primrec(n;(r(1570796326))/1000000000;λi,x. radd_rcos(x))
Lemma: rcos-seq_wf
∀[n:ℕ]. (rcos-seq(n) ∈ ℝ)
Lemma: rcos-seq-step
∀[n:ℕ]. (rcos-seq(n + 1) = (rcos-seq(n) + rcos(rcos-seq(n))))
Lemma: rcos-seq-positive
∀n:ℕ. ((r0 < rcos-seq(n)) ∧ (∀t:{t:ℝ| t ∈ [r0, rcos-seq(n)]} . (r0 < rcos(t))))
Lemma: rcos-seq-increasing
∀n:ℕ. (rcos-seq(n) < rcos-seq(n + 1))
Lemma: rcos-seq-differences
∀n:ℕ. (0 < n ⇒ ((rcos-seq(n + 1) - rcos-seq(n)) ≤ ((r1 - rsin(rcos-seq(n - 1))) * (rcos-seq(n) - rcos-seq(n - 1)))))
Lemma: increasing-sequence-converges
∀x:ℕ ⟶ ℝ
((∀n:ℕ. ((x n) < (x (n + 1))))
⇒ (∃c:{2...}
∃m:ℕ+
((∀n:ℕ+. (((x (n + 1)) - x n) ≤ ((r1/r(c)) * ((x n) - x (n - 1)))))
∧ ((r(c) * ((x 1) - x 0)/r(c - 1)) ≤ (r1/r(m)))))
⇒ x n↓ as n→∞)
Lemma: rcos-seq-converges
rcos-seq(n)↓ as n→∞
Lemma: rcos-seq-converges-ext
rcos-seq(n)↓ as n→∞
Definition: half-pi
This definition of π/2 is the real that rcos-seq(n) converges to as n -> ∞.
It is displayed with (slower) because we later define another real number
that is equal to this one but computes faster (and we take that to be our
"official" definition of π/2.⋅
π/2(slower) ==
λn.eval m = 4 * n in
eval n = exp-ratio(1;3164556962025316455;0;m;1000000000) + 1 in
(rcos-seq(n) m) ÷ 4
Lemma: half-pi_wf
π/2(slower) ∈ ℝ
Lemma: half-pi-positive
r0 < π/2(slower)
Lemma: half-pi-interval-proper
iproper((-(π/2(slower)), π/2(slower)))
Lemma: rcos-seq-converges-to-half-pi
lim n→∞.rcos-seq(n) = π/2(slower)
Lemma: rcos-half-pi
rcos(π/2(slower)) = r0
Lemma: rsin-half-pi
rsin(π/2(slower)) = r1
Lemma: radd_rcos-Taylor
∀b:ℝ. (|radd_rcos(b) - π/2(slower)| ≤ (|b - π/2(slower)|^3/r(2)))
Definition: fastpi
fastpi(n) ==
primrec(n;λn.eval m = 4 * n in
(m * 314159265358979323846) ÷ 400000000000000000000;λi,x. eval j = i + 1 in
eval N = 2 * 10^20 * 3^j in
(radd_rcos(x) within 1/N))
Lemma: fastpi_wf
∀n:ℕ. (fastpi(n) ∈ ℝ)
Lemma: fastpi-property
∀n:ℕ. (|fastpi(n) - π/2(slower)| ≤ (r1/r(10^(20 * 3^n))))
Definition: cubic_converge
cubic_converge(b;m)==r if m ≤z b then 0 else eval r = iroot(3;m) + 1 in eval n = cubic_converge(b;r) in n + 1 fi
Lemma: cubic_converge_wf
∀b:{9...}. ∀m:ℕ. (cubic_converge(b;m) ∈ {n:ℕ| m ≤ b^3^n} )
Definition: cubic_converge2
cubic_converge2(a;b;k;m)
==r if a * m ≤z b
then 0
else if m=2 then k else eval r = iroot(3;m) + 1 in eval n = cubic_converge2(a;b;k;r) in n + 1
fi
Lemma: cubic_converge2_wf
∀a:ℕ+. ∀b:{a + 1...}. ∀k:{k:ℕ| (2 * a^3^k) ≤ b^3^k} . ∀m:ℕ. (cubic_converge2(a;b;k;m) ∈ {n:ℕ| (a^3^n * m) ≤ b^3^n} )
Lemma: fastpi-converges
lim n→∞.fastpi(n) = π/2(slower)
Lemma: fastpi-converges-ext
lim n→∞.fastpi(n) = π/2(slower)
Definition: halfpi
π/2 == λn.eval m = 4 * n in eval m2 = 2 * m in eval N = cubic_converge(100000000000000000000;m2) in fastpi(N) m ÷ 4
Lemma: halfpi_wf1
π/2 ∈ {x:ℝ| x = π/2(slower)}
Lemma: halfpi_wf
π/2 ∈ ℝ
Lemma: halfpi-half-pi
π/2 = π/2(slower)
Lemma: halfpi-positive
r0 < π/2
Lemma: halfpi-interval-proper
iproper((-(π/2), π/2))
Lemma: rcos-halfpi
rcos(π/2) = r0
Lemma: rsin-halfpi
rsin(π/2) = r1
Lemma: rcos-positive-before-half-pi
∀x:{x:ℝ| x ∈ [r0, π/2)} . (r0 < rcos(x))
Lemma: rsin-shift-half-pi
∀[x:ℝ]. (rsin(x + π/2) = rcos(x))
Lemma: rcos-shift-half-pi
∀[x:ℝ]. (rcos(x + π/2) = -(rsin(x)))
Definition: pi
π == 2 * π/2
Lemma: pi_wf
π ∈ ℝ
Lemma: pi-positive
r0 < π
Lemma: rsin-shift-pi
∀[x:ℝ]. (rsin(x + π) = -(rsin(x)))
Lemma: rcos-shift-pi
∀[x:ℝ]. (rcos(x + π) = -(rcos(x)))
Lemma: rcos-pi
rcos(π) = -(r1)
Lemma: rsin-pi
rsin(π) = r0
Lemma: rsin-shift-2pi
∀[x:ℝ]. (rsin(x + 2 * π) = rsin(x))
Lemma: rcos-shift-2pi
∀[x:ℝ]. (rcos(x + 2 * π) = rcos(x))
Lemma: rsin-first-req-1
∀x:ℝ. ((r0 ≤ x) ⇒ (rsin(x) = r1) ⇒ (π/2 ≤ x))
Lemma: rcos-nonneg-upto-half-pi
∀x:{x:ℝ| x ∈ [r0, π/2]} . (r0 ≤ rcos(x))
Lemma: rcos-nonneg
∀x:{x:ℝ| x ∈ [-(π/2), π/2]} . (r0 ≤ rcos(x))
Lemma: rcos-nonpositive
∀x:{x:ℝ| x ∈ [π/2, π + π/2]} . (rcos(x) ≤ r0)
Lemma: rcos-positive
∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (r0 < rcos(x))
Lemma: rsin-positive
∀x:{x:ℝ| x ∈ (r0, π)} . (r0 < rsin(x))
Lemma: rsin-nonneg
∀x:{x:ℝ| x ∈ [r0, π]} . (r0 ≤ rsin(x))
Lemma: rsin-strict-bound
∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (rsin(x) ∈ (r(-1), r1))
Lemma: rsin-strictly-increasing
rsin(x) strictly-increasing for x ∈ (-(π/2), π/2)
Lemma: rsin-strictly-increasing2
rsin(x) strictly-increasing for x ∈ [-(π/2), π/2]
Lemma: rcos-strictly-decreasing
rcos(x) strictly-decreasing for x ∈ [r0, π]
Lemma: rcos-1-implies-at-least-2pi
∀x:{x:ℝ| r0 < x} . ((rcos(x) = r1) ⇒ (2 * π ≤ x))
Lemma: rcos-is-1
∀n:ℤ. (rcos(2 * n * π) = r1)
Lemma: period-rsin-is-2pi
∀a:ℝ. ((r0 < a) ⇒ (∀x:ℝ. (rsin(x + a) = rsin(x))) ⇒ (2 * π ≤ a))
Lemma: period-rcos-is-2pi
∀a:ℝ. ((r0 < a) ⇒ (∀x:ℝ. (rcos(x + a) = rcos(x))) ⇒ (2 * π ≤ a))
Lemma: rcos-nonzero-on
rcos(x)≠r0 for x ∈ (-(π/2), π/2)
Definition: rtan
rtan(x) == (rsin(x)/rcos(x))
Lemma: rtan_wf
∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . (rtan(x) ∈ ℝ)
Lemma: rtan_functionality
∀x:{x:ℝ| x ∈ (-(π/2), π/2)} . ∀[y:ℝ]. rtan(x) = rtan(y) supposing x = y
Lemma: rtan0
rtan(r0) = r0
Lemma: derivative-rtan
d(rtan(x))/dx = λx.(r1/rcos(x)^2) on (-(π/2), π/2)
Lemma: rtan_functionality_wrt_rleq
∀[x,y:{x:ℝ| x ∈ (-(π/2), π/2)} ]. rtan(x) ≤ rtan(y) supposing x ≤ y
Lemma: rtan_functionality_wrt_rless
∀x,y:{x:ℝ| x ∈ (-(π/2), π/2)} . rtan(x) < rtan(y) supposing x < y
Lemma: rtan_one_one
∀x,y:{x:ℝ| x ∈ (-(π/2), π/2)} . x = y supposing rtan(x) = rtan(y)
Lemma: rtan-radd-denom-positive
∀x,y:{x:ℝ| x ∈ (-(π/2), π/2)} .
(r0 < rcos(x)) ∧ (r0 < rcos(y)) ∧ (r0 < (r1 - rtan(x) * rtan(y))) supposing x + y ∈ (-(π/2), π/2)
Lemma: rtan-radd
∀[x,y:{x:ℝ| x ∈ (-(π/2), π/2)} ].
rtan(x + y) = (rtan(x) + rtan(y)/r1 - rtan(x) * rtan(y)) supposing x + y ∈ (-(π/2), π/2)
Lemma: rtan-double
∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. rtan(r(2) * x) = (r(2) * rtan(x)/r1 - rtan(x)^2) supposing r(2) * x ∈ (-(π/2), π/2)
Lemma: rsin-pi-over-4
rsin((π/r(4))) = (r1/rsqrt(r(2)))
Lemma: rcos-pi-over-4
rcos((π/r(4))) = (r1/rsqrt(r(2)))
Lemma: rtan-pi-over-4
rtan((π/r(4))) = r1
Lemma: rtan-rminus
∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. (rtan(-(x)) = -(rtan(x)))
Lemma: rtan-rsub
∀[x,y:{x:ℝ| x ∈ (-(π/2), π/2)} ].
rtan(x - y) = (rtan(x) - rtan(y)/r1 + (rtan(x) * rtan(y))) supposing x - y ∈ (-(π/2), π/2)
Definition: arctangent
arctangent(x) == r0_∫-x (r1/r1 + t^2) dt
Lemma: arctangent_wf
∀[x:ℝ]. (arctangent(x) ∈ ℝ)
Lemma: derivative-arctangent
d(arctangent(x))/dx = λx.(r1/r1 + x^2) on (-∞, ∞)
Lemma: arctangent_functionality
∀[x,y:ℝ]. arctangent(x) = arctangent(y) supposing x = y
Lemma: arctangent_functionality_wrt_rless
∀x,y:ℝ. arctangent(x) < arctangent(y) supposing x < y
Lemma: arctangent_one_one
∀x,y:ℝ. x = y supposing arctangent(x) = arctangent(y)
Lemma: arctangent0
arctangent(r0) = r0
Lemma: arctangent-rtan
∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. (arctangent(rtan(x)) = x)
Lemma: arctangent-bounds
∀x:ℝ. (arctangent(x) ∈ (-(π/2), π/2))
Lemma: rtan-arctangent
∀[x:ℝ]. (rtan(arctangent(x)) = x)
Lemma: arctangent-rleq
∀x:ℝ. arctangent(x) ≤ x supposing r0 ≤ x
Lemma: Machin-lemma
(π/r(4)) = ((r(4) * arctangent((r1/r(5)))) - arctangent((r1/r(239))))
Lemma: Machin-formula
π = ((r(16) * arctangent((r1/r(5)))) - r(4) * arctangent((r1/r(239))))
Lemma: arctangent1
arctangent(r1) = (π/r(4))
Lemma: arctangent-rminus
∀[x:ℝ]. (arctangent(-(x)) = -(arctangent(x)))
Lemma: arctangent-chain-rule
∀I:Interval. ∀f,f':I ⟶ℝ.
(iproper(I)
⇒ (∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on I
⇒ d(arctangent(f[x]))/dx = λx.(f'[x]/r1 + f[x]^2) on I)
Lemma: arctangent-rinv
∀[x:{x:ℝ| x ∈ (r0, ∞)} ]. (arctangent(rinv(x)) = (π/2 - arctangent(x)))
Lemma: arctangent-negative-rinv
∀[x:{x:ℝ| x ∈ (-∞, r0)} ]. (arctangent(rinv(x)) = (-(π/2) - arctangent(x)))
Definition: arctan-poly
arctan-poly(x;k) == Σ{(if (i rem 2 =z 0) then x^(2 * i) + 1 else -(x^(2 * i) + 1) fi )/(2 * i) + 1 | 0≤i≤k}
Lemma: arctan-poly_wf
∀[x:ℝ]. ∀[k:ℕ]. (arctan-poly(x;k) ∈ ℝ)
Lemma: arctan-poly-approx-1
∀[x:{x:ℝ| r0 ≤ x} ]. ∀[k:ℕ]. (|arctangent(x) - arctan-poly(x;k)| ≤ (x^(2 * k) + 3/r((2 * k) + 3)))
Lemma: arctan-poly-approx
∀[x:ℝ]. ∀[k:ℕ]. (|arctangent(x) - arctan-poly(x;k)| ≤ (|x|^(2 * k) + 3/r((2 * k) + 3)))
Definition: atan-approx
atan-approx(k;x;N) ==
eval u = poly-approx(λi.(r(if (i rem 2 =z 0) then 1 else -1 fi ))/(2 * i) + 1;x * x;k;2 * N) in
eval b = |u| + 1 in
eval z = x b in
(u * z) ÷ 4 * b
Lemma: atan-approx_wf
∀[k:ℕ]. ∀[x:ℝ]. ∀[N:ℕ+]. (atan-approx(k;x;N) ∈ ℤ)
Lemma: atan-approx-property
∀[k:ℕ]. ∀[x:ℝ]. ∀[N:ℕ+]. ((|x| ≤ (r1/r(2))) ⇒ 1-approx(arctan-poly(x;k);N;atan-approx(k;x;N)))
Definition: gen_log_aux
gen_log_aux(p;c;x;i;n;M)
==r if M ≤z c * p then n else eval p' = x * p in eval c' = c + i in eval n' = n + 1 in gen_log_aux(p';c';x;i;n';M) fi
Lemma: gen_log_aux_wf
∀[p,c:ℕ+]. ∀[x:{2...}]. ∀[i,n:ℕ]. ∀[M:ℤ].
(gen_log_aux(p;c;x;i;n;M) ∈ {k:{n...}| M ≤ ((c + ((k - n) * i)) * p * x^(k - n))} )
Definition: atan-log
atan-log(a;M) == gen_log_aux(a^3;3;a^2;2;0;M)
Lemma: atan-log_wf
∀[a:{2...}]. ∀[M:ℤ]. (atan-log(a;M) ∈ {k:ℕ| M ≤ (((2 * k) + 3) * a^((2 * k) + 3))} )
Definition: atan_approx
atan_approx(a;x;M) == eval k = atan-log(a;M) in atan-approx(k;x;M)
Lemma: atan_approx_wf
∀[a:{2...}]. ∀[x:ℝ]. ∀[N:ℕ+]. (atan_approx(a;x;N) ∈ ℤ)
Lemma: atan_approx-property
∀[a:{2...}]. ∀[x:ℝ]. ∀[N:ℕ+].
|arctangent(x) - (r(atan_approx(a;x;N))/r(2 * N))| ≤ (r(2)/r(N)) supposing |x| ≤ (r1/r(a))
Definition: atan
atan(a;x) == accelerate(2;λN.atan_approx(a;x;N))
Lemma: atan_wf
∀[a:{2...}]. ∀[x:ℝ]. atan(a;x) ∈ {y:ℝ| arctangent(x) = y} supposing |x| ≤ (r1/r(a))
Definition: MachinPi4
MachinPi4() == 4 * atan(5;(r1)/5) - atan(239;(r1)/239)
Lemma: MachinPi4_wf
MachinPi4() ∈ {x:ℝ| x = (π/r(4))}
Lemma: 2-MachinPi4
2 * MachinPi4() = π/2
Lemma: MachinPi4-req
MachinPi4() = (π/r(4))
Lemma: MachinPi4-positive
r0 < MachinPi4()
Lemma: pi-irrational-instance
∃k:ℕ. (((r1)/k + 2 < |(r(22))/7 - 4 * MachinPi4()|) ∧ (|(r(22))/7 - 4 * MachinPi4()| < (r1)/k + 1))
Lemma: rsin-shift-2n-pi
∀x:ℝ. ∀M:ℤ. (rsin(x + (r(M) * 2 * π)) = rsin(x))
Lemma: rcos-shift-2n-pi
∀x:ℝ. ∀M:ℤ. (rcos(x + (r(M) * 2 * π)) = rcos(x))
Lemma: rcos-is-1-iff
∀x:ℝ. (rcos(x) = r1 ⇐⇒ ∃n:ℤ. (x = 2 * n * π))
Lemma: req-rcos-and-rsin-implies
∀x,y:ℝ. ((rsin(x) = rsin(y)) ⇒ (rcos(x) = rcos(y)) ⇒ (∃n:ℤ. ((x - y) = 2 * n * π)))
Definition: reduce-halfpi
reduce-halfpi(x) == reduce-real(x;2 * MachinPi4();4)
Lemma: reduce-halfpi_wf
∀[x:ℝ]. (reduce-halfpi(x) ∈ {n:ℤ| |x - r(n) * π/2| ≤ r(2)} )
Lemma: rcos-reduce-half-pi
∀[n:ℤ]. ∀[x:ℝ].
(rcos(x - n * π/2)
= if (n mod 4 =z 0) then rcos(x)
if (n mod 4 =z 2) then -(rcos(x))
if (n mod 4 =z 1) then rsin(x)
else -(rsin(x))
fi )
Lemma: rsin-reduce-half-pi
∀[n:ℤ]. ∀[x:ℝ].
(rsin(x - n * π/2)
= if (n mod 4 =z 0) then rsin(x)
if (n mod 4 =z 2) then -(rsin(x))
if (n mod 4 =z 1) then -(rcos(x))
else rcos(x)
fi )
Definition: rsine
rsine(x) ==
eval n = reduce-halfpi(x) in
eval i = n mod 4 in
if (i =z 0) then sine-medium(x - n * 2 * MachinPi4())
if (i =z 2) then -(sine-medium(x - n * 2 * MachinPi4()))
if (i =z 1) then cosine-medium(x - n * 2 * MachinPi4())
else -(cosine-medium(x - n * 2 * MachinPi4()))
fi
Lemma: rsine_wf
∀[x:ℝ]. (rsine(x) ∈ {y:ℝ| y = rsin(x)} )
Definition: rcosine
rcosine(x) ==
eval n = reduce-halfpi(x) in
eval i = n mod 4 in
if (i =z 0) then cosine-medium(x - n * 2 * MachinPi4())
if (i =z 2) then -(cosine-medium(x - n * 2 * MachinPi4()))
if (i =z 1) then -(sine-medium(x - n * 2 * MachinPi4()))
else sine-medium(x - n * 2 * MachinPi4())
fi
Lemma: rcosine_wf
∀[x:ℝ]. (rcosine(x) ∈ {y:ℝ| y = rcos(x)} )
Lemma: rsin-shift-MachinPi4
∀x:ℝ. ∀M:ℤ. (rsin(x - 8 * M * MachinPi4()) = rsin(x))
Lemma: arctangent-reduction
∀B:{B:ℝ| r0 < B} . ∀x:{x:ℝ| (r(-1)/B) < x} . (arctangent(x) = (arctangent(B) + arctangent((x - B/r1 + (x * B)))))
Lemma: arctangent-reduction-1
∀x:{x:ℝ| r(-1) < x} . (arctangent(x) = (MachinPi4() + arctangent((x - r1/r1 + x))))
Definition: atan-size-bound
atan-size-bound(x) == eval z = |x| 1000 in imax(2000 ÷ z + 2;2)
Lemma: atan-size-bound_wf
∀[x:{x:ℝ| |x| ≤ (r1/r(2))} ]. (atan-size-bound(x) ∈ {a:{2...}| |x| ≤ (r1/r(a))} )
Definition: atan-small
atan-small(x) == atan(atan-size-bound(x);x)
Lemma: atan-small_wf
∀[x:ℝ]. atan-small(x) ∈ {y:ℝ| arctangent(x) = y} supposing |x| ≤ (r1/r(2))
Definition: full-arctan
full-arctan(x) ==
case rless-case((r(-1))/2;r0;8;x)
of inl(_) =>
case rless-case((r1)/3;(r1)/2;16;x)
of inl(_) =>
case rless-case(r(2);r(3);4;x)
of inl(_) =>
2 * MachinPi4() - atan-small((r1/x))
| inr(_) =>
MachinPi4() + atan-small((x - r1/r1 + x))
| inr(_) =>
atan-small(x)
| inr(_) =>
-(case rless-case((r1)/3;(r1)/2;16;-(x))
of inl(_) =>
case rless-case(r(2);r(3);4;-(x))
of inl(_) =>
2 * MachinPi4() - atan-small((r1/-(x)))
| inr(_) =>
MachinPi4() + atan-small((-(x) - r1/r1 + -(x)))
| inr(_) =>
atan-small(-(x)))
Lemma: full-arctan_wf
∀[x:ℝ]. (full-arctan(x) ∈ {y:ℝ| y = arctangent(x)} )
Definition: arctan
arctan(x) == approx-arg(λ2x.full-arctan(x);1;x)
Lemma: arctan_wf1
∀[x:ℝ]. (arctan(x) ∈ {y:ℝ| y = arctangent(x)} )
Lemma: arctan_wf
∀[x:ℝ]. (arctan(x) ∈ ℝ)
Lemma: arctan-is-arctangent
∀[x:ℝ]. (arctan(x) = arctangent(x))
Definition: faster-sin
faster-sin(x) == eval N = 8 * ((((x/MachinPi4()))/8 1) ÷ 2) in rsin(x - N * MachinPi4())
Lemma: faster-sin_wf
∀[x:ℝ]. (faster-sin(x) ∈ {y:ℝ| y = rsin(x)} )
Definition: rlog
rlog(x) == r1_∫-x (r1/t) dt
Lemma: rlog_wf
∀[x:{x:ℝ| r0 < x} ]. (rlog(x) ∈ ℝ)
Lemma: rlog1
rlog(r1) = r0
Lemma: rlog_functionality
∀[x:{x:ℝ| r0 < x} ]. ∀[y:ℝ]. rlog(x) = rlog(y) supposing x = y
Lemma: derivative-rlog
d(rlog(x))/dx = λx.(r1/x) on (r0, ∞)
Lemma: rlog_functionality_wrt_rless
∀x,y:{t:ℝ| r0 < t} . ((x < y) ⇒ (rlog(x) < rlog(y)))
Lemma: rlog_functionality_wrt_rleq
∀x,y:{t:ℝ| r0 < t} . ((x ≤ y) ⇒ (rlog(x) ≤ rlog(y)))
Lemma: rlog-difference-bound
∀x,y:ℝ. ((r0 < x) ⇒ (x < y) ⇒ ((rlog(y) - rlog(x)) ≤ (y - x/x)))
Lemma: rabs-rlog-difference-bound
∀x,y:ℝ. ((r0 < x) ⇒ (r0 < y) ⇒ (|rlog(y) - rlog(x)| ≤ (|y - x|/rmin(x;y))))
Lemma: rlog-rmul
∀x,y:{t:ℝ| r0 < t} . (rlog(x * y) = (rlog(x) + rlog(y)))
Lemma: rlog-rdiv
∀x,y:{t:ℝ| r0 < t} . (rlog((x/y)) = (rlog(x) - rlog(y)))
Lemma: rlog-inv
∀y:{t:ℝ| r0 < t} . (rlog((r1/y)) = -(rlog(y)))
Lemma: rlog-rexp
∀[x:ℝ]. (rlog(e^x) = x)
Lemma: rlog-integral-non-zero
∀a,b:ℝ. ((r0 < a) ⇒ (a < b) ⇒ (¬(∫ (r1/t) dt on [a, b] = r0)))
Lemma: rexp-rlog
∀[x:{x:ℝ| r0 < x} ]. (e^rlog(x) = x)
Definition: log-contraction
log-contraction(a;x) == x + (r(2) * (a - e^x/a + e^x))
Lemma: log-contraction_wf
∀[a,x:ℝ]. log-contraction(a;x) ∈ ℝ supposing r0 < a
Definition: lgc
lgc(a;x) == (x - r(2)) + 4 * (a/a + real_exp(x))
Lemma: lgc_wf
∀[a,x:ℝ]. lgc(a;x) ∈ ℝ supposing r0 < a
Lemma: lgc-req
∀[a,x:ℝ]. lgc(a;x) = log-contraction(a;x) supposing r0 < a
Lemma: derivative-log-contraction
∀a:{a:ℝ| r0 < a} . d(log-contraction(a;x))/dx = λx.(a - e^x/a + e^x)^2 on (-∞, ∞)
Lemma: derivative-log-contraction-bound
∀a:{a:ℝ| r0 < a} . ∀[x:ℝ]. (|(a - e^x/a + e^x)^2| ≤ r1)
Lemma: second-derivative-log-contraction
∀a:{a:ℝ| r0 < a} . d((a - e^x/a + e^x)^2)/dx = λx.(((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3) on (-∞, ∞)
Lemma: third-derivative-log-contraction
∀a:{a:ℝ| r0 < a}
d((((r(-4) * a) * e^x) * (a - e^x)/a + e^x^3))/dx = λx.(((r(16) * a^2) * e^x^2)
+ ((r(-4) * a^3) * e^x)
+ ((r(-4) * a) * e^x^3)/a + e^x^4) on (-∞, ∞)
Lemma: third-derivative-log-contraction-bound
∀a:{a:ℝ| r0 < a} . ∀x:ℝ.
((((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4) ≤ (r1/r(2)))
Lemma: third-derivative-log-contraction-nonneg
∀a:{a:ℝ| r0 < a} . ∀x:ℝ.
((|x - rlog(a)| ≤ r1) ⇒ (r0 ≤ (((r(16) * a^2) * e^x^2) + ((r(-4) * a^3) * e^x) + ((r(-4) * a) * e^x^3)/a + e^x^4)))
Lemma: log-contraction-Taylor
∀[a,x:ℝ]. |log-contraction(a;x) - rlog(a)| ≤ ((r1/r(4)) * |x - rlog(a)|^3) supposing (r0 < a) ∧ (|x - rlog(a)| ≤ r1)
Definition: logseq
logseq(a;b;n) ==
primrec(n;b;λi,x. eval j = i + 1 in
eval N = 4 * 10^3^j in
eval xx = x N in
eval N2 = 2 * N in
(lgc(a;(r(xx))/N2) within 1/N))
Lemma: logseq_wf
∀[a:{a:ℝ| r0 < a} ]. ∀[b:ℝ]. ∀[n:ℕ]. (logseq(a;b;n) ∈ ℝ)
Lemma: logseq-property
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . ∀n:ℕ. (|logseq(a;b;n) - rlog(a)| ≤ (r1/r(10^3^n)))
Lemma: logseq-converges
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . lim n→∞.logseq(a;b;n) = rlog(a)
Lemma: logseq-converges-ext
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . lim n→∞.logseq(a;b;n) = rlog(a)
Definition: log-from
log-from(a;b) == λn.eval m = 4 * n in eval m2 = 2 * m in eval N = cubic_converge(10;m2) in logseq(a;b;N) m ÷ 4
Lemma: log-from_wf
∀a:{a:ℝ| r0 < a} . ∀b:{b:ℝ| |b - rlog(a)| ≤ (r1/r(10))} . (log-from(a;b) ∈ {x:ℝ| x = rlog(a)} )
Lemma: near-log-exists
∀a:{a:ℝ| r0 < a} . ∀N:ℕ+. ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
Lemma: near-log-exists-ext
∀a:{a:ℝ| r0 < a} . ∀N:ℕ+. ∃m:ℕ+. (∃z:ℤ [(|(r(z))/m - rlog(a)| ≤ (r1/r(N)))])
Definition: near-log
near-log(a;N) == TERMOF{near-log-exists-ext:o, 1:l} a N
Lemma: near-log_wf
∀[a:{a:ℝ| r0 < a} ]. ∀[N:ℕ+]. (near-log(a;N) ∈ {r:ℕ+ × ℤ| let j,c = r in |(r(c))/j - rlog(a)| ≤ (r1/r(N))} )
Definition: ln
ln(a) == let j,c = near-log(a;10) in log-from(a;(r(c))/j)
Lemma: ln_wf
∀a:{a:ℝ| r0 < a} . (ln(a) ∈ {x:ℝ| x = rlog(a)} )
Lemma: ln-req
∀[a:{a:ℝ| r0 < a} ]. (ln(a) = rlog(a))
Lemma: ln_functionality
∀[a:{a:ℝ| r0 < a} ]. ∀[b:ℝ]. ln(a) = ln(b) supposing a = b
Lemma: log-by-IVT
∀a:{a:ℝ| r0 < a} . ∃x:ℝ. (x = rlog(a))
Definition: IVTlog
IVTlog(a) == fst((TERMOF{log-by-IVT:o, 1:l} a))
Lemma: IVTlog_wf
∀a:{a:ℝ| r0 < a} . (IVTlog(a) ∈ {x:ℝ| x = rlog(a)} )
Lemma: rexp-rless
∀x,y:ℝ. (x < y ⇐⇒ e^x < e^y)
Lemma: rexp-rleq
∀x,y:ℝ. (x ≤ y ⇐⇒ e^x ≤ e^y)
Lemma: rabs-rexp-difference-bound
∀x,y:ℝ. (|e^x - e^y| ≤ (e^rmax(x;y) * |x - y|))
Lemma: real-upper-bound
∀[x:ℝ]. ∀[n:ℕ+]. (x ≤ r((((x n) + 1) ÷ 2 * n) + 1))
Lemma: cheap-real-upper-bound
∀[x:ℝ]. (x ≤ r((((x 1) + 1) ÷ 2) + 1))
Definition: approx-rexp
approx-rexp(x;n) ==
if n=0
then r0
else eval x1 = (((x 1) + 1) ÷ 2) + 1 in
eval c = if (x1) < (0) then 1 else 3^x1 in
eval nc = n * c in
eval m = 2 * nc in
eval a = (x m) - 2 in
(e^(r(a))/2 * m within 1/nc)
Lemma: approx-rexp_wf
∀[x:ℝ]. ∀[n:ℕ]. (approx-rexp(x;n) ∈ ℝ)
Lemma: converges-to-rexp
∀x:ℝ. lim n→∞.approx-rexp(x;n) = e^x
Lemma: converges-to-rexp-ext
∀x:ℝ. lim n→∞.approx-rexp(x;n) = e^x
Definition: expr
expr(x) ==
eval x1 = (((x 1) + 1) ÷ 2) + 1 in
cauchy-limit(n.if n=0
then r0
else eval c = if (x1) < (0) then 1 else 3^x1 in
eval nc = n * c in
eval m = 2 * nc in
eval a = (x m) - 2 in
(e^(r(a))/2 * m within 1/nc);λk.((2 * k) + ((2 * k) ÷ if (x1) < (0) then 1 else 3^x1) + 1))
Lemma: expr_wf
∀[x:ℝ]. (expr(x) ∈ {y:ℝ| y = e^x} )
Lemma: expr-req
∀[x:ℝ]. (expr(x) = e^x)
Lemma: expr_functionality
∀[x,y:ℝ]. expr(x) = expr(y) supposing x = y
Lemma: expr-ln
∀x:ℝ. ((r0 < x) ⇒ (expr(ln(x)) = x))
Lemma: ln-expr
∀x:ℝ. (ln(expr(x)) = x)
Lemma: ln-req-iff
∀[x:{x:ℝ| r0 < x} ]. ∀[y:ℝ]. uiff(ln(x) = y;x = expr(y))
Definition: fast-rexp
fast-rexp(x) ==
eval a = x 200 in
eval u = (r(a + 2))/400 in
eval l = (r(a - 2))/400 in
eval B = canonical-bound(e^u) in
approx-arg-interval(λx.e^x;l;u;B;x)
Lemma: fast-rexp_wf
∀[x:ℝ]. (fast-rexp(x) ∈ {y:ℝ| y = e^x} )
Lemma: rsqrt-as-rexp
∀[x:{x:ℝ| r0 < x} ]. (rsqrt(x) = e^(rlog(x)/r(2)))
Definition: realexp
realexp(x;y) == expr(y * ln(x))
Lemma: realexp_wf
∀[x:{x:ℝ| r0 < x} ]. ∀[y:ℝ]. (realexp(x;y) ∈ ℝ)
Lemma: realexp_functionality
∀[x1:{x:ℝ| r0 < x} ]. ∀[x2,y1,y2:ℝ]. (realexp(x1;y1) = realexp(x2;y2)) supposing ((y1 = y2) and (x1 = x2))
Lemma: realexp-radd
∀[x:{x:ℝ| r0 < x} ]. ∀[a,b:ℝ]. (realexp(x;a + b) = (realexp(x;a) * realexp(x;b)))
Lemma: realexp-nat
∀[x:{x:ℝ| r0 < x} ]. ∀[n:ℕ]. (realexp(x;r(n)) = x^n)
Lemma: derivative-rexp-function
∀I:Interval. ∀f,f':I ⟶ℝ.
(iproper(I)
⇒ (∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ d(f[x])/dx = λx.f'[x] on I
⇒ d(e^f[x])/dx = λx.e^f[x] * f'[x] on I)
Lemma: derivative-rsqrt
d(rsqrt(x))/dx = λx.(r1/r(2) * rsqrt(x)) on (r0, ∞)
Lemma: derivative-rsqrt-function
∀I:Interval
(iproper(I)
⇒ (∀f,f':I ⟶ℝ.
((∀x:{x:ℝ| x ∈ I} . (r0 < f[x]))
⇒ (∀x,y:{x:ℝ| x ∈ I} . ((x = y) ⇒ (f'[x] = f'[y])))
⇒ (∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a ≤ b)} . ∃c:{t:ℝ| t ∈ [a, b]} . ∀x:{t:ℝ| t ∈ [a, b]} . (f[c] ≤ f[x])\000C)
⇒ d(f[x])/dx = λx.f'[x] on I
⇒ d(rsqrt(f[x]))/dx = λx.(f'[x]/r(2) * rsqrt(f[x])) on I)))
Definition: cosh
cosh(x) == (expr(x) + expr(-(x)))/2
Lemma: cosh_wf
∀[x:ℝ]. (cosh(x) ∈ ℝ)
Definition: sinh
sinh(x) == (expr(x) - expr(-(x)))/2
Lemma: sinh_wf
∀[x:ℝ]. (sinh(x) ∈ ℝ)
Lemma: sinh0
sinh(r0) = r0
Lemma: cosh0
cosh(r0) = r1
Lemma: sinh_functionality
∀[x,y:ℝ]. sinh(x) = sinh(y) supposing x = y
Lemma: cosh_functionality
∀[x,y:ℝ]. cosh(x) = cosh(y) supposing x = y
Lemma: cosh2-sinh2
∀[x:ℝ]. ((cosh(x)^2 - sinh(x)^2) = r1)
Lemma: cosh-ge-1
∀[x:ℝ]. (r1 ≤ cosh(x))
Lemma: cosh-gt-1
∀x:ℝ. (x ≠ r0 ⇒ (r1 < cosh(x)))
Lemma: cosh-radd
∀[x,y:ℝ]. (cosh(x + y) = ((cosh(x) * cosh(y)) + (sinh(x) * sinh(y))))
Lemma: sinh-radd
∀[x,y:ℝ]. (sinh(x + y) = ((sinh(x) * cosh(y)) + (cosh(x) * sinh(y))))
Lemma: sinh-rminus
∀[x:ℝ]. (sinh(-(x)) = -(sinh(x)))
Lemma: cosh-rminus
∀[x:ℝ]. (cosh(-(x)) = cosh(x))
Definition: inv-sinh
inv-sinh(x) == ln(x + rsqrt((x * x) + r1))
Lemma: inv-sinh-domain
∀x:ℝ. ((r0 ≤ ((x * x) + r1)) ∧ (r0 < (x + rsqrt((x * x) + r1))))
Lemma: inv-sinh_wf
∀[x:ℝ]. (inv-sinh(x) ∈ ℝ)
Lemma: inv-sinh_functionality
∀[x,y:ℝ]. inv-sinh(x) = inv-sinh(y) supposing x = y
Lemma: rneq-inv-sinh
∀x,y:ℝ. (inv-sinh(x) ≠ inv-sinh(y) ⇒ x ≠ y)
Lemma: sinh-inv-sinh
∀[x:ℝ]. (sinh(inv-sinh(x)) = x)
Lemma: inv-sinh-sinh
∀[x:ℝ]. (inv-sinh(sinh(x)) = x)
Definition: inv-cosh
inv-cosh(x) == ln(x + rsqrt((x * x) - r1))
Lemma: inv-cosh_wf
∀[x:{x:ℝ| r1 ≤ x} ]. (inv-cosh(x) ∈ ℝ)
Lemma: cosh-inv-cosh
∀[x:{x:ℝ| r1 ≤ x} ]. (cosh(inv-cosh(x)) = x)
Lemma: derivative-sinh
d(sinh(x))/dx = λx.cosh(x) on (-∞, ∞)
Lemma: sinh-rleq
∀[x,y:ℝ]. sinh(x) ≤ sinh(y) supposing x ≤ y
Lemma: sinh-rless
∀x,y:ℝ. sinh(x) < sinh(y) supposing x < y
Lemma: rneq-sinh
∀x,y:ℝ. (sinh(x) ≠ sinh(y) ⇒ x ≠ y)
Lemma: rneq-cosh
∀x,y:ℝ. (cosh(x) ≠ cosh(y) ⇒ x ≠ y)
Lemma: derivative-cosh
d(cosh(x))/dx = λx.sinh(x) on (-∞, ∞)
Lemma: arcsine-root-bounds
∀t:ℝ. ((t ∈ (r(-1), r1)) ⇒ (r0 < (r1 - t * t)))
Definition: arcsine_deriv
arcsine_deriv(x) == (r1/rsqrt(r1 - x * x))
Lemma: arcsine_deriv_wf
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsine_deriv(x) ∈ ℝ)
Lemma: arcsine_deriv_functionality
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. ∀[y:ℝ]. arcsine_deriv(x) = arcsine_deriv(y) supposing x = y
Definition: arcsine
arcsine(x) == r0_∫-x arcsine_deriv(t) dt
Lemma: arcsine_wf
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsine(x) ∈ ℝ)
Lemma: derivative-arcsine
d(arcsine(x))/dx = λx.arcsine_deriv(x) on (r(-1), r1)
Lemma: arcsine_functionality
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. ∀[y:ℝ]. arcsine(x) = arcsine(y) supposing x = y
Lemma: arcsine_functionality_wrt_rless
∀x,y:{x:ℝ| x ∈ (r(-1), r1)} . ((x < y) ⇒ (arcsine(x) < arcsine(y)))
Lemma: arcsine0
arcsine(r0) = r0
Lemma: arcsine-rsin
∀[x:{x:ℝ| x ∈ (-(π/2), π/2)} ]. (arcsine(rsin(x)) = x)
Lemma: arcsine-bounds
∀x:{x:ℝ| x ∈ (r(-1), r1)} . (arcsine(x) ∈ (-(π/2), π/2))
Lemma: arcsine-rless
∀x:{x:ℝ| x ∈ (r(-1), r1)} . (arcsine(x) < π/2)
Lemma: rless-arcsine
∀x:{x:ℝ| x ∈ (r(-1), r1)} . (-(π/2) < arcsine(x))
Lemma: rsin-arcsine
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (rsin(arcsine(x)) = x)
Lemma: arcsine-nonneg
∀[x:{x:ℝ| x ∈ [r0, r1)} ]. (r0 ≤ arcsine(x))
Lemma: arcsine-unique
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. ∀[y:{y:ℝ| y ∈ (-(π/2), π/2)} ]. ((rsin(y) = x) ⇒ (arcsine(x) = y))
Lemma: arcsine-rminus
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsine(-(x)) = -(arcsine(x)))
Lemma: arcsine-shift
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. arcsine(x) = (π/2 - arcsine(rsqrt(r1 - x * x))) supposing r0 < x
Definition: arcsine-contraction
arcsine-contraction(a;x) == x + ((a * rcos(x)) - rsqrt(r1 - a * a) * rsin(x))
Lemma: arcsine-contraction_wf
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x:ℝ]. (arcsine-contraction(a;x) ∈ ℝ)
Lemma: arcsine-contraction-difference
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x,y:ℝ].
(|arcsine-contraction(a;x) - arcsine-contraction(a;y)| ≤ (r(3) * |x - y|))
Lemma: arcsine-contraction-Taylor2
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x:ℝ].
∀c:ℝ. |arcsine-contraction(a;x) - arcsine(a)| ≤ (c * |x - arcsine(a)|^3) supposing (|a| ≤ c) ∧ (rsqrt(r1 - a * a) ≤ c)
Lemma: arcsine-contraction-Taylor
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[x:ℝ].
∀c:ℝ
|arcsine-contraction(a;x) - arcsine(a)| ≤ (c * |x - arcsine(a)|^3)
supposing (r0 ≤ a) ∧ (a ≤ c) ∧ (rsqrt(r1 - a * a) ≤ c)
Definition: iter-arcsine-contraction
arcsine-contraction^n(a) == λx.arcsine-contraction(a;x)^n a
Lemma: iter-arcsine-contraction_wf
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[n:ℕ]. (arcsine-contraction^n(a) ∈ ℝ)
Definition: approx-iter-arcsine
approx-iter-arcsine(a;k;n)
==r if (n =z 0)
then a k
else eval m = n - 1 in
eval k6 = 6 * k in
eval k12 = 2 * k6 in
eval y = approx-iter-arcsine(a;k6;m) in
arcsine-contraction(a;(r(y))/k12) k
fi
Lemma: approx-iter-arcsine_wf
∀[a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} ]. ∀[n:ℕ]. ∀[k:ℕ+].
(approx-iter-arcsine(a;k;n) ∈ {y:ℤ| |arcsine-contraction^n(a) - (r(y))/2 * k| ≤ (r(2)/r(k))} )
Lemma: iter-arcsine-contraction-property2
∀a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} . ∀n:ℕ. (|arcsine-contraction^n(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^n)
Lemma: iter-arcsine-contraction-property
∀a:{a:ℝ| (r(-1) < a) ∧ (a < r1)} . ((r0 ≤ a) ⇒ (∀n:ℕ. (|arcsine-contraction^n(a) - arcsine(a)| ≤ |a - arcsine(a)|^3^n))\000C)
Lemma: arcsine-bounds2
∀x:{x:ℝ| (r0 < x) ∧ (x < (r(3)/r(4)))} . (|arcsine(x) - x| < (r1/r(10)))
Definition: arcsine-approx
arcsine-approx(a;n) ==
eval n2 = 2 * n in
eval nn = cubic_converge(10;n2) in
eval n4 = 2 * n2 in
eval y = approx-iter-arcsine(a;n4;nn) in
(r(y))/2 * n4
Lemma: arcsine-approx_wf
∀a:{a:ℝ| ((r(-3)/r(4)) < a) ∧ (a < (r(3)/r(4)))} . ∀n:ℕ+. (arcsine-approx(a;n) ∈ {x:ℝ| |x - arcsine(a)| ≤ (r1/r(n))} )
Definition: partial-arcsin
partial-arcsin(a) == real-from-approx(n.arcsine-approx(a;n))
Lemma: partial-arcsin_wf
∀a:{a:ℝ| ((r(-3)/r(4)) < a) ∧ (a < (r(3)/r(4)))} . (partial-arcsin(a) ∈ {x:ℝ| x = arcsine(a)} )
Definition: full-arcsin
full-arcsin(a) ==
case rless-case((r(73))/100;(r(3))/4;110;|a|)
of inl(u) =>
case rless-case(r0;(r1)/2;10;a)
of inl(u) =>
2 * MachinPi4() - partial-arcsin(rsqrt(r1 - a * a))
| inr(v) =>
partial-arcsin(rsqrt(r1 - a * a)) - 2 * MachinPi4()
| inr(v) =>
partial-arcsin(a)
Lemma: full-arcsin_wf
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (full-arcsin(a) ∈ {x:ℝ| (x ∈ [-(π/2), π/2]) ∧ (rsin(x) = a)} )
Lemma: small-arcsine
∀N:ℕ+. ∀a:ℝ. ((|a| ≤ (r1/r(N + 1))) ⇒ (|arcsine(a)| ≤ (r1/r(N))))
Lemma: near-arcsine-exists
∀a:{a:ℝ| a ∈ (r(-1), r1)} . ∀N:ℕ+. (∃y:ℝ [(|y - arcsine(a)| ≤ (r1/r(N)))])
Lemma: near-arcsine-exists-ext
∀a:{a:ℝ| a ∈ (r(-1), r1)} . ∀N:ℕ+. (∃y:ℝ [(|y - arcsine(a)| ≤ (r1/r(N)))])
Definition: near-arcsine
near-arcsine(a;N) ==
eval b = a 4000 in
if (4) < (b)
then eval b = a 400 in
if (588) < (b)
then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
else if (b + 4) < (584) then arcsine-approx(a;N) else arcsine-approx(a;N)
else if (b + 4) < (0)
then -(eval b = -(a) 400 in
if (588) < (b)
then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
else if (b + 4) < (584) then arcsine-approx(-(a);N) else arcsine-approx(-(a);N))
else eval m = 4 * (N + 1) in
eval a@0 = r0 m in
eval b = a m in
if (a@0 + 4) < (b)
then eval b = a 400 in
if (588) < (b)
then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - a * a);2 * N)
else if (b + 4) < (584) then arcsine-approx(a;N) else arcsine-approx(a;N)
else if (b + 4) < (a@0)
then -(eval b = -(a) 400 in
if (588) < (b)
then (π/2 within 1/2 * N) - arcsine-approx(rsqrt(r1 - -(a) * -(a));2 * N)
else if (b + 4) < (584)
then arcsine-approx(-(a);N)
else arcsine-approx(-(a);N))
else r0
Lemma: near-arcsine_wf
∀a:{a:ℝ| a ∈ (r(-1), r1)} . ∀N:ℕ+. (near-arcsine(a;N) ∈ {y:ℝ| |y - arcsine(a)| ≤ (r1/r(N))} )
Definition: alt-arcsin
alt-arcsin(a) == real-from-approx(n.near-arcsine(a;n))
Lemma: alt-arcsin_wf
∀[a:{a:ℝ| a ∈ (r(-1), r1)} ]. (alt-arcsin(a) ∈ {y:ℝ| y = arcsine(a)} )
Definition: arcsin
arcsin(a) == full-arcsin(a)
Lemma: arcsin_wf
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arcsin(a) ∈ {x:ℝ| (x ∈ [-(π/2), π/2]) ∧ (rsin(x) = a)} )
Lemma: rsin-arcsin
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (rsin(arcsin(a)) = a)
Lemma: rcos-arcsin
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (rcos(arcsin(a)) = rsqrt(r1 - a * a))
Lemma: arcsin-bounds
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arcsin(a) ∈ [-(π/2), π/2])
Lemma: arcsin-unique
∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[y:{y:ℝ| y ∈ [-(π/2), π/2]} ]. ((rsin(y) = x) ⇒ (arcsin(x) = y))
Lemma: arcsin_functionality
∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[x':ℝ]. arcsin(x) = arcsin(x') supposing x = x'
Lemma: arcsin-rminus
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arcsin(-(a)) = -(arcsin(a)))
Lemma: arcsin0
arcsin(r0) = r0
Lemma: arcsin1
arcsin(r1) = π/2
Lemma: arcsin-minus1
arcsin(r(-1)) = -(π/2)
Lemma: arcsin-is-arcsine
∀[x:{x:ℝ| x ∈ (r(-1), r1)} ]. (arcsin(x) = arcsine(x))
Lemma: arcsin-shift
∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. arcsin(x) = (π/2 - arcsin(rsqrt(r1 - x * x))) supposing r0 ≤ x
Definition: arccos
arccos(x) == π/2 - arcsin(x)
Lemma: arccos_wf
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arccos(a) ∈ {x:ℝ| (x ∈ [r0, π]) ∧ (rcos(x) = a)} )
Lemma: rcos-arccos
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (rcos(arccos(a)) = a)
Lemma: arccos-bounds
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arccos(a) ∈ [r0, π])
Lemma: arccos-unique
∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[y:{y:ℝ| y ∈ [r0, π]} ]. ((rcos(y) = x) ⇒ (arccos(x) = y))
Lemma: arccos_functionality
∀[x:{x:ℝ| x ∈ [r(-1), r1]} ]. ∀[x':ℝ]. arccos(x) = arccos(x') supposing x = x'
Lemma: arccos-rminus
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (arccos(-(a)) = (π - arccos(a)))
Lemma: rsin-arccos
∀[a:{a:ℝ| a ∈ [r(-1), r1]} ]. (rsin(arccos(a)) = rsqrt(r1 - a * a))
Lemma: integration-by-parts
∀I:Interval. ∀u,v,h:I ⟶ℝ. ∀u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ ((h x) = (h y)))} .
(d(u[t])/dt = λt.u'[t] on I
⇒ d(v[t])/dt = λt.v'[t] on I
⇒ d(h[t])/dt = λt.u'[t] * v[t] on I
⇒ d((u[t] * v[t]) - h[t])/dt = λt.u[t] * v'[t] on I)
Lemma: integral-by-parts
∀I:Interval. ∀u,v,u',v':{h:I ⟶ℝ| ∀x,y:{t:ℝ| t ∈ I} . ((x = y) ⇒ ((h x) = (h y)))} .
(d(u[t])/dt = λt.u'[t] on I
⇒ d(v[t])/dt = λt.v'[t] on I
⇒ iproper(I)
⇒ (∀a,b:{a:ℝ| a ∈ I} . (a_∫-b u[t] * v'[t] dt = ((u[b] * v[b]) - u[a] * v[a] - a_∫-b u'[t] * v[t] dt))))
Lemma: ftc-example1
∀a,b:ℝ. (a_∫-b t^2 dt = ((b^3/r(3)) - (a^3/r(3))))
Lemma: ftc-example2
∀a,b:ℝ.
(a_∫-b t^3 * cosine(t) dt
= ((((b^3 - r(6) * b) * sine(b)) - (a^3 - r(6) * a) * sine(a))
+ ((((r(3) * b^2) - r(6)) * cosine(b)) - ((r(3) * a^2) - r(6)) * cosine(a))))
Lemma: Legendre-orthogonal
∀[n,k:ℕ].
r(-1)_∫-r1 x^k * Legendre(n;x) dx = if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) else r0 fi
supposing k ≤ n
Lemma: Legendre-orthogonal-rpolynomial
∀[n,k:ℕ]. ∀[a:ℕk + 1 ⟶ ℝ].
r(-1)_∫-r1 (Σi≤k. a_i * x^i) * Legendre(n;x) dx
= if (k =z n) then (r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n) else r0 fi
supposing k ≤ n
Lemma: Legendre-annihilates-rpolynomial
∀[n:ℕ]. ∀[f:[r(-1), r1] ⟶ℝ].
r(-1)_∫-r1 f[x] * Legendre(n;x) dx = r0
supposing ∃k:ℕn. ∃a:ℕk + 1 ⟶ ℝ. ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤k. a_i * x^i))
Lemma: Legendre-rpolynomial-same-degree
∀[n:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[f:[r(-1), r1] ⟶ℝ].
r(-1)_∫-r1 f[x] * Legendre(n;x) dx = ((r(2 * (n)!)/r(doublefact((2 * n) + 1))) * (a n))
supposing ∀x:{x:ℝ| x ∈ [r(-1), r1]} . ((f x) = (Σi≤n. a_i * x^i))
Lemma: Legendre-orthogonality
∀[n,m:ℕ]. (r(-1)_∫-r1 Legendre(n;x) * Legendre(m;x) dx = if (n =z m) then (r(2)/r((2 * n) + 1)) else r0 fi )
Lemma: Legendre-roots-lemma
∀n:{2...}. ∀z:ℕn - 1 ⟶ {x:ℝ| x ∈ (r(-1), r1)} .
((∀i:ℕn - 1. (Legendre(n - 1;z i) = r0))
⇒ (∀i:ℕn - 2. ((z i) < (z (i + 1))))
⇒ (∀i:ℕn. ∀v:{v:ℝ| (v ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))) ∧ (Legendre(n;v) = r0)} \000C.
(r0 < (r(-1)^n - i * Legendre(n + 1;v)))))
Lemma: Legendre-roots-lemma2
∀n:ℕ. ∀z:ℕn - 1 ⟶ {x:ℝ| x ∈ (r(-1), r1)} .
((∀i:ℕn - 1. (Legendre(n - 1;z i) = r0))
⇒ (∀i:ℕn - 2. ((z i) < (z (i + 1))))
⇒ (∀i:ℕn. ∀v:{v:ℝ| (v ∈ (if i=0 then r(-1) else (z (i - 1)), if i=n - 1 then r1 else (z i))) ∧ (Legendre(n;v) = r0)} \000C.
(r0 < (r(-1)^n - i * Legendre(n + 1;v)))))
Lemma: Legendre-roots-sq
∀n:ℕ
(∃z:i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
[(∀i:ℕn - 1. ((z i) < (z (i + 1))))])
Definition: Legendre-root
Legendre-root(n;i) ==
primrec(n;λi.r0;λi,x. if i + 1=1
then λi.r0
else (λi@0.rational_fun_zero(λx.ratLegendre(i + 1;x);if i@0=0
then r(-1)
else (x (i@0 - 1));if i@0=(i + 1) - 1
then r1
else (x i@0))))
i
Lemma: Legendre-roots-ext
∀n:ℕ
(∃z:i:ℕn ⟶ {x:ℝ| (x ∈ (r(-1), r1)) ∧ (Legendre(n;x) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;x)))}
[(∀i:ℕn - 1. ((z i) < (z (i + 1))))])
Lemma: Legendre-root_wf
∀[n:ℕ]. ∀[i:ℕn].
(Legendre-root(n;i) ∈ {z:ℝ| (z ∈ (r(-1), r1)) ∧ (Legendre(n;z) = r0) ∧ (r0 < (r((-1)^(n - i)) * Legendre(n + 1;z)))} )
Lemma: Legendre-roots-rless
∀n:ℕ. ∀i,j:ℕn. (i < j ⇒ (Legendre-root(n;i) < Legendre-root(n;j)))
Lemma: Legendre-roots-unique
∀[n:ℕ]. ∀[z:ℕn ⟶ ℝ].
(∀[i:ℕn]. ((z i) = Legendre-root(n;i))) supposing
((∀i:ℕn. (Legendre(n;z i) = r0)) and
(∀i:ℕn - 1. ((z i) < (z (i + 1)))))
Lemma: Legendre-roots-property
∀n:ℕ. ∀z:ℕn ⟶ ℝ.
(∀i:ℕn. (r0 < (r((-1)^(n - i)) * Legendre(n + 1;z i)))) supposing
((∀i:ℕn. (Legendre(n;z i) = r0)) and
(∀i:ℕn - 1. ((z i) < (z (i + 1)))))
Lemma: Legendre-sign-changes
∀n:ℕ. ∃L:(ℤ × ℕ+) List [((||L|| = (n - 1) ∈ ℤ) ∧ rat-sign-change-list(λx.ratLegendre(n;x);<-1, 1>;<1, 1>;L))] supposing \000C0 < n
Definition: Legendre_changes
Legendre_changes(n) ==
primrec(n;Ax;λn,x. if n + 1=1
then []
else eval L = x in
let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - i) then inl Ax else (inr (λx.Ax) ) in
eval-mklist(n + 0;λi.if i=0
then if i=n - 1
then find_rational(<-1, 1>;<1, 1>;d i)
else eval b = L[i] in
find_rational(<-1, 1>;b;d i)
else eval a = L[i - 1] in
if i=n - 1
then find_rational(a;<1, 1>;d i)
else eval b = L[i] in
find_rational(a;b;d i);0))
Lemma: Legendre-sign-changes-ext
∀n:ℕ. ∃L:(ℤ × ℕ+) List [((||L|| = (n - 1) ∈ ℤ) ∧ rat-sign-change-list(λx.ratLegendre(n;x);<-1, 1>;<1, 1>;L))] supposing \000C0 < n
Lemma: Legendre_changes_wf
∀[n:ℕ+]
(Legendre_changes(n) ∈ {L:(ℤ × ℕ+) List| (||L|| = (n - 1) ∈ ℤ) ∧ rat-sign-change-list(λx.ratLegendre(n;x);<-1, 1>;<1, \000C1>;L)} )
Definition: ratLegendreSign
ratLegendreSign(n;k;m) == ratsign(ratLegendre(n;<k, m>))
Lemma: ratLegendreSign_wf
∀[n:ℕ]. ∀[k:ℤ]. ∀[m:ℕ+]. (ratLegendreSign(n;k;m) ∈ {-1..2-})
Definition: LegendreSigns
LegendreSigns(n;L) ==
interpolate-list(a,b.let x,s = a
in let y,s' = b
in eval m = rat-midpoint(x;y) in
eval s'' = ratsign(ratLegendre(n;m)) in
<m, s''>;L)
Lemma: LegendreSigns_wf
∀[n:ℕ]. ∀[L:(x:ℤ × ℕ+ × {s:{-1..2-}| s = ratsign(ratLegendre(n;x)) ∈ ℤ} ) List].
(LegendreSigns(n;L) ∈ (x:ℤ × ℕ+ × {s:{-1..2-}| s = ratsign(ratLegendre(n;x)) ∈ ℤ} ) List)
Definition: NextNonZero
NextNonZero(L) == if L = Ax then L otherwise let h,t = L in if snd(h)=0 then NextNonZero(t) else L
Lemma: NextNonZero_wf
∀[T:Type]. ∀[L:(T × ℤ) List].
(NextNonZero(L) ∈ {L':(T × ℤ) List|
∃Z:(T × {z:ℤ| z = 0 ∈ ℤ} ) List
((L = (Z @ L') ∈ ((T × ℤ) List)) ∧ (0 < ||L'|| ⇒ (¬((snd(hd(L'))) = 0 ∈ ℤ))))} )
Definition: OnlyChanges
OnlyChanges(L) ==
if L = Ax then L otherwise let h,t = L
in let a,s = h
in if s=0
then OnlyChanges(t)
else eval nz = NextNonZero(t) in
if nz = Ax then [] otherwise eval ch = OnlyChanges(nz) in
let h',t' = nz
in let b,s' = h'
in if s'=-s then [<a, b> / ch] else ch
Definition: getLegendreChanges
getLegendreChanges(n;h;L) ==
eval ch = OnlyChanges(L) in
if ||ch||=h then ch else eval L' = LegendreSigns(n;L) in getLegendreChanges(n;h;L')
Definition: LegendreChangesAux
LegendreChangesAux(n; m; L; i; j; s) ==
if i=m
then L
else eval i' = i + 1 in
eval s' = ratLegendreSign(n;i';m) in
if s'=0
then LegendreChangesAux(n; m; L; i'; j; s)
else if s'=s
then LegendreChangesAux(n; m; L; i'; i'; s')
else LegendreChangesAux(n; m; [<j, i'> / L]; i'; i'; s')
Definition: findLegendreChanges
findLegendreChanges(n) ==
eval h = n ÷ 2 in
eval m = 2 * n in
eval L = eager-map(λk.eval s = ratLegendreSign(n;k;m) in
<<k, m>, s>;upto(m + 1)) in
getLegendreChanges(n;h;L)
Definition: pos-Legendre-changes
pos-Legendre-changes(n) ==
primrec(n;Ax;λn,x. if n + 1=1
then []
else eval L = x in
eval m = n ÷ 2 in
eval r = n rem 2 in
if r=1
then let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - i)
then inl Ax
else (inr (λx.Ax) ) in
eval-mklist(m;λi.eval a = L[i] in
if i=m - 1
then find_rational(a;<1, 1>;d i)
else eval b = L[i + 1] in
find_rational(a;b;d i);0)
else let d = λi,r. if ratsign(ratLegendre(n + 1;r))=(-1)^(n - 1 - i)
then inl Ax
else (inr (λx.Ax) ) in
eval-mklist(m;λi.if i=0
then if i=m - 1
then find_rational(<0, 1>;<1, 1>;d i)
else eval b = L[i] in
find_rational(<0, 1>;b;d i)
else eval a = L[i - 1] in
if i=m - 1
then find_rational(a;<1, 1>;d i)
else eval b = L[i] in
find_rational(a;b;d i);0))
Definition: Legendre_zero
Legendre_zero(n;i) ==
eval L = Legendre_changes(n) in
rational-fun-zero(λx.int-rat-mul(-1^n - i - 1;ratLegendre(n;x));if i=0 then <-1, 1> else L[i - 1];if i=n - 1
then <1, 1>
else L[i])
Definition: LegCh
LegCh(n) ==
primrec(n;Ax;λn,x. if n + 1=1
then []
else mklist(n
+ 0;λi.find_rational(if i=0 then <-1, 1> else x[i - 1];if i=n - 1
then <1, 1>
else x[i];λr.if ratsign(ratLegendre(n
+ 1;r))=(-1)^((n + 0) - i)
then inl Ax
else (inr (λx.Ax) ))))
Comment: summary of definitions
k-regular-seq(f) == ∀n,m:ℕ+. (|(m * (f n)) - n * (f m)| ≤ ((2 * k) * (n + m)))
bdd-diff(f;g) == ∃B:ℕ. ∀n:ℕ+. (|(f n) - g n| ≤ B)
ℝ == {f:ℕ+ ⟶ ℤ| regular-seq(f)}
x = y == ∀n:ℕ+. (|(x n) - y n| ≤ 4)
x < y == ∃n:ℕ+ [(x n) + 4 < y n]
accelerate(k;f) == eval k2 = 2 * k in λn.eval m = k2 * n in (f m) ÷ k2
a + b == accelerate(2;reg-seq-list-add([a; b]))
-(x) == λn.(-(x n))
rmax(x;y) == λn.imax(x n;y n)
|x| == rmax(x;-(x))
a * b ==
eval a1 = a in
eval b1 = b in
accelerate((2 * imax(canonical-bound(a1);canonical-bound(b1))) + 1;reg-seq-mul(a1;b1))⋅
Comment: sample reals lemmas
regular-int-seq;
bdd-diff;
real;
accelerate;
accelerate-bdd-diff;
radd;
rminus;
rmul;
req;
radd_functionality;
rmax;
rabs;
rless;
rlessw_wf;
rleq-iff4;
converges-iff-cauchy;
converges-iff-cauchy-ext;
rmul-limit;
reals-uncountable-simple;
cosine-exists-ext;
Taylor-series-converges⋅
Comment: What is uniformity conjecture?
It conjectures that an expression built from integers using exp, log, rroot,
and +, -, *, rdiv can not be too small, if the the expression is short.
The original version of the conjecture had some counter examples.
They were expressions F(x) that were 0 at 0 to "high order".
Then iterating F(F(x)) would not increase the length too much (if x occurs only
twice, say), and would have an even higher order zero at 0.
So then for x = 1/10^N F(F(x)) is very small.⋅
Definition: un-ctrex1
un-ctrex1(x) == (rroot(2;x + r1) - r(2) * rroot(3;r1 + ((r(3))/4 * x))) + r1
Lemma: un-ctrex1_wf
∀[x:{x:ℝ| r(-1) ≤ x} ]. (un-ctrex1(x) ∈ ℝ)
Definition: small-ctrex1
small-ctrex1() == un-ctrex1(un-ctrex1((r1)/10^126))
Lemma: small-ctrex1_wf
small-ctrex1() ∈ ℝ
Lemma: ctrex1-calculation
small-ctrex1() 10^1143 ~ 23
Lemma: small-ctrex1-bounds
(r1/r(10))≤r(10^1141) * small-ctrex1()≤(r1/r(4))
Lemma: basic-continuity
∀[F:(ℤ ⟶ ℤ) ⟶ ℤ]. ∀[f:ℤ ⟶ ℤ].
(↓∃n:ℕ. ∀[g:ℤ ⟶ ℤ]. (F f) = (F g) ∈ ℤ supposing ∀[i:ℤ]. (f i) = (g i) ∈ ℤ supposing |i| < n)
Lemma: BB-problem-21
∀a:ℝ. ∀b:{b:ℝ| a ≤ b} . ∀f,g:{f:[a, b] ⟶ℝ| ifun(f;[a, b])} .
((∀x:ℝ. ((x ∈ [a, b]) ⇒ (r0 ≤ g[x])))
⇒ (∀e:{e:ℝ| r0 < e} . ∃c:{x:ℝ| x ∈ [a, b]} . (|a_∫-b f[x] * g[x] dx - f[c] * a_∫-b g[x] dx| < e)))
Lemma: Taylor-remainder-as-integral
∀I:Interval
(iproper(I)
⇒ (∀a,b:{a:ℝ| a ∈ I} . ∀n:ℕ. ∀F:ℕn + 2 ⟶ I ⟶ℝ.
((∀k:ℕn + 2. ∀x,y:{a:ℝ| a ∈ I} . ((x = y) ⇒ (F[k;x] = F[k;y])))
⇒ finite-deriv-seq(I;n + 1;i,x.F[i;x])
⇒ (Taylor-remainder(I;n;b;a;k,x.F[k;x]) = a_∫-b (F[n + 1;t]/r((n)!)) * b - t^n dt))))
Definition: qreal
[ℝ] == x,y:ℝ//(x = y)
Lemma: qreal_wf
[ℝ] ∈ Type
Lemma: real-subtype-qreal
ℝ ⊆r [ℝ]
Lemma: qreal-function
∀[f:ℝ ⟶ ℝ ⟶ ℝ]. f ∈ [ℝ] ⟶ [ℝ] ⟶ [ℝ] supposing ∀a1,a2,b1,b2:ℝ. ((a1 = a2) ⇒ (b1 = b2) ⇒ (f[a1;b1] = f[a2;b2]))
Definition: qrle
qrle(x;y) == ↓∃a,b:ℝ. ((a = x ∈ [ℝ]) ∧ (b = y ∈ [ℝ]) ∧ (a ≤ b))
Lemma: qrle_wf
∀[x,y:[ℝ]]. (qrle(x;y) ∈ ℙ)
Definition: num-digits
num-digits(k)==r if (k) < (10) then 1 else eval k' = k ÷ 10 in 1 + num-digits(k')
Lemma: num-digits_wf
∀[k:ℕ]. (num-digits(k) ∈ {n:ℕ+| ((10^(n - 1) ≤ k) ∨ (k = 0 ∈ ℤ)) ∧ k < 10^n} )
Definition: rbinop
rbinop(op;p;q) ==
if op=4
then p - q
else if op=5
then p * q
else if op=6
then (p/q)
else if op=7
then rmax(p;q)
else if op=8 then rmin(p;q) else if op=9 then p + q else if op=10 then realexp(p;q) else (p + q)
Lemma: rbinop_wf
∀[op:ℤ]. ∀[p,q:ℝ]. rbinop(op;p;q) ∈ ℝ supposing ((op = 6 ∈ ℤ) ⇒ q ≠ r0) ∧ ((op = 10 ∈ ℤ) ⇒ (r0 < p))
Definition: runop
runop(op;p) ==
if op=0
then -(p)
else if op=1
then rsin(p)
else if op=2
then rcos(p)
else if op=3
then |p|
else if op=4
then expr(p)
else if op=5
then ln(p)
else if op=6
then arcsin(p)
else if op=7
then cosh(p)
else if op=8
then sinh(p)
else if op=9
then inv-cosh(p)
else if op=10
then inv-sinh(p)
else if op=11
then rinv(p)
else if op=12 then rtan(p) else if op=13 then arctan(p) else p
Lemma: runop_wf
∀[op:ℤ]. ∀[p:ℝ].
(runop(op;p) ∈ ℝ) supposing
(((op = 5 ∈ ℤ) ⇒ (r0 < p)) and
((op = 6 ∈ ℤ) ⇒ (p ∈ (r(-1), r1))) and
((op = 9 ∈ ℤ) ⇒ (r1 ≤ p)) and
((op = 11 ∈ ℤ) ⇒ p ≠ r0) and
((op = 12 ∈ ℤ) ⇒ ((-(π/2) < p) ∧ (p < π/2))))
Definition: rP_to_real
rP_to_real(stack;L)
==r if L = Ax then stack otherwise let op,more = L
in if op=1
then let c,evenmore = more
in rP_to_real([r(c) / stack];evenmore)
else if op=2
then let c,d,evenmore = more in
rP_to_real([r(c) + (r(d))/10^num-digits(d) / stack];evenmore)
else if op=3
then rP_to_real(<4 * MachinPi4(), stack>;more)
else if op <z 11
then let q,p,s = stack in
rP_to_real([rbinop(op;p;q) / s];more)
if op <z 25
then let p,s = stack
in rP_to_real([runop(op - 11;p) / s];more)
if op <z 29
then let c,evenmore = more
in let p,s = stack
in let q = if op=25
then rroot(c;p)
else if op=26
then c * p
else if op=27 then (p)/c else p^c in
rP_to_real([q / s];evenmore)
else stack
fi
Definition: rfun-ap
f(x) == f x
Lemma: rfun-ap_wf
∀[f:ℝ ⟶ ℝ]. ∀[x:ℝ]. (f(x) ∈ ℝ)
Lemma: rfun-ap_functionality
∀[f:ℝ ⟶ ℝ]. ∀x,y:ℝ. f(x) = f(y) supposing x = y supposing ∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y)))
Lemma: Cauchy-equation-1-iff
∀[f:ℝ ⟶ ℝ]
uiff(∀x,y:ℝ. (f(x + y) = (f(x) + f(y)));∀x:ℝ. (f(x) = (x * f(r1)))) supposing ∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y)))
Lemma: Cauchy-equation-iff
∀f:ℝ ⟶ ℝ
∀x,y:ℝ. (f(x + y) = (f(x) + f(y))) ⇐⇒ ∃c:ℝ. ∀x:ℝ. (f(x) = (c * x)) supposing ∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y)))
Lemma: rexp-functional-equation
∀f:ℝ ⟶ ℝ
∀x,y:ℝ. (f(x + y) = (f(x) * f(y))) ⇐⇒ (∃c:ℝ. ∀x:ℝ. (f(x) = e^c * x)) ∨ (∀x:ℝ. (f(x) = r0))
supposing ∀x,y:ℝ. ((x = y) ⇒ ((f x) = (f y)))
Lemma: DAlembert-equation-lemma
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y))))
⇒ ((∀x:ℝ. (f(-(x)) = f(x)))
∧ (∀n:ℤ. ∀y:ℝ. (f(r(n + 1) * y) = ((r(2) * f(y) * f(r(n) * y)) - f(r(n - 1) * y))))
∧ (∀t:ℝ. ((f((t/r(2))) * f((t/r(2)))) = (f(t) + r1/r(2)))))
⇒ ((∀x:ℝ. (g(-(x)) = g(x)))
∧ (∀n:ℤ. ∀y:ℝ. (g(r(n + 1) * y) = ((r(2) * g(y) * g(r(n) * y)) - g(r(n - 1) * y))))
∧ (∀t:ℝ. ((g((t/r(2))) * g((t/r(2)))) = (g(t) + r1/r(2)))))
⇒ (f(r0) = g(r0))
⇒ (∀a:ℝ
((r0 < a)
⇒ (f(a) = g(a))
⇒ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < f(x)))
⇒ (∀x:{x:ℝ| x ∈ [-(a), a]} . (r0 < g(x)))
⇒ (∀x:ℝ. (f(x) = g(x))))))
Lemma: DAlembert-equation-iff
∀f:ℝ ⟶ ℝ
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))
⇐⇒ (∀x:ℝ. (f(x) = r0)) ∨ (¬¬((∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))))
Lemma: DAlembert-equation-iff2
∀f:ℝ ⟶ ℝ
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
∧ (∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))
∧ (∃u:ℝ
((r0 < u)
∧ (∃g,h:(-(u), u) ⟶ℝ
(d(f(x))/dx = λx.g(x) on (-(u), u) ∧ d(g(x))/dx = λx.h(x) on (-(u), u) ∧ ((h(r0) ≤ r0) ∨ (r0 ≤ h(r0)))))))
⇐⇒ (∀x:ℝ. (f(x) = r0)) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = rcos(c * x))) ∨ (∃c:ℝ. ∀x:ℝ. (f(x) = cosh(c * x))))
Lemma: DAlembert-equation-iff3
∀f:ℝ ⟶ ℝ
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
∧ (∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))
∧ (∃u:ℝ
((r0 < u)
∧ (∃g,h:(-(u), u) ⟶ℝ
(d(f(x))/dx = λx.g(x) on (-(u), u)
∧ d(g(x))/dx = λx.h(x) on (-(u), u)
∧ ((h(r0) < r0) ∨ (h(r0) = r0) ∨ (r0 < h(r0)))))))
⇐⇒ (∀x:ℝ. (f(x) = r0))
∨ (∀x:ℝ. (f(x) = r1))
∨ (∃c:{c:ℝ| r0 < c} . ∀x:ℝ. (f(x) = rcos(c * x)))
∨ (∃c:{c:ℝ| r0 < c} . ∀x:ℝ. (f(x) = cosh(c * x))))
Lemma: cos-sin-equation-nc
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y))))
⇒ (∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⇒ (∃a:ℝ. f(a) ≠ f(r0))
⇒ (∃b:ℝ. g(-(b)) ≠ g(b))
⇒ ((∀x,y:ℝ. (f(x - y) = f(y - x)))
∧ (∀y:ℝ. (f(-(y)) = f(y)))
∧ (∀y:ℝ. (g(-(y)) = -(g(y))))
∧ (g(r0) = r0)
∧ (∃d:ℝ. f(d) ≠ r0)
∧ (f(r0) = r1)
∧ (∀x:ℝ. ((f(x)^2 + g(x)^2) = r1))
∧ (∀x:ℝ. (|f(x)| ≤ r1))
∧ (∀x,y:ℝ. ((f(x - -(y)) + f(x - y)) = (r(2) * f(x) * f(y))))
∧ (∀x,y:ℝ. ((f(x + y) + f(x - y)) = (r(2) * f(x) * f(y))))))
Lemma: cos-sin-equation
∀f,g:ℝ ⟶ ℝ.
(((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y)))) ∧ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y)))))
∧ (∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⇐⇒ ¬¬((∃c:ℝ
((r0 ≤ (c - c^2))
∧ (∀x:ℝ. (f(x) = c))
∧ ((∀x:ℝ. (g(x) = rsqrt(c - c^2))) ∨ (∀x:ℝ. (g(x) = -(rsqrt(c - c^2)))))))
∨ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))))
Lemma: cos-sin-equation-non-constant1
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y))))
⇒ (∃a,b:ℝ. f(a) ≠ f(b))
⇒ (∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⇒ (¬¬(∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x)))))))
Lemma: cos-sin-equation-non-constant2
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y))))
⇒ (∃u,v:ℝ. f(u) ≠ f(v))
⇒ (∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⇒ (∃I:Interval. (iproper(I) ∧ (r0 ∈ I) ∧ (∃g':I ⟶ℝ. d(g(x))/dx = λx.g' x on I)))
⇒ (∃a:ℝ. ((∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
Lemma: cos-sin-equation-non-constant3
∀f,g:ℝ ⟶ ℝ.
((∀x,y:ℝ. ((x = y) ⇒ (f(x) = f(y))))
⇒ (∀x,y:ℝ. ((x = y) ⇒ (g(x) = g(y))))
⇒ (∃a,b:ℝ. f(a) ≠ f(b))
⇒ (∀x,y:ℝ. (f(x - y) = ((f(x) * f(y)) + (g(x) * g(y)))))
⇒ (∃b:ℝ. (r0_∫-b -(g(x)) dx ≠ r0 ∧ f(b) ≠ r1))
⇒ (∃a:ℝ. (a ≠ r0 ∧ (∀x:ℝ. (f(x) = rcos(a * x))) ∧ (∀x:ℝ. (g(x) = rsin(a * x))))))
Lemma: ratio-functional-equation
∀[T:Type]
∀t:T. ∀F:T ⟶ T ⟶ ℝ.
(∀x,y,z:T. (((F x y) * (F y z)) = (F x z))
⇐⇒ (∀x,y:T. ((F x y) = r0)) ∨ (∃f:T ⟶ {x:ℝ| x ≠ r0} . ∀x,y:T. ((F x y) = (f x/f y))))
Definition: weighted-mean-properties
weighted-mean-properties(I;F) ==
(∀x:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ((F x x r s) = x))
∧ (∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r,s:{s:ℝ| r0 < s} .
((a = (F a b r1 r0)) ∧ ((F a b r1 r0) < (F a b r s)) ∧ ((F a b r s) < (F a b r0 r1)) ∧ ((F a b r0 r1) = b)))
∧ (∀a,b:{b:ℝ| b ∈ I} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀t:{t:ℝ| r0 < t} .
((F a b (r * t) (s * t)) = (F a b r s)))
∧ (∀x,y:{x:ℝ| x ∈ I} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} . ∀X,Y:{x:ℝ| x ∈ I} . ∀R:{R:ℝ|
(r0 ≤ R)
∧ (r0 < (r + R))} \000C.
∀S:{S:ℝ| ((r0 ≤ S) ∧ (r0 < (s + S))) ∧ (r0 < (R + S))} .
((F (F x y r s) (F X Y R S) (r + s) (R + S)) = (F (F x X r R) (F y Y s S) (r + R) (s + S))))
∧ (∀a:{a:ℝ| a ∈ I} . ∀b:{b:ℝ| (b ∈ I) ∧ (a < b)} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 ≤ s} . ∀t:{t:ℝ| s < t} .
((F a b r s) < (F a b r t)))
∧ (∀x,y:{x:ℝ| x ∈ I} . ∀z:{z:ℝ| (z ∈ I) ∧ (y < z)} . ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| r0 < s} . ((F x y r s) < (F x z r s)\000C))
Lemma: weighted-mean-properties_wf
∀[I:Interval]. ∀[F:{x:ℝ| x ∈ I} ⟶ {x:ℝ| x ∈ I} ⟶ r:{r:ℝ| r0 ≤ r} ⟶ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} ⟶ {x:ℝ| x ∈ \000CI} ].
(weighted-mean-properties(I;F) ∈ ℙ)
Definition: convex-comb
convex-comb(x;y;r;s) == ((r * x) + (s * y)/r + s)
Lemma: convex-comb_wf1
∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. (convex-comb(x;y;r;s) ∈ ℝ)
Lemma: convex-comb_wf
∀[I:Interval]. ∀[x,y:{x:ℝ| x ∈ I} ]. ∀[r:{r:ℝ| r0 ≤ r} ]. ∀[s:{s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))} ].
(convex-comb(x;y;r;s) ∈ {x:ℝ| x ∈ I} )
Lemma: convex-comb_functionality
∀[x1,y1,r1,x2,y2,r2:ℝ]. ∀[s1:{s:ℝ| r1 + s ≠ r0} ]. ∀[s2:{s:ℝ| r2 + s ≠ r0} ].
(convex-comb(x1;y1;r1;s1) = convex-comb(x2;y2;r2;s2)) supposing ((s1 = s2) and (r1 = r2) and (y1 = y2) and (x1 = x2))
Lemma: convex-comb-req
∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. (convex-comb(x;y;r;s) = (((r1 - (s/r + s)) * x) + ((s/r + s) * y)))
Lemma: convex-comb-same
∀[x,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. (convex-comb(x;x;r;s) = x)
Lemma: convex-comb-homog
∀[x,y,r:ℝ]. ∀[s:{s:ℝ| r + s ≠ r0} ]. ∀[t:{t:ℝ| t ≠ r0} ]. (convex-comb(x;y;r * t;s * t) = convex-comb(x;y;r;s))
Lemma: convex-comb-rless1
∀x,y:ℝ. ∀r:{r:ℝ| r0 ≤ r} . ∀s:{s:ℝ| (r0 < s) ∧ (r0 < (r + s))} . ∀z:{z:ℝ| y < z} .
(convex-comb(x;y;r;s) < convex-comb(x;z;r;s))
Lemma: convex-comb-rless2
∀x:ℝ. ∀y:{y:ℝ| x < y} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 < (r + s)} . ∀t:{t:ℝ| s < t} .
(convex-comb(x;y;r;s) < convex-comb(x;y;r;t))
Lemma: convex-comb-rless3
∀x:ℝ. ∀y:{y:ℝ| y < x} . ∀r:{r:ℝ| r0 < r} . ∀s:{s:ℝ| r0 < (r + s)} . ∀t:{t:ℝ| s < t} .
(convex-comb(x;y;r;t) < convex-comb(x;y;r;s))
Lemma: convex-comb-1-0
∀[x,y:ℝ]. ∀[t:{t:ℝ| t ≠ r0} ]. (convex-comb(x;y;t;r0) = x)
Lemma: convex-comb-0-1
∀[x,y:ℝ]. ∀[t:{t:ℝ| t ≠ r0} ]. (convex-comb(x;y;r0;t) = y)
Lemma: convex-comb-strict-lower-bound
∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ. ((y < x) ⇒ (y < convex-comb(x;y;r;s)))
Lemma: convex-comb-strict-lower-bound2
∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ. ((x < y) ⇒ (x < convex-comb(x;y;r;s)))
Lemma: convex-comb-strict-upper-bound
∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ. ((x < y) ⇒ (convex-comb(x;y;r;s) < y))
Lemma: convex-comb-strict-upper-bound2
∀r,s:{s:ℝ| r0 < s} . ∀x,y:ℝ. ((y < x) ⇒ (convex-comb(x;y;r;s) < x))
Definition: quasilinear-weighted-mean
quasilinear-weighted-mean(f;g) == λx,y,r,s. (f convex-comb(g x;g y;r;s))
Lemma: quasilinear-weighted-mean_wf
∀[I,J:Interval]. ∀[f:{x:ℝ| x ∈ J} ⟶ {x:ℝ| x ∈ I} ]. ∀[g:{x:ℝ| x ∈ I} ⟶ {x:ℝ| x ∈ J} ].
(quasilinear-weighted-mean(f;g) ∈ {x:ℝ| x ∈ I}
⟶ {x:ℝ| x ∈ I}
⟶ r:{r:ℝ| r0 ≤ r}
⟶ {s:ℝ| (r0 ≤ s) ∧ (r0 < (r + s))}
⟶ {x:ℝ| x ∈ I} )
Lemma: quasilinear-weighted-mean-properties
∀I,J:Interval. ∀f:{x:ℝ| x ∈ J} ⟶ {x:ℝ| x ∈ I} . ∀g:{x:ℝ| x ∈ I} ⟶ {x:ℝ| x ∈ J} .
(((∀x1,x2:{x:ℝ| x ∈ J} . ((x1 < x2) ⇒ ((f x1) < (f x2)))) ∨ (∀x1,x2:{x:ℝ| x ∈ J} . ((x1 < x2) ⇒ ((f x2) < (f x1)))\000C))
⇒ (∀x1,x2:{x:ℝ| x ∈ J} . ((x1 = x2) ⇒ ((f x1) = (f x2))))
⇒ (∀x1,x2:{x:ℝ| x ∈ I} . ((x1 = x2) ⇒ ((g x1) = (g x2))))
⇒ (∀x:{x:ℝ| x ∈ I} . ((f (g x)) = x))
⇒ weighted-mean-properties(I;quasilinear-weighted-mean(f;g)))
Definition: real*
ℝ* == ℕ ⟶ ℝ
Lemma: real*_wf
ℝ* ∈ Type
Definition: real*-ap
x(n) == x n
Lemma: real*-ap_wf
∀[x:ℝ*]. ∀[n:ℕ]. (x(n) ∈ ℝ)
Definition: rrel*
R*(x,y) == ∃n:ℕ. ∀m:{n...}. (R (x m) (y m))
Lemma: rrel*_wf
∀[R:ℝ ⟶ ℝ ⟶ ℙ]. ∀[x,y:ℝ*]. (R*(x,y) ∈ ℙ)
Definition: req*
x = y == ∃n:ℕ. ∀m:{n...}. ((x m) = (y m))
Lemma: req*_wf
∀[x,y:ℝ*]. (x = y ∈ ℙ)
Lemma: req*_weakening
∀[x,y:ℝ*]. x = y supposing x = y ∈ ℝ*
Lemma: req*_inversion
∀[x,y:ℝ*]. (x = y ⇒ y = x)
Lemma: req*_transitivity
∀[x,y,z:ℝ*]. (x = y ⇒ y = z ⇒ x = z)
Lemma: req*_functionality
∀[x1,x2,y1,y2:ℝ*]. (x1 = x2 ⇒ y1 = y2 ⇒ (x1 = y1 ⇐⇒ x2 = y2))
Lemma: req*-equiv
EquivRel(ℝ*;x,y.x = y)
Lemma: rrel*_functionality
∀[R:ℝ ⟶ ℝ ⟶ ℙ]
((∀x1,x2,y1,y2:ℝ. ((x1 = x2) ⇒ (y1 = y2) ⇒ (R x1 y1 ⇐⇒ R x2 y2)))
⇒ (∀x1,x2,y1,y2:ℝ*. (x1 = x2 ⇒ y1 = y2 ⇒ (R*(x1,y1) ⇐⇒ R*(x2,y2)))))
Definition: rfun*
f*(x) == λn.(f (x n))
Lemma: rfun*_wf
∀[f:ℝ ⟶ ℝ]. ∀[x:ℝ*]. (f*(x) ∈ ℝ*)
Lemma: rfun*_functionality
∀[f:ℝ ⟶ ℝ]. ∀[x,y:ℝ*]. ((∀[a,b:ℝ]. (f a) = (f b) supposing a = b) ⇒ x = y ⇒ f*(x) = f*(y))
Definition: rabs*
|x| == λa.|a|*(x)
Lemma: rabs*_wf
∀[x:ℝ*]. (|x| ∈ ℝ*)
Lemma: rabs*_functionality
∀[x,y:ℝ*]. (x = y ⇒ |x| = |y|)
Definition: rfun*2
f*(x;y) == λn.(f (x n) (y n))
Lemma: rfun*2_wf
∀[f:ℝ ⟶ ℝ ⟶ ℝ]. ∀[x,y:ℝ*]. (f*(x;y) ∈ ℝ*)
Lemma: rfun*2_functionality
∀[f:ℝ ⟶ ℝ ⟶ ℝ]. ∀[x,y,u,v:ℝ*].
((∀[a,b,c,d:ℝ]. (f a c) = (f b d) supposing (a = b) ∧ (c = d)) ⇒ x = y ⇒ u = v ⇒ f*(x;u) = f*(y;v))
Definition: radd*
x + y == λa,b. (a + b)*(x;y)
Lemma: radd*_wf
∀[x,y:ℝ*]. (x + y ∈ ℝ*)
Lemma: radd*_functionality
∀[x,y,u,v:ℝ*]. (x = y ⇒ u = v ⇒ x + u = y + v)
Definition: rmul*
x * y == λa,b. (a * b)*(x;y)
Lemma: rmul*_wf
∀[x,y:ℝ*]. (x * y ∈ ℝ*)
Lemma: rmul*_functionality
∀[x,y,u,v:ℝ*]. (x = y ⇒ u = v ⇒ x * u = y * v)
Definition: rless*
x < y == λa,b. (a < b)*(x,y)
Lemma: rless*_wf
∀[x,y:ℝ*]. (x < y ∈ ℙ)
Definition: rleq*
x ≤ y == λa,b. (a ≤ b)*(x,y)
Lemma: rleq*_wf
∀[x,y:ℝ*]. (x ≤ y ∈ ℙ)
Lemma: standard-fact-example1
∀[x,y,z:ℝ*]. x * y * z = z * y * x
Lemma: radd*_functionality_wrt_rleq*
∀[x,y,u,v:ℝ*]. (x ≤ y ⇒ u ≤ v ⇒ x + u ≤ y + v)
Lemma: radd*_functionality_wrt_rless*_1
∀x,y,u,v:ℝ*. (x < y ⇒ u ≤ v ⇒ x + u < y + v)
Lemma: radd*_functionality_wrt_rless*_2
∀x,y,u,v:ℝ*. (x ≤ y ⇒ u < v ⇒ x + u < y + v)
Definition: rstar
(x)* == λn.x
Lemma: rstar_wf
∀[x:ℝ]. ((x)* ∈ ℝ*)
Lemma: rstar_functionality
∀[x,y:ℝ]. (x)* = (y)* supposing x = y
Lemma: rstar-rless
∀[x,y:ℝ]. ((x)* < (y)* ⇐⇒ x < y)
Lemma: rstar-rleq
∀[x,y:ℝ]. ((x)* ≤ (y)* ⇐⇒ x ≤ y)
Lemma: rstar-radd
∀[x,y:ℝ]. (x)* + (y)* = (x + y)*
Lemma: rstar-rmul
∀[x,y:ℝ]. (x)* * (y)* = (x * y)*
Definition: rgt*
x > y == y < x
Lemma: rgt*_wf
∀[x,y:ℝ*]. (x > y ∈ ℙ)
Definition: rge*
x ≥ y == y ≤ x
Lemma: rge*_wf
∀[x,y:ℝ*]. (x ≥ y ∈ ℙ)
Lemma: rless*_transitivity
∀x,y,z:ℝ*. (x < y ⇒ y < z ⇒ x < z)
Lemma: rleq*_transitivity
∀x,y,z:ℝ*. (x ≤ y ⇒ y ≤ z ⇒ x ≤ z)
Lemma: rleq*_antisymmetry
∀x,y:ℝ*. (x ≤ y ⇒ y ≤ x ⇒ x = y)
Lemma: rleq*_weakening
∀[x,y:ℝ*]. (x = y ⇒ x ≤ y)
Lemma: rleq*_weakening_rless
∀[x,y:ℝ*]. (x < y ⇒ x ≤ y)
Lemma: rleq*_weakening_equal
∀[x,y:ℝ*]. ((x = y ∈ ℝ*) ⇒ x ≤ y)
Lemma: rless*_transitivity1
∀x,y,z:ℝ*. (x < y ⇒ y ≤ z ⇒ x < z)
Lemma: rless*_transitivity2
∀x,y,z:ℝ*. (x ≤ y ⇒ y < z ⇒ x < z)
Lemma: rless*_functionality
∀a,b,c,d:ℝ*. (a = b ⇒ c = d ⇒ (a < c ⇐⇒ b < d))
Lemma: rleq*_functionality
∀a,b,c,d:ℝ*. (a = b ⇒ c = d ⇒ (a ≤ c ⇐⇒ b ≤ d))
Lemma: rless*_functionality_wrt_implies
∀a,b,c,d:ℝ*. (b ≥ a ⇒ c ≤ d ⇒ {b < c ⇒ a < d})
Lemma: rleq*_functionality_wrt_implies
∀a,b,c,d:ℝ*. (b ≥ a ⇒ c ≤ d ⇒ {b ≤ c ⇒ a ≤ d})
Definition: is-standard
is-standard(x) == ∃r:ℝ. x = (r)*
Lemma: is-standard_wf
∀[x:ℝ*]. (is-standard(x) ∈ ℙ)
Definition: is-infinitesmal
is-infinitesmal(x) == ∀n:ℕ+. |x| < ((r1/r(n)))*
Lemma: is-infinitesmal_wf
∀[x:ℝ*]. (is-infinitesmal(x) ∈ ℙ)
Definition: std-infinitesmal
∈ == λn.(r1/r(n + 1))
Lemma: std-infinitesmal_wf
∈ ∈ ℝ*
Lemma: std-is-infinitesmal
is-infinitesmal(∈)
Lemma: infinitesmal-iff
∀x:ℝ*. (is-infinitesmal(x) ⇐⇒ ∀r:{r:ℝ| r0 < r} . |x| < (r)*)
Lemma: radd*_functionality_wrt_infinitesmal
∀x,y:ℝ*. (is-infinitesmal(x) ⇒ is-infinitesmal(y) ⇒ is-infinitesmal(x + y))
Home
Index