### Fractal Art 2

As discussed before (see here), Iterated Function System (IFS) can generate Fractals. This method is introduced by Michael Barnsley in 1986. Indeed, he showed the Collage Theorem: if a collection (or collage) of mappings in the IFS satisfy a contracting criterion, any initial image for the iteration will converge eventually to the same fractal image. This means a fractal image can be encoded by some suitable IFS, which can be decoded simply upon iteration of IFS. This is the basis of fractal compression algorithms.

The Collage Theorem belongs to a class of fixed-point theorems in metric space: a system in which a distance is suitably defined. A mapping in metric space maps each point an image point in the same space. The mapping is a contraction if the distance between image points is less than their original distance. That contraction mappings in metric space has a fixed point is a result called the Banach Fix-Point Theorem.

For my project on this topic, I plan to do the following:

- Formalize metric space up to contraction maps, hence proving Banach Fix-Point Theorem
- Extend metric space formalization to include IFS, hence proving Collage Theorem

With such formalization I should be able to verify fractal generating algorithms based on IFS. I still have to look up a bit more about fractal compression algorithms to find out if these tools are sufficient to verify such algorithms.