Coinduction in mathematical analysis?

Question

Coinduction is a logical principle that is somehow dual to induction. I'm struggling to understand it.

Are there any interesting examples of coinduction in analysis?

A few examples seem like they could be promising:

• the $p$-adic numbers can be represented as infinite streams in such a way that the arithmetic operations are well-behaved. Therefore coinduction seems quite promising here.
• continued fractions for real numbers. Unfortunately, the arithmetic operations are not well behaved in this representation; so it's unclear if it's of any use.
• Real numbers with signed digits. Coinduction here is complicated by the fact that representations of real numbers become non-unique. But the arithmetic operations are well-behaved. Seems promising.
• Power series.
• Continued powers or "infinite radicals".

Answer 1

The signed digit representation of Real Numbers seems like an efficient approach for:

• Defining the arithmetic operations and proving their algebraic properties. This was done already in a Master's thesis by Michael Herrmann.
• Proving Cantor's theorem on the uncountability of the real numbers.
• Developing the notions of continuous and uniformly continuous functions.
• Proving the Extreme Value Theorem in the form that every function on $[0,1]$ has a finite supremum.
• Developing the Riemann integral.

This has the nice property of being constructive.

As demonstrated by Michael Hermann, the operations listed above can be defined using colagebraic coinduction and then reasoned about using set-theoretic coinduction.

This also suggests the possibility of proving analogues of the above in $p$-adic analysis. Here, a purely coalgebraic approach might actually work.

It's possible that vast swathes of General Topology (over separable spaces) can be developed using coinduction over $\mathbb N^\mathbb N$. Here, continuous functions would be defined by corecursion over $\mathbb N ^ \mathbb N$ and then reasoned about using set-theoretic coinduction. This appears to be the approach taken in Frank'a Waaldijk's Natural Topology (I'm not sure if it uses coinduction though).

The caveat of all the above is that I've never seen a full development of the above. But the possibility certainly exists if anyone has the time or motivation.