Samplinglib mathematical lesson

MonotoneProximalMap actual source component

AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap.nonexpansive_of_monotone_optimality · theorem · Teaching coverage

Read this first

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.

\[\|p(x)-p(y)\|\le\|x-y\|.\]

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.

Download module (.lean)

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

Exact module and namespace context

Proof 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.

\[x-y=d+\eta e,\qquad\|d\|^2\le\langle x-y,d\rangle.\]

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.

\[\|d\|^2\le\|x-y\|\|d\|\Longrightarrow\|d\|\le\|x-y\|.\]

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.

Download module (.lean)

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.MonotoneProximalMap

Exact module and namespace context

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.