Samplinglib mathematical lesson

Actual PBPS harmonic flow and conserved weighted energy

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_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 all x,v∈E, and assume η>0 and βη≤1. For every y,xRef∈E set c=y−η∇V(xRef), and for t∈ℝ, z=(x,p)∈E×E define Φ_t(z)=(c+cos(t)(x−c)+√η sin(t)p,−sin(t)(x−c)/√η+cos(t)p) and H(z)=(η⁻¹‖x−c‖²+‖p‖²)/2. Then (1) the map (y,xRef,t,z)↦Φ_t(z) is jointly continuous on (E×E)×ℝ×(E×E); (2) it is jointly Borel measurable; (3) Φ_0(z)=z; (4) Φ_{s+t}(z)=Φ_s(Φ_t(z)) for all real s,t; (5) Φ_{−t}(Φ_t(z))=Φ_t(Φ_{−t}(z))=z; (6) writing (X_t,P_t)=Φ_t(z), both time derivatives exist at every real t and satisfy dX_t/dt=√η P_t and dP_t/dt=−(X_t−y)/√η−√η∇V(xRef); (7) H(z)≥0; (8) H(Φ_t(z))=H(z); and (9) Φ_π(z)=(2c−x,−p). These conclusions quantify every displayed parameter and state. The original six source-standing callers persist; the deterministic calculation invokes C² through gradient continuity and η>0, while the two Hessian bounds, positive lower modulus and step cap are retained rather than used in its BODY. No energy positivity, positive dimension, strict endpoint or higher derivative assumption is added. This is the actual deterministic arc ingredient of the cited algorithm, with ASTIS supplying the omitted elementary continuity, group, differentiation and norm-cancellation bridges. It does not construct the stochastic trajectory, prove nonexplosion or identify an invariant/terminal sampling law.

\[c=y-\eta\nabla V(x_{\rm ref}),\quad\Phi_t(x,p)=\left(c+\cos t\,(x-c)+\sqrt\eta\sin t\,p,\,-\frac{\sin t}{\sqrt\eta}(x-c)+\cos t\,p\right).\quad H(x,p)=\frac{\eta^{-1}\|x-c\|^2+\|p\|^2}{2}\ge0,\quad H(\Phi_tz)=H(z),\qquad\Phi_\pi(x,p)=(2c-x,-p).\]

Lean statement · actual_harmonic_flow_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_harmonic_flow_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_harmonic_flow_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_harmonic_flow_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_harmonic_flow_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 Φ : E → E → ℝ → (E × E) → (E × E) := fun y xRef t z =>
      (c y xRef + Real.cos t • (z.1 - c y xRef) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y xRef) + Real.cos t • z.2)
    let H : E → E → (E × E) → ℝ := fun y xRef z =>
      (η⁻¹ * ‖z.1 - c y xRef‖ ^ 2 + ‖z.2‖ ^ 2) / 2
    Continuous (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) ∧
    Measurable (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) ∧
    (∀ y xRef : E, ∀ z : E × E, Φ y xRef 0 z = z) ∧
    (∀ y xRef : E, ∀ s t : ℝ, ∀ z : E × E,
      Φ y xRef (s + t) z = Φ y xRef s (Φ y xRef t z)) ∧
    (∀ y xRef : E, ∀ t : ℝ, ∀ z : E × E,
      Φ y xRef (-t) (Φ y xRef t z) = z ∧
      Φ y xRef t (Φ y xRef (-t) z) = z) ∧
    (∀ y xRef : E, ∀ t : ℝ, ∀ z : E × E,
      HasDerivAt (fun s : ℝ => (Φ y xRef s z).1)
        (Real.sqrt η • (Φ y xRef t z).2) t ∧
      HasDerivAt (fun s : ℝ => (Φ y xRef s z).2)
        (-(Real.sqrt η)⁻¹ • ((Φ y xRef t z).1 - y) -
          Real.sqrt η • gradient V xRef) t) ∧
    (∀ y xRef : E, ∀ z : E × E, 0 ≤ H y xRef z) ∧
    (∀ y xRef : E, ∀ t : ℝ, ∀ z : E × E,
      H y xRef (Φ y xRef t z) = H y xRef z) ∧
    (∀ y xRef : E, ∀ z : E × E,
      Φ y xRef Real.pi z = ((2 : ℝ) • c y xRef - z.1, -z.2))

Exact module and namespace context

Proof roadmap

1Establish the scale and joint continuity
Since η>0, r=√η is positive, nonzero and r²=η. The canonical ASTIS gradient-continuity theorem applies to V∈C² after lowering its differentiability order to one. Hence c depends continuously on (y,xRef), and the displayed trigonometric and scalar operations make Φ jointly continuous in all four inputs. Joint Borel measurability follows for the actual product Borel spaces; it is used when reassembling the conclusions.
2Verify identity, group composition and inverse
At time zero the sine vanishes and cosine is one. Expanding Φ_s(Φ_tz), the cosine and sine addition formulas identify both coordinates with Φ_{s+t}z; division is legitimate because √η≠0. Taking s=−t or t=−s yields both inverse identities. All times are real, with no domain restriction.
3Differentiate the two actual coordinates
Differentiate the sine and cosine expressions while fixing y,xRef and the initial state. The position derivative is −sin(t)(x−c)+r cos(t)p=rP_t. For momentum, −cos(t)(x−c)/r−sin(t)p equals −(X_t−y)/r−r∇V(xRef), using c=y−η∇V(xRef) and r²=η. HasDerivAt.congr_deriv changes only the vector derivative expression; it supplies no ODE hypothesis.
4Keep the weighted energy nonnegative
Both squared norms are nonnegative. Since η>0, its inverse is nonnegative, and dividing their weighted sum by two preserves nonnegativity. Zero initial energy is included.
5Cancel the mixed terms in the conserved energy
Put q=x−c, C=cos t and S=sin t. Translate the first coordinate back by c and expand each individual squared norm. The mixed terms are +2CS⟨q,p⟩/r and −2CS⟨q,p⟩/r, which cancel. The remaining sum is (C²+S²)(r⁻²‖q‖²+‖p‖²). Using C²+S²=1 and r²=η gives H(Φ_tz)=H(z), with the exact factor one half retained.
6Evaluate the half-turn and collect the nine laws
At t=π, sin π=0 and cos π=−1, so X_π=c−(x−c)=2c−x and P_π=−p. Collect the continuity/Borel, initial, group, two inverse, ODE, nonnegative-energy, conservation and half-turn conclusions. This endpoint belongs to a deterministic arc only; stochastic bounces may change the eventual terminal law.

Full assumptions and notation

All objects and hypotheses

E is a finite-dimensional real inner-product space with its norm and a measurable structure equal to its Borel structure. Rank zero is allowed; the product space uses its usual product structures.
V:E→ℝ is twice continuously Frechet differentiable on all E. The nonnegative moduli α,β satisfy 0<α and α≤β, and α‖v‖²≤D²V(x)[v,v]≤β‖v‖² for every x,v∈E.
The real step η satisfies η>0 and βη≤1. The endpoint αη=1 is allowed. The original six analytic callers are retained; only C² for gradient continuity and η>0 are invoked in this deterministic proof.
The parameters y,xRef range independently over E, the time variable over all real numbers, and z=(x,p) over E×E. The gradient is the Hilbert gradient of V; c,Φ,H are the exact displayed definitions.
H is a weighted SUM of the two individual squared vector norms, not the square of a product-space max norm. No nonzero energy, positive dimension, stochastic kernel, supplied flow certificate or higher derivative bound is assumed.

Mathematical proof

1. Establish the scale and joint continuity

Since η>0, r=√η is positive, nonzero and r²=η. The canonical ASTIS gradient-continuity theorem applies to V∈C² after lowering its differentiability order to one. Hence c depends continuously on (y,xRef), and the displayed trigonometric and scalar operations make Φ jointly continuous in all four inputs. Joint Borel measurability follows for the actual product Borel spaces; it is used when reassembling the conclusions.

\[r=\sqrt\eta>0,\quad r^2=\eta,\quad c(y,x_{\rm ref})=y-\eta\nabla V(x_{\rm ref})\ \text{is continuous}.\]

Corresponding Lean step

  have hr : 0 < Real.sqrt η := Real.sqrt_pos.2 hη
  have hr0 : Real.sqrt η ≠ 0 := ne_of_gt hr
  have hr2 : (Real.sqrt η) ^ 2 = η := Real.sq_sqrt hη.le
  have hgrad : Continuous (fun x : E => gradient V x) :=
    AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
      (hV.of_le (by norm_num))
  have hc : Continuous (fun a : E × E => c a.1 a.2) := by
    dsimp [c]
    fun_prop
  have hcont : Continuous (fun a : (E × E) × ℝ × (E × E) =>
      Φ a.1.1 a.1.2 a.2.1 a.2.2) := by
    dsimp [Φ]
    fun_prop