Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
Sup- and Inf-Convolutions of Bounded Viscosity Sub- and Supersolutions of the Penalty-Drift Equation with a Convex Penalty
lemmalem:penalty-drift-sup-inf-convolution-euclidean-2026aAnalysisPDEFor the penalty-drift equation with a penalty whose gradient is monotone and which satisfies the dissipation inequality, the penalised sup-convolution of a bounded viscosity subsolution (and the penalised inf-convolution of a bounded viscosity supersolution) is attained at points…The Relative Free Energy and the Relative Score of a Probability Measure for a Potential on an Open Set
definitiondef:relative-free-energy-score-euclidean-2026aAnalysisProbabilityFor a twice continuously differentiable potential on an open set and a positive temperature, the relative free energy of a probability measure concentrated on the set is temperature times entropy plus the integral of the potential, and its relative score is the gradient of the po…The Mean-Field Limit of the Lifted N-Particle Hamilton-Jacobi Equation with a Mollified Local Coupling
theoremthm:n-particle-local-coupling-limit-wasserstein-2026aAnalysisProbabilityPDEWith eps_N -> 0 and N eps_N^d -> infinity, the bounded solutions U_N of the lifted N-particle equations with the mollified N-particle costs satisfy U_N(mu^{tensor N})/N -> u(mu) uniformly on energy sublevel sets, and are asymptotically bounded below by u at one-particle marginals…Lower Convergence: The Solution with the Local Cost Is Asymptotically below the Mean-Field Solutions with the Mollified Costs
corollarycor:n-particle-mollified-lower-convergence-wasserstein-2026aAnalysisProbabilityPDEIf eps_N tends to 0, the bounded solution of the equation with the local density cost is, uniformly on energy sublevel sets, asymptotically below the bounded solutions of the mean-field equations with the mollified mean-field costs.Upper Convergence: Mean-Field Solutions with the Tensor-Averaged Mollified Costs Are Asymptotically below the Solution with the Local Cost
corollarycor:n-particle-mollified-upper-convergence-wasserstein-2026aAnalysisProbabilityPDEIf N eps_N^d tends to infinity, the bounded solution of the mean-field equation with the tensor-averaged cost of the mollified N-particle cost is, locally uniformly on energy sublevel sets, asymptotically below the bounded solution of the equation with the local density cost.The Mollified N-Particle Cost Dominates N Times the Mollified Mean-Field Cost of the One-Particle Marginal
lemmalem:mollified-cost-marginal-domination-wasserstein-2026aAnalysisProbabilityPDEFor every P in P_2(R^{dN}), N g_eps(P^{[1]}) <= int c_{N,eps} dP: the linear part is exact through the one-particle marginal and the density part follows from Jensen's inequality pointwise and Tonelli's theorem.The Mollified N-Particle Cost: Regularity, Its Tensor-Averaged Cost, and the Defect against the Local Cost
lemmalem:mollified-cost-tensor-average-wasserstein-2026aAnalysisProbabilityPDEThe mollified mean-field and N-particle costs are bounded and uniformly continuous; the tensor-averaged cost of the N-particle cost is the linear cost plus the tensor average of the mollified density cost at the empirical measure; and its excess over the local cost is bounded by…The Mollified Mean-Field Cost and the Mollified N-Particle Cost of a Local Coupling
definitiondef:n-particle-mollified-cost-wasserstein-2026aAnalysisProbabilityPDEDefines the mollified mean-field cost g_eps(nu) = int f dnu + G_{Phi,eps}(nu) on P_2(R^d) and the mollified N-particle cost c_{N,eps}(x) = N g_eps(mu^N_x) on R^{dN}, the empirical-measure form of a mollified local coupling.The Mean Distance Between the Mollified Empirical Measure and the Mollified Measure
lemmalem:mollified-empirical-fluctuation-euclidean-2026aAnalysisProbabilityFor N particles drawn from the tensor power of a measure mu with finite second moment, the expected Lebesgue L^1 distance between the mollified empirical measure and the mollified measure at scale eps <= 1 is at most the square root of kappa_d R^d S eps^{-d}/N plus 2 M_2(mu)/(R-1…Mean-Square Deviation of the Empirical Average of a Bounded Borel Function under a Tensor Power
lemmalem:empirical-average-variance-euclidean-2026aAnalysisProbabilityUnder the N-fold tensor power of a probability measure rho, the integral of a bounded Borel function phi against the empirical measure has mean-square deviation (int phi^2 d rho - (int phi d rho)^2)/N from its mean, which is at most (int phi^2 d rho)/N.The Mollified Density Cost is Bounded, Lipschitz for the Wasserstein Distance, and Below the Density Cost
lemmalem:mollified-density-cost-properties-wasserstein-2026aAnalysisProbabilityThe mollified density cost with a convex Lipschitz integrand of constant L takes values in [0,L], is Lipschitz on the Wasserstein space with an explicit constant depending on L, the kernel and eps, and never exceeds the density cost of an absolutely continuous measure.The Mollified Density Cost of a Probability Measure with Finite Second Moment
definitiondef:mollified-density-cost-euclidean-2026aAnalysisProbabilityFor a convex Lipschitz integrand, a mollifier kernel and a scale eps, the mollified density cost of a probability measure with finite second moment is the Lebesgue integral of the integrand applied to its mollified density.Mollifying a Probability Measure on Euclidean Space: Kernel Bounds, the Translation Estimate, the Mollified Density and Its Cost
lemmalem:mollified-measure-density-euclidean-2026aAnalysisProbabilityIntegrating a rescaled mollifier kernel of radius eps against a probability measure on R^d gives a continuous probability density bounded by eps^{-d} times a bound of the kernel; translating the rescaled kernel by h changes it in L^1 by at most an explicit constant over eps times…Supporting Lines, Composition and Jensen's Inequality for a Convex Lipschitz Integrand
lemmalem:jensen-integral-convex-integrand-2026aAnalysisProbabilityA convex Lipschitz integrand has a supporting line at every point of the half-line; composed with a nonnegative measurable function it stays measurable and lies between 0 and L times the function; and on a probability space it satisfies Jensen's inequality.Stability of Comparison on the Wasserstein Space under Locally Vanishing Cost Defects
theoremthm:stability-cost-defect-wasserstein-2026bAnalysisProbabilityPDELet F satisfy the hypotheses of the comparison principle, and let F_n, F'_n be operators with F - h_n <= F_n and F'_n <= F + h'_n, where the defects h_n, h'_n take values in [0,H] and tend to zero uniformly on every set of measures with bounded penalty and bounded score. If u_n i…Lipschitz Dependence of the Bounded Viscosity Solution of the Langevin Hamilton-Jacobi Equation with a Density Cost on the Running Cost
corollarycor:langevin-density-cost-cost-lipschitz-wasserstein-2026aAnalysisProbabilityPDEFor two bounded uniformly continuous running costs g, g' with sup|g-g'| <= k, the bounded viscosity solutions u, u' of the corresponding Langevin Hamilton-Jacobi equations with common noise and density cost satisfy |u-u'| <= k/lambda_0 on the penalty domain. Proof: u'+k/lambda_0…Adding a Constant to a Viscosity Subsolution or Supersolution on the Wasserstein Space
lemmalem:constant-shift-viscosity-wasserstein-2026aAnalysisProbabilityPDEIf u is a viscosity subsolution of F relative to a penalty pair and F'(nu,r+s,q,Y) <= F(nu,r,q,Y) everywhere, then u+s is a viscosity subsolution of F'; symmetrically for supersolutions with the reverse inequality. The delta-envelopes of u+s are those of u shifted by s.The Potential Gradient Paired with the Score, and a Fisher Information Bound on the Domain of the Langevin Free-Energy Pair
lemmalem:langevin-fisher-bound-euclidean-2026aAnalysisProbabilityOn the domain of the Langevin free-energy pair, the pairing of the potential gradient with the score equals minus the mean Laplacian of the potential, that is minus the trace of the translation Hessian; consequently sigma^4/4 times the Fisher information is at most the squared no…Translation and Mollification Estimates in the Integrable Norm for a Density of Finite Fisher Information, and the Mollified Density Cost
lemmalem:score-translation-l1-euclidean-2026aAnalysisProbabilityFor an absolutely continuous measure with finite second moment and finite Fisher information, translating its density by z moves it by at most |z| times the square root of the Fisher information in the integrable norm; mollifying at scale eps moves it by at most eps times that ro…The Structure Estimate at a Maximiser for Operators within a Cost Defect of a Reference Operator
lemmalem:comparison-estimate-cost-defect-wasserstein-2026bAnalysisProbabilityPDEFor a subsolution of one operator and a supersolution of another, each within a bounded zeroth-order defect of a reference operator satisfying the comparison hypotheses, a nonnegative supremum of the Wasserstein-doubled difference of their delta-envelopes is attained at a pair in…