zstone1

On further reflection, something is wrong with the ~~current~~ previous formulation. Most applications of this theorem carve out a subset `U` of `X`, which is invariant under `f`, and where...

Yes, support for a "between 0 and 1" real would definitely simplify things for this proof. There are some details regarding strictness of the inequalities. I defined contractions here as...

It's definitely an improvement. Factoring out the reusable bits from that giant algebra rewrite block is great. This look like a good halfway to building some canonical automation. I have...

Yeah, this looks good. That theory should probably move elsewhere, but otherwise I'm quite happy to see this improvement.

Bigger and better cantor stuff coming. With #763, the bulk of this work becomes redundant anyway.

I've just checked out the lemma statements (not the proofs), and it looks pretty neat. The existing `hlength_measure` canonical instance provides a reasonably nice interface for it. And `Hahn_ext_measure`. One...

With a long-term goal of doing spectral theory, I'm looking at defining integrals for a TVS. The most straightforward choice seems to be "weak integrals". I can work in a...

Interesting. I have not seen this trick before. Although, I can't find an example of it elsewhere in mathcomp analysis. For what it's worth, in the proof I have I...

Defining complex holomorphic in terms of the cauchy Riemann equations is quite nice. This works well when working only in `C` because multiplication is the same as scaling. But if...

Turns out the approach above is doomed. Coercions don't behave like I want. In particular, I want a coercion from `CNormedModule.class_of >-> NormedModule.class_of R` and `CNormedModule.class_of >-> NormedModule.class_of C`. Turns...