AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate

Samplinglib mathematical lesson

Actual PBPS zero-safe bounce, rate and energy-layer bound

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product Borel space, including rank zero. Let V:E→ℝ be C² on all E, let α,β≥0 satisfy 0<α≤β and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E, and let η>0 with βη≤1. For all y,xRef∈E define c=y−η∇V(xRef), h(xRef,x)=∇V(x)−∇V(xRef), R(n,p)=p−(2⟨p,n⟩/‖n‖²)n with total real division, S(xRef,(x,p))=(x,R(h(xRef,x),p)), λ(xRef,(x,p))=√η max(0,⟨p,h(xRef,x)⟩) and H(y,xRef,(x,p))=(η⁻¹‖x−c‖²+‖p‖²)/2. Then: (1) S is jointly Borel measurable in (xRef,x,p); (2) λ is jointly continuous; (3) λ is jointly Borel measurable; (4) R(0,p)=p for every p; (5) for every n,p, R(n,R(n,p))=p, ‖R(n,p)‖=‖p‖ and ⟨R(n,p),n⟩=−⟨p,n⟩; (6) for every xRef,z, S fixes the position coordinate and S(xRef,S(xRef,z))=z; (7) H(y,xRef,S(xRef,z))=H(y,xRef,z) for all y,xRef,z; (8) λ(xRef,z)≥0, λ(xRef,S(xRef,z))=√η max(0,−⟨p,h(xRef,x)⟩) and λ(xRef,z)−λ(xRef,S(xRef,z))=√η⟨p,h(xRef,x)⟩; (9) h(xRef,x)=0 implies both S(xRef,(x,p))=(x,p) and λ(xRef,(x,p))=0; (10) for every y,xRef,z₀ put ℰ=H(y,xRef,z₀). Then ℰ≥0, and every z=(x,p) with H(y,xRef,z)=ℰ obeys ‖p‖≤√(2ℰ), ‖x−c‖≤√(2ηℰ) and λ(xRef,z)≤√η β√(2ℰ)(√(2ηℰ)+‖c−xRef‖). The gradient β-Lipschitz bound is derived internally from the canonical Hessian producer, never supplied as a new premise. The original six callers persist. Positive α, α≤β and βη≤1 remain standing conditions unused by this bounded deterministic BODY; C², the global Hessian bounds and η>0 supply the proof. No joint continuity of S is claimed at its zero-normal locus. This result supplies actual jump/rate prerequisites for Algorithm1/AppendixA.1 Proposition3.1; random clocks, path construction, nonexplosion, invariant and terminal kernels, convergence and costs remain open.

\[c=y-\eta\nabla V(x_{\rm ref}),\quad h=\nabla V(x)-\nabla V(x_{\rm ref}),\quad R(n,p)=p-\frac{2\langle p,n\rangle}{\|n\|^2}n,\quad R(0,p)=p.\quad S(x_{\rm ref},(x,p))=(x,R(h,p)),\quad\lambda(x_{\rm ref},(x,p))=\sqrt\eta\max\{0,\langle p,h\rangle\},\quad H=\tfrac12(\eta^{-1}\|x-c\|^2+\|p\|^2).\quad H(Sz)=H(z),\quad\lambda(z)-\lambda(Sz)=\sqrt\eta\langle p,h\rangle,\quad\lambda(z)\le\Lambda_{\mathcal E}=\sqrt\eta\,\beta\sqrt{2\mathcal E}\bigl(\sqrt{2\eta\mathcal E}+\|c-x_{\rm ref}\|\bigr)\quad(H(z)=\mathcal E).\]

Lean statement · actual_bounce_rate_energy_laws

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 actual_bounce_rate_energy_laws
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) :
    actual_bounce_rate_energy_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_bounce_rate_energy_statement

This literal definition stores the complete proposition asserted above. It supplies no mathematical proof or additional hypothesis; the theorem proof must establish its value.

Download module (.lean)

private def actual_bounce_rate_energy_statement
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ) * ‖v‖ ^ 2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ) * ‖v‖ ^ 2)
    (hη : 0 < η) (hβη : (β : ℝ) * η ≤ 1) : Prop :=
    let c : E → E → E := fun y xRef => y - η • gradient V xRef
    let h : E → E → E := fun xRef x => gradient V x - gradient V xRef
    let R : E → E → E := fun n p =>
      p - (2 * inner ℝ p n / ‖n‖ ^ 2) • n
    let S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, R (h xRef z.1) z.2)
    let rate : E → (E × E) → ℝ := fun xRef z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (h xRef z.1))
    let H : E → E → (E × E) → ℝ := fun y xRef z =>
      (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
    Measurable (fun a : E × (E × E) => S a.1 a.2) ∧
    Continuous (fun a : E × (E × E) => rate a.1 a.2) ∧
    Measurable (fun a : E × (E × E) => rate a.1 a.2) ∧
    (∀ p : E, R 0 p = p) ∧
    (∀ n p : E, R n (R n p) = p ∧ ‖R n p‖ = ‖p‖ ∧
      inner ℝ (R n p) n = -inner ℝ p n) ∧
    (∀ xRef : E, ∀ z : E × E,
      (S xRef z).1 = z.1 ∧ S xRef (S xRef z) = z) ∧
    (∀ y xRef : E, ∀ z : E × E,
      H y xRef (S xRef z) = H y xRef z) ∧
    (∀ xRef : E, ∀ z : E × E, 0 ≤ rate xRef z ∧
      rate xRef (S xRef z) =
        Real.sqrt η * max 0 (-inner ℝ z.2 (h xRef z.1)) ∧
      rate xRef z - rate xRef (S xRef z) =
        Real.sqrt η * inner ℝ z.2 (h xRef z.1)) ∧
    (∀ xRef x p : E, h xRef x = 0 →
      S xRef (x,p) = (x,p) ∧ rate xRef (x,p) = 0) ∧
    (∀ y xRef : E, ∀ z₀ : E × E,
      0 ≤ H y xRef z₀ ∧
      ∀ z : E × E, H y xRef z = H y xRef z₀ →
        ‖z.2‖ ≤ Real.sqrt (2 * H y xRef z₀) ∧
        ‖z.1 - c y xRef‖ ≤ Real.sqrt (2 * η * H y xRef z₀) ∧
        rate xRef z ≤ Real.sqrt η * (β : ℝ) *
          Real.sqrt (2 * H y xRef z₀) *
          (Real.sqrt (2 * η * H y xRef z₀) + ‖c y xRef - xRef‖))

Exact module and namespace context

Proof roadmap

1Derive the gradient bound internally
Finite dimension supplies completeness. Apply the existing quadratic-regularization Hessian theorem with r=0 to obtain LipschitzWith β (gradient V), hence continuity of the actual gradient. This closes a proof ingredient without adding a caller.
2Identify the zero-safe orthogonal reflection
Total division gives R(0,p)=p. For all n, R is the existing isometric reflection in the orthogonal complement of span(n). Its square is identity and it preserves norm. Expanding the inner product gives its sign reversal; the nonzero branch uses ‖n‖²≠0, while n=0 is handled separately.
3Check Borel and continuous operations
The state-dependent reflection uses continuous gradients, inner products and norms, together with total real division, which is Borel. Thus S is jointly Borel, including h=0. The positive-part rate uses no quotient, so it is jointly continuous and consequently Borel. Joint continuity of S is not required or asserted.
4Prove the actual bounce and rate identities
The position stays fixed, so its residual h stays fixed. Reflection involution proves S²=I and norm preservation proves exact H conservation. Its pairing sign reversal gives the flipped rate. For a=⟨p,h⟩, the two sign cases prove max(0,a)−max(0,−a)=a. The zero-residual case gives identity and zero rate.
5Keep zero energy and collect the first nine laws
η>0 makes η⁻¹ nonnegative, so H is nonnegative as the weighted sum of two squared vector norms divided by two. Collect the first nine laws, then fix arbitrary y,xRef,z₀ and z on its actual energy layer.
6Extract the two energy-layer radii
The equality H(z)=ℰ gives η⁻¹‖x−c‖²+‖p‖²=2ℰ. Dropping each nonnegative summand gives the momentum radius and, after multiplication by positive η, the position radius. Taking square roots requires no ℰ>0 and no division by ℰ.
7Derive the exact pointwise majorant
The triangle inequality bounds ‖x−xRef‖ by ‖x−c‖+‖c−xRef‖. Apply the internally derived β-Lipschitz estimate to h, then Cauchy–Schwarz and max(0,⟨p,h⟩)≤‖p‖‖h‖. Insert both radii and multiply by √η≥0. The resulting Λ is the printed same-energy-layer majorant, not a stochastic path or cost bound.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with compatible norm and its Borel measurable structure; products have product structures. Rank zero is allowed.
V:E→ℝ is C² on all E. The nonnegative α,β satisfy 0<α and α≤β, with α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E.
η is real, η>0 and βη≤1. These are the original six analytic callers. No gradient-Lipschitz, nonzero-normal, positive-energy, positive-dimension, flow or stochastic-law certificate is a caller.
All y,xRef,x,p are independent arbitrary points of E. Define c,h,R,S,λ,H exactly as displayed. Real division is total, so R(0,p)=p. H is a weighted sum of separate vector squared norms.
The final bound quantifies each z₀ and each z in the SAME actual H energy layer. It assumes no strictly positive energy or positive majorant; no division by either occurs.

Mathematical proof

1. Derive the gradient bound internally

Finite dimension supplies completeness. Apply the existing quadratic-regularization Hessian theorem with r=0 to obtain LipschitzWith β (gradient V), hence continuity of the actual gradient. This closes a proof ingredient without adding a caller.

\[\|\nabla V(x)-\nabla V(u)\|\le\beta\|x-u\|.\]

Corresponding Lean step

  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  have hLip : LipschitzWith β (gradient V) := by
    simpa using
      (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
        (m := α) (L := β) (r := 0) hV hH (0 : E)).2
  have hgrad : Continuous (gradient V) := hLip.continuous