精读笔记

Problem Setting

这篇论文处理的是 Ekeland 变分原理在 BISH 构造数学中的可证明版本。问题不是 classical EVP 是否为真，而是其中的存在性证明是否携带可计算/可构造内容。

真正困难点有三个。第一，在 BISH 中“bounded below”不意味着 infimum 存在，因此 classical proof 一开始就不可用。第二，即便函数连续、空间局部紧，也不能构造性地证明所有 lower sections L(f,λ) 都全有界或紧；只能在排除可数多坏阈值后得到紧性。第三，经典证明里常用的嵌套紧集交非空、序列紧性、极小值达到等步骤，在构造数学中都可能等价于额外非构造原则。

所以关键矛盾是：EVP 本质上是一个“存在近似极小点”的原则，但构造数学不允许通过不可计算的 infimum/compactness 自动抽取这个点。本文的任务就是重新组织证明，使每一步都只使用可构造的 infimum、可构造的紧 lower section、以及可计算收缩。

Motivation

已有 classical EVP 的路线在构造语境下不够，不是因为结论形式小修小补即可，而是因为其证明依赖的基础对象本身不可构造。特别是，有下界的实数集没有必然 infimum；紧空间上的连续函数有 infimum，但不一定能证明达到 minimum；lower section 的紧性也只在“除可数例外”的层面可控。

作者的核心观察是：如果不能直接构造 minimizer，就应该构造一列越来越小的可控 lower sections，并让它们的直径趋零。这样最后得到的点不是从非构造选择中抽出来的，而是由 Cauchy 收缩过程产生。

关键缺口是 constructive optimisation 中缺少一个能替代 classical EVP 的基础工具。本文试图填补的是“在没有非构造紧性原则的情况下，如何仍然得到 Ekeland 型近似最优性”的证明模板。

Core Idea

论文的核心思想是：把 EVP 的点存在性问题改写为一列 compact lower sections 的收缩问题。给定当前点 x_n，考虑惩罚函数 g_n(x)=f(x)+cρ(x,x_n)，再选择一个避开坏阈值的 ε_n，使 K_n=L(g_n,f(x_n)-ε_n) 在构造意义下紧。随后在 K_n 上选取一个近似 infimum 点 x_{n+1}，并重复。这个过程避免了要求真正 minimizer 存在。

它理论上成立的原因是，近似最小性会强制后续 lower section 的直径下降：如果 x_n 已经接近 K_{n-1} 上的 inf f，那么 K_n 中任一点离 x_n 都不能太远，否则惩罚项会使其不可能低于阈值。于是 K_n 递降且 diam(K_n)→0，构造上可以得到唯一极限点 v。

和 prior 的本质区别在于，这不是在 classical EVP 上做语义解释，而是重写了证明的几何结构：从“全局完备空间 + lsc + bounded below”转向“局部紧空间 + 连续函数 + explicit infimum + good lower sections”。新增的 inductive bias 是局部紧化与阈值避让，而不是 classical 的全局序列紧性或 Zorn-like 选择。

Method

1. lower section 闭性：作者先证明 sequentially continuous f 的 epigraph 和 lower sections 是闭的。它解决的是后续把 lower section 当作 closed subspace 使用的问题。这里的作用不是创新，而是确保构造环境下闭性不偷用排中律。

2. 好阈值紧性：Proposition 2/4 是技术支点。紧空间上连续函数的 lower section 对除可数多 λ 外紧；局部紧空间中通过紧球耗尽，把这个结论推广到 L(f,λ) 局部紧。它解决的是“不能对所有 λ 证明 lower section 紧”的构造障碍。核心变化是从 uniform-for-all thresholds 改成 avoid-countably-many-bad-thresholds。

3. 距离惩罚保证有界性：Corollary 5 对 g(x)=f(x)+cρ(x,a) 建立 infimum 存在，并证明好阈值下 L(g,λ) 紧。距离惩罚项让 lower section 自动有界，这是把局部紧性转化为紧性的关键。

4. 嵌套 compact sections 构造：Theorem 7 中递归构造 K_n、x_n、ε_n。每一步要么发现当前点已满足近似 EVP 条件并停机式稳定，要么生成一个更小的紧 lower section。它解决的是不能直接取极小点的问题。

5. 直径收缩替代非构造交集：Proposition 6 要求 diam(K_n)→0，从而构造唯一交点。这个条件不是装饰，而是避免 classical sequential compactness 的关键；文中还用 Brouwerian example 说明若去掉直径收缩，会导出 LLPO 这类非构造原则。

Key Insight / Why It Works

最关键的 insight 是：constructive EVP 的障碍不在 Ekeland 不等式本身，而在“从下有界函数中抽取足够低的点”的证据结构。作者通过 lower section 的可紧化，把抽取问题变成一个显式收缩过程。

真正有效的是三者组合：距离惩罚带来 coercivity-like boundedness；好阈值选择带来 compactness；近似 infimum 选择带来 diameter contraction。单独任何一项都不够。距离惩罚如果没有局部紧性，只能给有界性，不能给 compactness；好阈值紧性如果没有收缩估计，只能得到嵌套紧集，构造上仍不能保证交非空；近似 infimum 如果没有紧 lower section，则 infimum 本身可能不可用。

最可能的核心贡献是 Theorem 7 的证明组织方式，而不是 Proposition 1 这类基础闭性结论。Proposition 2 是已有 constructive analysis 结果，本文的贡献在于把它嵌入 EVP proof，使“可数坏阈值”从障碍变成可绕开的参数选择机制。

这里没有 scaling/data/retrieval 一类问题；如果类比机器学习术语，它更像是 better inductive bias：把不可构造的全局存在性替换为局部紧化 + 收缩式证据。辅助部分是对 continuity/compact image 等概念的铺垫，必要但不是主要新意。

一个直接判断：本文得到的是 constructive counterpart，而不是 classical EVP 的无损构造化。ε 松弛、局部紧性、inf f exists 这些限制不是小代价，而是构造可证明性的核心成本。

Relation To Prior Work

最接近的是 classical Ekeland Variational Principle 及 Bishop/Bridges 系列 constructive analysis 中关于 compact metric spaces、infimum、fan theorem、unique maxima 的工作。本文属于 constructive optimisation theory，而不是 nonlinear analysis 中常规 EVP 推广。

与 classical EVP 的本质差异：classical 版本只要求 complete metric space、lower semicontinuous、bounded below；本文要求 locally compact、continuous、inf f exists，并得到带 ε 的近似 strict inequality。也就是说，它牺牲了适用范围，换取了构造有效性。

看似新的 lower section 技术本身并非完全新，Proposition 2 直接引用 Bishop & Bridges；嵌套 compact sets 的直径收缩也属于构造数学中的标准安全模式。实质创新在于把这些碎片组合成 EVP 的构造证明，并明确指出哪些 classical 步骤会导向非构造原则。

从技术谱系看，它不是对 EVP 的参数改良，而是对证明原则的替换：从 classical completeness/semicontinuity/infimum machinery，转向 located compactness、good sections、dependent choice 和 Cauchy contraction。

Dataset / Evaluation

没有 dataset，也没有实验 evaluation。本文的 evaluation 是证明层面的：是否在 BISH 中推出一个 EVP-like theorem，并且证明中不调用非构造原则。

从 claim 支撑看，Theorem 7 确实支撑了“constructive counterpart”的主张，但不支撑“完整 constructive EVP”的更强说法。它验证的是在局部紧、连续、infimum 已存在条件下的 approximate EVP，而非 classical EVP 的全域构造化。

文中通过 Brouwerian example 说明某些 classical compactness 推理不可构造，这比一般数学论文中的反例更有价值：它解释了为什么作者必须加入 diam(K_n)→0 这样的条件。不过，文中未充分说明该版本在实际优化控制问题中的覆盖范围；应用层面的有效性基本没有展开。

Limitation

最大的限制是局部紧性。classical EVP 的重要应用大量发生在无限维 Banach 空间、函数空间、控制空间中，这些空间通常不局部紧。因此本文版本更像是 constructive analysis 内部的基础结果，而不是直接替代 classical EVP 的通用工具。

第二，连续性假设强于 lower semicontinuity。classical EVP 的威力很大一部分来自 lsc + completeness 的组合；本文要求 Bishop-style continuity，并通过 compact image 附近的 uniform continuity 保证组合性质。这是构造上合理的，但明显缩窄了函数类。

第三，inf f exists 是显式前提。它把 classical bounded below 的一部分负担转移给用户：在应用中你必须先构造 infimum，不能只证明有下界。这不是 implementation detail，而是方法成立的关键前提。

第四，结论有 ε 松弛。Theorem 7 的第二个不等式是 f(v)<f(x)+cρ(v,x)+ε，而 classical EVP 是无 ε 的 strict variational inequality。这个损失可能是本质的，也可能是当前证明技术的代价；文中未充分说明。

第五，阈值避让机制依赖“除可数多坏值外”的选择。它很优雅，但也说明证明对 lower section 的可紧性非常敏感；如果目标问题中没有办法有效识别或避开坏阈值，应用时可能仍然卡住。

Takeaway

• 1. 构造化 EVP 的关键不是重写结论，而是重写证明中的存在性来源：从非构造极小点抽取变成可控 lower sections 的收缩。
• 2. 距离惩罚项在这里的真正作用是把局部紧性提升为 lower section 紧性；它不是普通 regularization，而是 constructive compactness generator。
• 3. “除可数多阈值外成立”是一个值得迁移的 constructive proof pattern：不强求全参数一致成立，而是在递归构造中动态避开坏参数。
• 4. 未来真正值得做的是弱化局部紧性，寻找适用于无限维空间的 effective compactness/coercivity 替代条件；否则该版本与 classical EVP 的主战场仍有距离。

一句话总结

这篇论文把 Ekeland 变分原理从 classical 的完备性—下半连续性存在定理，重构为一个依赖局部紧性、好阈值 lower sections 和直径收缩的 Bishop-style constructive optimisation 原理。