Theorem knoppcn

Description: The continuous nowhere differentiable function W ( Knopp, K. (1918). Math. Z. 2, 1-26 ) is, in fact, continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021) (Revised by Asger C. Ipsen, 5-Jul-2021)

	Ref	Expression
Hypotheses	knoppcn.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	knoppcn.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
	knoppcn.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
	knoppcn.n	$$⊢\phi \to N\in \mathbb{N}$$
	knoppcn.1	$$⊢\phi \to C\in ℝ$$
	knoppcn.2	$$⊢\phi \to \left|C\right|<1$$
Assertion	knoppcn	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		knoppcn.t	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		knoppcn.f	$$⊢F=\left(y\in ℝ⟼\left(n\in {\mathbb{N}}_0⟼C^{n}T\left({2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}}^{n}y\right)\right)\right)$$
3		knoppcn.w	$$⊢W=\left(w\in ℝ⟼\sum _{i\in {\mathbb{N}}_0}F\left(w\right)\left(i\right)\right)$$
4		knoppcn.n	$$⊢\phi \to N\in \mathbb{N}$$
5		knoppcn.1	$$⊢\phi \to C\in ℝ$$
6		knoppcn.2	$$⊢\phi \to \left|C\right|<1$$
7		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
8		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
9	1 2 4 5	knoppcnlem11	$$⊢\phi \to seq0\left({\circ }_f+,\left(m\in {\mathbb{N}}_0⟼\left(z\in ℝ⟼F\left(z\right)\left(m\right)\right)\right)\right):{\mathbb{N}}_0⟶ℝ\underset{cn}{⟶}ℂ$$
10	1 2 3 4 5 6	knoppcnlem9	$$⊢\phi \to seq0\left({\circ }_f+,\left(m\in {\mathbb{N}}_0⟼\left(z\in ℝ⟼F\left(z\right)\left(m\right)\right)\right)\right)\underset{u}{⇝}\left(ℝ\right)W$$
11	7 8 9 10	ulmcn	$$⊢\phi \to W:ℝ\underset{cn}{⟶}ℂ$$