@article{Affeldt_Cohen_Rouhling_2018, title={Formalization Techniques for Asymptotic Reasoning in Classical Analysis}, volume={11}, url={https://jfr.unibo.it/article/view/8124}, DOI={10.6092/issn.1972-5787/8124}, abstractNote={Formalizing analysis on a computer involves a lot of “epsilon-delta” reasoning, while informal reasoning may use some asymptotical hand-waving. Whether or not the arithmetic details are hidden using some abstraction like filters, a human user eventually has to break it down for the proof assistant anyway, and provide a witness for the existential variable “delta”. We describe formalization techniques that take advantage of existential variables to delay the input of witnesses until a stage where the proof assistant can actually infer them. We use these techniques to prove theorems about classical analysis and to provide equational Bachmann-Landau notations. This partially restores the simplicity of informal hand-waving without compromising the proof. As expected this also reduces the size of proof scripts and the time to write them, and it also makes proofs more stable.}, number={1}, journal={Journal of Formalized Reasoning}, author={Affeldt, Reynald and Cohen, Cyril and Rouhling, Damien}, year={2018}, month={Jan.}, pages={43–76} }