MonotoneProximalMap actual source component
AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimality · theorem · Teaching coverage
Mathematical statement
The given exact optimality solution p is 1-Lipschitz. This abstract implication is extracted verbatim from the existing private proof and is consumed by both the existing input-estimator theorem and the actual proximal-phase comparison. It carries no new mathematical-completion credit.
Lean statement · nonexpansive_of_monotone_optimality
Complete exact statement with all constructed source arrays, probability laws, terminal-query identities and Euclidean cost as applicable.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem nonexpansive_of_monotone_optimality
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
{g p : E → E} {eta : ℝ} (heta : 0 ≤ eta)
(hmono : ∀ x y, 0 ≤ inner ℝ (g x - g y) (x - y))
(heq : ∀ y, p y + eta • g (p y) = y) : LipschitzWith 1 pProof roadmap
- 1Subtract the genuine equations
Set d=p(x)-p(y) and e=g(p(x))-g(p(y)); subtract optimality. Pair with d and use eta≥0 and monotonicity. No nonexpansiveness premise is supplied.
- 2Cancel only for nonzero displacement
Cauchy-Schwarz gives ||d||²≤||x-y||||d||. The zero case is immediate; otherwise norm d is strictly positive, so cancellation is legitimate. This is the exact existing argument moved into one shared module.
Full assumptions and notation
All objects and hypotheses
- E is any real inner-product normed additive group; g,p:E→E, eta≥0.
- For every x,y, inner(g(x)-g(y),x-y)≥0, and for every y, p(y)+eta*g(p(y))=y. No differentiability, probability, finite dimension, existence or measurability is assumed or concluded by this abstract leaf.
Mathematical proof
1. Subtract the genuine equations
Set d=p(x)-p(y) and e=g(p(x))-g(p(y)); subtract optimality. Pair with d and use eta≥0 and monotonicity. No nonexpansiveness premise is supplied.
Corresponding Lean step
hsub; hpair; real_inner_smul_left
2. Cancel only for nonzero displacement
Cauchy-Schwarz gives ||d||²≤||x-y||||d||. The zero case is immediate; otherwise norm d is strictly positive, so cancellation is legitimate. This is the exact existing argument moved into one shared module.
Corresponding Lean step
real_inner_le_norm; hzero; hpos; LipschitzWith.of_dist_le_mul
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · nonexpansive_of_monotone_optimality
Entire current module is covered, including private phase, finite weighted difference, measurability, actual kernel and transport helpers. Extraction carries no new mathematical credit.
Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.
theorem nonexpansive_of_monotone_optimality
{E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
{g p : E → E} {eta : ℝ} (heta : 0 ≤ eta)
(hmono : ∀ x y, 0 ≤ inner ℝ (g x - g y) (x - y))
(heq : ∀ y, p y + eta • g (p y) = y) : LipschitzWith 1 p := by
apply LipschitzWith.of_dist_le_mul
intro x y
simp only [NNReal.coe_one, one_mul, dist_eq_norm]
have hsub : x - y = (p x - p y) + eta • (g (p x) - g (p y)) := by
calc
x - y = (p x + eta • g (p x)) - (p y + eta • g (p y)) :=
congrArg₂ (fun a b : E => a - b) (heq x).symm (heq y).symm
_ = _ := by module
have hpair : ‖p x - p y‖ ^ 2 ≤ inner ℝ (x - y) (p x - p y) := by
calc
_ ≤ ‖p x - p y‖ ^ 2 + eta * inner ℝ (g (p x) - g (p y)) (p x - p y) :=
le_add_of_nonneg_right (mul_nonneg heta (hmono (p x) (p y)))
_ = inner ℝ (x - y) (p x - p y) := by
conv_rhs => rw [hsub]
rw [inner_add_left, real_inner_smul_left, real_inner_self_eq_norm_sq]
have hbound := hpair.trans (real_inner_le_norm (x - y) (p x - p y))
by_cases hzero : ‖p x - p y‖ = 0
· simpa only [hzero] using norm_nonneg (x - y)
· have hpos : 0 < ‖p x - p y‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hzero)
nlinarith
end AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMapSource assumptions versus formal assumptions
| Source | Actual Lean | Difference kind | Why it matters |
|---|---|---|---|
| Source uses normalized Euclidean strongly convex C2 potential and true Euclidean phase distance. | E is any real inner-product normed additive group; g,p:E→E, eta>=0. | generalization | The abstract shared implication is an explicit prerequisite; paper consumer supplies its exact Hessian hypotheses. Main uses finite real inner-product coordinates and explicitly sqrt(sum squares), never default product max norm. |
| D2 gives universal C Lambda h delta under h²Lambda<=1 for arbitrary measurable delta-accurate oracle delta>=0; B1 includes further positivity/logarithmic claims. | Shared abstract prerequisite for source proximal nonexpansiveness; not an existence, algorithm, stochastic estimator or paper theorem. Actual paper consumers derive monotonicity and construct p themselves. | unresolved | Only D1/D2 one-phase comparison or a named prerequisite is asserted. Absolute-b proof is a faithful universal-constant route adapter, not a source assumption repair or completed B1. |
Shared abstract prerequisite for source proximal nonexpansiveness; not an existence, algorithm, stochastic estimator or paper theorem. Actual paper consumers derive monotonicity and construct p themselves.
Encoder–denoiser: accepted · equivalent-after-elaboration
A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.
Scope and omitted-condition boundaries
- Shared abstract prerequisite for source proximal nonexpansiveness; not an existence, algorithm, stochastic estimator or paper theorem. Actual paper consumers derive monotonicity and construct p themselves.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
Mathlib API called (external library)
- real_inner_le_norm
- real_inner_self_eq_norm_sq
- LipschitzWith.of_dist_le_mul
Mathematical sources
- SPHMC proximal phase and coefficient prerequisites — Shared abstract prerequisite for source proximal nonexpansiveness; not an existence, algorithm, stochastic estimator or paper theorem. Actual paper consumers derive monotonicity and construct p themselves.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.