rescaling norms and weak exactness

Stream: condensed mathematics

[Johan Commelin]

Here's a sorry that should be very doable without context: https://github.com/leanprover-community/lean-liquid/blob/master/src/thm95/col_exact.lean#L77
It's about how weak exactness behaves when we rescale the norms of the objects in degree $i$ by $i!$.

[Johan Commelin]

I have done a start of the proof, so there is some inequality of real numbers left.

[Johan Commelin]

But I didn't pay attention to the $\varepsilon$, so it might need to be tweaked when used in the proof a couple lines up.

[Johan Commelin]

I'm done for the weekend. See you all next week.

[Riccardo Brasca]

I am having a look at it

[Riccardo Brasca]

It's not the best proof I've ever written, but scale_factorial.is_weak_bounded_exact is sorry free.