Functional analysis

The Lean Pool projects whose card's first MSC2020 code is in class 46, Functional analysis: 11 articles, one per card.

TheoremA counterexample to Scottish Book Problem 155#

A Lean proof that there are real Banach spaces X and Y and a bijection U from X to Y which preserves every pairwise distance on every closed ball of radius one quarter while failing to be a global isometry. This gives a counterexample to Scottish Book Problem 155.

Quoted from the card LeanPool/projects/lean-scottish-book-155.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanScottishBook155.claim14

TheoremConditional formalization of Zhou's Connes-rigidity counterexample#

Constructs Zhou's two countable discrete groups and, assuming the project's universe-polymorphic property-(T) predicate for EL₃(𝔽₂[t]), proves that both satisfy the same predicate, are ICC and nonisomorphic, while their group von Neumann algebras are trace-preservingly normally star-isomorphic.

Quoted from the card LeanPool/projects/connes-rigidity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists one main result, with its informal statement quoted from the card. The scan finds its declaration in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • Connes.theoremA (theorem; a main declaration), declared in LeanPool/ConnesRigidity/Main.lean, line 29: “At any Hilbert-space universe, assuming property-(T) for EL₃(𝔽₂[t]), constructs two countable discrete ICC groups satisfying property-(T) at that universe which are nonisomorphic although their group von Neumann algebras are trace-preservingly normally star-isomorphic.”
Project
Sources
LeanConnes.theoremA

TheoremGrothendieck's theorem for Bessel sequences#

Every Bessel sequence with bound one in a complex Hilbert space has its Gram kernel represented by correlations of measurable functions bounded by one on the unit interval. The proof includes real and complex finite matrix decompositions, a Ball--Prodromou argument, and a countable moment-measure construction followed by standard Borel realization.

Quoted from the card LeanPool/projects/grothendieck-bessel.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanGrothendieckBessel.main

TheoremHalving the Kalton-Roberts upper bound#

Formalizes the paper-style Boolean-algebra theorem that every approximately additive real-valued set function is uniformly close to a finitely additive signed measure, proving the certified Kalton-Roberts constant bound below 19.838.

Quoted from the card LeanPool/projects/kalton-roberts.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
  • Authors: Ho Boon Suan.
  • Source: Halving the original Kalton-Roberts upper bound for nearly additive set functions by Ho Boon Suan, Tomasz Kania, arXiv:2606.06807.
  • Project repository: boonsuan/KaltonRoberts.
  • Provenance: AI, which in Lean Pool's terms means its Lean proofs were “mostly produced by an AI system”.
  • License: MIT, under which the project was published; Lean Pool redistributes it under Apache-2.0.
  • MSC2020: 46B20, 28A12, 05C35.
  • In Lean Pool: LeanPool/KaltonRoberts, from the card LeanPool/projects/kalton-roberts.yaml.
Sources
LeanKaltonRoberts.KR_constant_lt

AbbreviationInfinite counterexamples to Connes's rigidity conjecture#

Constructs one finitely generated property-(T) ICC group and an infinite family of finitely generated property-(T) ICC groups that are pairwise nonisomorphic and are each nonisomorphic to the first group, while all of their tracial group von Neumann algebras are normally star-isomorphic. This unconditional infinite-family result is independent of the pooled conditional two-group Connes-rigidity formalization.

Quoted from the card LeanPool/projects/infinite-connes-rigidity.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanConnesRigidity.infiniteConnesRigidity

TheoremLie–Trotter product formula with commutator scaling#

Proves the Lie–Trotter product formula in a complete normed real algebra with norm-one unit, with an explicit error bound proportional to the commutator.

Quoted from the card LeanPool/projects/lie-trotter-commutator.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLieTrotter.norm_trotter_sub_le_commutator · LieTrotter.trotter_product

TheoremMichal–Bastiani Calculus on Locally Convex Spaces#

Develops real Michal–Bastiani calculus on Hausdorff locally convex spaces, with the chain rule, continuous symmetric higher differentials, and Taylor's formula in weak form. It proves equivalence with smooth Fréchet calculus on open subsets of normed spaces. Weak integrals exist for continuous curves in sequentially complete spaces and for continuously differentiable curves in Mackey complete spaces; Mackey completeness is characterized by weak integrability of Lipschitz curves. A smooth map from a Banach space to a normed space with derivative uniformly bounded below reflects finite differentiability of continuous maps from open locally convex domains.

Quoted from the card LeanPool/projects/lc-analysis.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 6 main results, each with its informal statement quoted from the card. The scan finds 6 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanLCAnalysis.ContDiffMBOn.comp · LCAnalysis.ContDiffMBOn.exists_iteratedDMB_multilinear · LCAnalysis.smoothMBOn_iff_contDiffOn · LCAnalysis.exists_hasWeakIntegral · LCAnalysis.mackeyComplete_iff_integratesLipschitzCurves · LCAnalysis.ContDiffMBOn.of_comp_of_boundedBelow

TheoremOrder closure, order adherence and Fatou norms#

Formalizes order and unbounded-order adherence in vector lattices, the Gao-Leung characterization of order-continuous norms on sigma-order-complete Banach lattices, and the Solovay/Stone-space construction of order-complete C(K) spaces with arbitrarily large density and norm-closed separable sublattices whose only order-closed vector-sublattice extension is the whole C(K) space. Constructs solid sets with a prescribed infinite number kappa of solid generators whose adherence towers are strict below any ordinal at most kappa's successor cardinal. Constructs a complete weakly Fatou lattice norm with constant 2 that is not equivalent to any Fatou lattice norm. Includes reusable vector-lattice, net-convergence, sublattice, seminorm, Boolean-algebra and transfinite-iteration infrastructure.

Quoted from the card LeanPool/projects/order-closures.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 4 main results, each with its informal statement quoted from the card. The scan finds 4 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

  • OrderClosures.gaoLeung_orderContinuous_characterization (theorem), declared in LeanPool/OrderClosures/GaoLeungCharacterization.lean, line 1012: “For a sigma-order-complete Banach lattice X, the following are equivalent: every vector sublattice has order-closed order adherence; every vector sublattice has equal order and unbounded-order adherence; and the norm of X is order continuous.” Its source, as the card gives it: “Paper Theorem 1.1, recalling Gao-Leung Theorem 2.7.”
  • OrderClosures.gao_counterexample (theorem), declared in LeanPool/OrderClosures/GaoLeungProblem/Counterexample.lean, line 45: “For every cardinal kappa there is a compact Hausdorff space K such that C(K, R) is order complete and has density at least kappa, with a norm-closed separable vector sublattice Y whose only order-closed vector-sublattice extension is all of C(K, R).” Its source, as the card gives it: “Paper Proposition 2.1, via the Solovay Boolean algebra.”
  • OrderClosures.solid_sets_require_arbitrarily_many_iterations (theorem), declared in LeanPool/OrderClosures/GaoLeungProblem/Iterations.lean, line 625: “For every infinite cardinal kappa and ordinal xi at most the initial ordinal of kappa's successor cardinal, there is a vector lattice and a solid set with solid generator number kappa whose order-adherence tower has a proper step at every stage below xi. The witness and cardinal/ordinal parameters are lifted one universe in Lean.” Its source, as the card gives it: “Paper Theorem 2.6, with its explicit infinite-cardinal hypothesis. Lean strengthens the stated size-kappa generating-set conclusion to minimum solid generator number exactly kappa; this exact-minimum conclusion is proved in the formalization, not stated in the paper.”
  • OrderClosures.exists_weaklyFatou_not_equivalent_fatou (theorem; a main declaration), declared in LeanPool/OrderClosures/WeaklyFatou/FinalSpace.lean, line 588: “There is a real vector lattice with a complete lattice norm p satisfying the weak Fatou property with constant 2, such that no lattice norm q with the Fatou property is equivalent to p. Norms, completeness and equivalence are represented explicitly by PaperLatticeNorm, IsCompleteFor and EquivalentNorms.” Its source, as the card gives it: “Paper Theorem 3.1; self-contained construction of the result previously announced by Anthony Wickstead and credited to Michael Elliott. The paper credits Jaume de Dios Pont for an earlier Lean formalization of this result.”
Project
Sources
LeanOrderClosures.exists_weaklyFatou_not_equivalent_fatou

TheoremRank parity and complex structures on the Kalton–Peck space#

Develops symplectic Fredholm theory and the real Kalton–Peck space to prove rank parity of finite-rank perturbations and rule out a complex structure on a hyperplane.

Quoted from the card LeanPool/projects/kaltonpeck.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanKaltonPeck.noHyperplaneComplexStructure

TheoremRellich–Kondrachov compact embedding theorem#

Formalizes the Rellich–Kondrachov compact embedding theorem: the Sobolev embedding H¹ → L² is a compact operator on compact Riemannian manifolds. The proof builds the Euclidean core (compactness of the H¹ → L² inclusion on a fixed compact support via the Fréchet–Kolmogorov criterion and the H¹ translation estimate ‖τₐu − u‖₂ ≤ ‖a‖ · ‖∇u‖₂), glues chart contributions over a finite atlas, and specializes to the Levi-Civita Riemannian volume measure.

Quoted from the card LeanPool/projects/rellich-kondrachov.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 3 main results, each with its informal statement quoted from the card. The scan finds 3 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanRellichKondrachov.Geometry.Manifold.Sobolev.exists_riemannianFiniteChartData

TheoremUnconditional Schauder Bases#

Develops an API for Schauder bases and unconditional Schauder bases of complete normed spaces, including ordered partial-sum convergence, rearrangement criteria for unconditionality, and an arbitrary-index variant built on unconditional summability, then proves a finite sign criterion: a family with dense closed span, nonzero vectors, and a uniform finite sign bound is the basis of an unconditional Schauder basis.

Quoted from the card LeanPool/projects/unconditional-schauder-basis.yaml of LeanPool/lean-pool at commit 2b205bf9, Apache-2.0.

Main results

The card lists 2 main results, each with its informal statement quoted from the card. The scan finds 2 of their declarations in the project's files at commit 2b205bf9. A found declaration links its page in Lean Pool's documentation, which Lean Pool rebuilds daily from its main branch, and its line at this commit.

Project
Sources
LeanUnconditionalCriterion.exists_unconditionalSchauderBasis_of_finiteSignBound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.