Jingwei Liang (梁经纬)

Plug-and-Play (PnP) algorithms are a class of iterative methods for inverse imaging. Within an optimization algorithm, they combine a flexible fidelity term, encoding the forward operator, and a pretrained image denoiser, in order to deal with more severe corruptions such as blurring or downsampling when reconstructing an image. This work studies provably convergent PnP methods for mixed-noise forward processes by using the infimal convolution as a fidelity term, providing a statistical interpretation as a joint maximum a-posteriori estimator over both noises, and preserving the Bayesian MAP interpretation of PnP methods. Independently, we extend the PnP formulation to multiple prior terms using the Davis–Yin three-operator splitting. This extension can be combined with either standard fidelities or the proposed mixed-noise infimal-convolution fidelities. We verify that these generalized PnP methods are convergent under standard Kurdyka–Lojasiewicz conditions. Numerical experiments on Laplace-Gaussian and Poisson–Gaussian noise demonstrate stable convergence of single-prior and multiple-prior PnP methods, and divergence under fidelity mismatch. Furthermore, PnP with infimal convolution fidelities are able to scale to noise up to 38% standard deviation, with multiple priors reaching different stationary points that qualitatively preserve more textural properties.

Optimal transport (OT) compares distributions and aligns datasets in machine learning, yet unregularized discrete OT requires a linear program with quadratically many transport variables. We propose HELLO, a hierarchical solver that casts large-scale discrete OT as edge localization and uses dual potentials to guide both coarse-to-fine initialization and within-level refinement. Initialization propagates coarse dual potentials across a recursive subsampling hierarchy to assign candidate edges. Refinement then iteratively inserts the largest dual violators in each row and column until the relative KKT residual meets a prescribed tolerance, while budgeted pruning ensures linear memory complexity. For exact-arithmetic refinement, we prove finite termination at a global optimum under a symbolic lexicographic rule. At the million-point scale, HELLO attains lower transport objectives with order-of-magnitude runtime improvements over strong baselines across feature dimensions from single digits to thousands. It further scales to 1.28 million samples per marginal in 8192 dimensions on a single H100, using 41.6 GiB peak GPU memory while satisfying a full relative KKT residual below 10^-6. Beyond standard discrete OT, the framework supports general pairwise costs and serves as a scalable balanced-OT oracle for semi-discrete OT, Gromov–Wasserstein, unbalanced OT, and OT-based Flow Matching.

Typical dimension reduction techniques for nonoverlapping sparse optimization involve screening or sieving strategies based on a dual certificate derived from the first-order optimality condition, approximating the gradients or exploiting certain inherent low-dimensional structure of the sparse solution. In comparison, dimension reduction rules for overlapping group sparsity are generally less developed because the subgradient structure is more complex, making the link between sparsity pattern and the dual variable indirect due to the non-separability. In this work, we propose new dual certificates for overlapping group sparsity and a novel adaptive scheme for identifying the support of the overlapping group LASSO. We demonstrate how this scheme can be integrated into and significantly accelerate existing algorithms, including Primal-Dual splitting method, alternating direction method of multipliers and a recently developed variable projection scheme based on over-parameterization. We provide convergence analysis of the method and verify its practical effectiveness through experiments on standard datasets.

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel’skiĭ–Mann iteration and Halpern iteration are two widely used schemes. In this work, we formalize the convergence of these two fixed-point algorithms in the interactive theorem prover Lean4 based on type dependent theory. To this end, weak convergence and topological properties in the infinite-dimensional real Hilbert space are formalized. Definition and properties of nonexpansive operators are also provided. As a useful tool in convex analysis, we then formalize the Fejér monotone sequence. Building on these foundations, we verify the convergence of both the iteration schemes. Our formalization provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces. Our code is available at https://github.com/TTony2019/fixed-point-iterations-in-lean.