F Background and references
On this page · Permalink · Source line 2
The references identify standard sources for limits, descent, Hilbert projection, bounded inverse theorems, and regularization. Appendix E gives the analytic arguments used repeatedly in the text. The accompanying Lean source and its pinned mathematical-library revision determine the formal interfaces used in this edition. Online library documentation is a navigation aid and may describe a different revision. The consultation dates below are retained from the recorded source checks.
References
[1] stacks-limits
The Stacks Project Authors. Limits and colimits over preordered sets. Section 4.21, Tag 002Z, including the finite-set inverse-limit theorem in Lemma 4.21.7. https://stacks.math.columbia.edu/tag/002Z. Accessed 10 October 2026.
[2] stacks-stack
The Stacks Project Authors. Stacks. Section 8.4, Tag 0268. In particular the effective descent and equivalence-of-descent-categories formulations. https://stacks.math.columbia.edu/tag/0268. Accessed 10 October 2026.
[3] mathlib-stack
The mathlib Community. CategoryTheory.Sites.Descent.IsStack. Standard pseudofunctor stack interface. https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Sites/Descent/IsStack.html.
[4] mathlib-projection
The mathlib Community. Analysis.InnerProductSpace.Projection.Basic. Orthogonal projection onto complete subspaces. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/InnerProductSpace/Projection/Basic.html.
[5] mathlib-banach
The mathlib Community. Analysis.Normed.Operator.Banach. Banach open mapping and continuous inverse constructions. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Operator/Banach.html.
[6] clason-inverse
Christian Clason. Regularization of Inverse Problems. Graduate lecture notes, arXiv:2001.00617v2, 2021. Sections 2, 4, and 6 provide standard background on weak convergence, parameter choice, and Tikhonov regularization. https://arxiv.org/abs/2001.00617v2. Consulted 12 October 2026.