Samplinglib mathematical lesson

Actual PBPS finite-path energy and Gibbs/survival balance

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedGibbsSurvival.actual_prescribed_gibbs_survival_balance · theorem · Teaching coverage

Read this first

Mathematical statement

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E→R, alpha,beta≥0 and eta in R. Assume alpha>0, alpha≤beta, V is C2, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v in E, eta>0 and beta*eta≤1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n≥0 and horizon T≥0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0≤j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a≤s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). Define the actual positive-part event rate lambda_r(x,p)=sqrt(eta) max(0,<p,grad V(x)-grad V(r)>), and the target energy U_y(x,p)=V(x)+||x-y||^2/(2 eta)+||p||^2/2. The rate after momentum reversal is lambda_r(R(x,p)); it is evaluated on the same trajectory, not on a reversed-time trajectory. For every y,r,z,n,T,t as above, extend the actual prescribed path to real s by gamma(s)=Gamma(min(max(s,0),T)), with the argument understood as the nonnegative closed-interval subtype. Put A=Gamma(T), Iplus=integral from 0 to T of lambda_r(gamma(s)) ds, and Iminus=integral from 0 to T of lambda_r(R(gamma(s))) ds, both with real Lebesgue measure. Both integrands are interval integrable. The exact identities are U_y(A)-U_y(z)=Iplus-Iminus, exp(-U_y(z)) exp(-Iplus)=exp(-U_y(A)) exp(-Iminus). All finite event counts n≥0, horizons T≥0, rank-zero spaces and zero reflection normals are included. No positive jump-rate condition is imposed on the prescribed tuple. No measurability, integrability, energy identity or normalizing-constant premise is added to the six source assumptions. The simplex measure m is retained to preserve the existing path interface but is not used by these two scalar identities. The weights here are unnormalized; a common Gibbs normalizer would cancel but existence of the normalized stationary law is a separate obligation. This is the actual finite prescribed-path energy and Gibbs/survival identity in the Appendix A.1 reversal proof. It does not assert reversed-event density matching, pointwise time reversal at right-continuous jump values, weighted sector preservation, stationary averaging or invariant probability laws, restart/Markovness, hypocoercivity, implementation errors, expected oracle cost, main sampling results or actual-input composition.

\[U_y(A)-U_y(z)=I_+-I_-,\qquad e^{-U_y(z)}e^{-I_+}=e^{-U_y(A)}e^{-I_-}.\]

Lean statement · actual_prescribed_gibbs_survival_balance

Let E be a finite-dimensional real inner-product space with its Borel sigma algebra, including dimension zero. Let V:E->R, alpha,beta>=0 and eta in R. Assume alpha>0, alpha<=beta, V is C2, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v in E, eta>0 and beta*eta<=1. For y,r in E put c=y-eta grad V(r), h_r(x)=grad V(x)-grad V(r), R(x,p)=(x,-p), Phi_(y,r,u)(x,p)=(c+cos(u)(x-c)+sqrt(eta)sin(u)p, -sin(u)/sqrt(eta)(x-c)+cos(u)p), S_r(x,p)=(x,p-(2<p,h_r(x)>/||h_r(x)||^2)h_r(x)). Real division by zero is zero, so a zero normal gives the identity bounce. Let ell=volume_E tensor volume_E, with canonical Hilbert-space Lebesgue measure. For every integer n>=0 and horizon T>=0, let Delta_n(T) consist of real tuples 0<t_0<...<t_(n-1)<T. Equivalently, prepending 0 produces a strictly increasing tuple and every entry is less than T. Let Prefix_n(T) be this subtype and m_n,T the comap of Lebesgue measure on R^n under its inclusion. This is unnormalized simplex volume. For n=0 the tuple is empty and its zero-dimensional volume is one; for T=0 and n>0 the subtype is empty. Write q_0=0 and q_(j+1)=t_j. Starting at z_0=z, define z_(j+1)=S_r(Phi_(y,r,t_j-q_j)(z_j)) for 0<=j<n. Define records K_j=(q_j,z_j), each embedded in the live branch of (R_nonnegative x (E x E)) plus a cemetery symbol. For a general history of n+1 such records, the path reconstruction Psi at s in [0,T] starts from z and visits records in increasing index order: a live record (a,w) replaces the accumulator by Phi_(y,r,s-a)(w) exactly when a<=s; future records and cemetery records leave it unchanged. Here s-a is nonnegative subtraction. Define Gamma_(y,r,z,t)=Psi(K), the actual finite prescribed path; thus its value at an event is the post-bounce value. Let A_(y,r)(z,t)=Gamma_(y,r,z,t)(T). Define the actual positive-part event rate lambda_r(x,p)=sqrt(eta) max(0,<p,grad V(x)-grad V(r)>), and the target energy U_y(x,p)=V(x)+||x-y||^2/(2 eta)+||p||^2/2. The rate after momentum reversal is lambda_r(R(x,p)); it is evaluated on the same trajectory, not on a reversed-time trajectory. For every y,r,z,n,T,t as above, extend the actual prescribed path to real s by gamma(s)=Gamma(min(max(s,0),T)), with the argument understood as the nonnegative closed-interval subtype. Put A=Gamma(T), Iplus=integral from 0 to T of lambda_r(gamma(s)) ds, and Iminus=integral from 0 to T of lambda_r(R(gamma(s))) ds, both with real Lebesgue measure. Both integrands are interval integrable. The exact identities are U_y(A)-U_y(z)=Iplus-Iminus, exp(-U_y(z)) exp(-Iplus)=exp(-U_y(A)) exp(-Iminus). All finite event counts n>=0, horizons T>=0, rank-zero spaces and zero reflection normals are included. No positive jump-rate condition is imposed on the prescribed tuple. No measurability, integrability, energy identity or normalizing-constant premise is added to the six source assumptions. The simplex measure m is retained to preserve the existing path interface but is not used by these two scalar identities. The weights here are unnormalized; a common Gibbs normalizer would cancel but existence of the normalized stationary law is a separate obligation. This is the actual finite prescribed-path energy and Gibbs/survival identity in the Appendix A.1 reversal proof. It does not assert reversed-event density matching, pointwise time reversal at right-continuous jump values, weighted sector preservation, stationary averaging or invariant probability laws, restart/Markovness, hypocoercivity, implementation errors, expected oracle cost, main sampling results or actual-input composition.

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_prescribed_gibbs_survival_balance
    {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_prescribed_gibbs_survival_statement hα hαβ hV hH hη hβη

Exact module and namespace context

Full Lean proposition (definition) · actual_prescribed_gibbs_survival_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_prescribed_gibbs_survival_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 := by
  classical
  exact
    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 S : E → (E × E) → (E × E) := fun xRef z =>
      (z.1, z.2 - (2 * inner ℝ z.2 (gradient V z.1 - gradient V xRef) /
        ‖gradient V z.1 - gradient V xRef‖ ^ 2) • (gradient V z.1 - gradient V xRef))
    let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
    let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
    let Δ : (n : ℕ) → ℝ≥0 → Set (Fin n → ℝ) := fun n T =>
      {t | StrictMono (Fin.cons (0 : ℝ) t) ∧ ∀ i, t i < (T : ℝ)}
    let Prefix : (n : ℕ) → ℝ≥0 → Type := fun n T => {t : Fin n → ℝ // t ∈ Δ n T}
    let m : (n : ℕ) → (T : ℝ≥0) → Measure (Prefix n T) := fun n T =>
      Measure.comap (fun t : Prefix n T => t.val) (volume : Measure (Fin n → ℝ))
    let zAt : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Fin (n + 1) → (E × E) := fun y xRef z₀ n T t =>
      Fin.induction z₀ (fun i z =>
        S xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc) z))
    let K : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
        Prefix n T → Hist n := fun y xRef z₀ n T t j =>
      Sum.inl (Real.toNNReal ((Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) j), zAt y xRef z₀ n T t j)
    let Path : ℝ≥0 → Type _ := fun T => {s : ℝ≥0 // s ≤ T} → E × E
    let Ψ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Hist n → Path T :=
      fun y xRef z₀ n T h s =>
        Fin.foldl (n + 1) (fun z j => (h j).elim
          (fun a => if a.1 ≤ s.val then Φ y xRef ((s.val - a.1 : ℝ≥0) : ℝ) a.2 else z)
          (fun _ => z)) z₀
    let Γ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → Path T :=
      fun y xRef z₀ n T t => Ψ y xRef z₀ n T (K y xRef z₀ n T t)
    let R : E × E → E × E := fun z => (z.1, -z.2)
    let rate : E → E × E → ℝ := fun r z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V r))
    let U : E → E × E → ℝ := fun y z =>
      V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
    ∀ y r : E, ∀ z : E × E, ∀ n : ℕ, ∀ T : ℝ≥0, ∀ t : Prefix n T,
      let gamma : ℝ → E × E := fun s =>
        Γ y r z n T t ⟨min (Real.toNNReal s) T, min_le_right _ _⟩
      let A : E × E := Γ y r z n T t ⟨T, le_rfl⟩
      let Iplus : ℝ := ∫ s in (0 : ℝ)..(T : ℝ), rate r (gamma s)
      let Iminus : ℝ := ∫ s in (0 : ℝ)..(T : ℝ), rate r (R (gamma s))
      IntervalIntegrable (fun s => rate r (gamma s)) volume 0 (T : ℝ) ∧
      IntervalIntegrable (fun s => rate r (R (gamma s))) volume 0 (T : ℝ) ∧
      U y A - U y z = Iplus - Iminus ∧
      Real.exp (-U y z) * Real.exp (-Iplus) = Real.exp (-U y A) * Real.exp (-Iminus)

Exact module and namespace context

Proof roadmap

1Differentiate the actual target energy along a flow arc
Use the already proved actual ODE xdot=sqrt(eta)p and pdot=-(x-y)/sqrt(eta)-sqrt(eta)grad V(r). The chain rule gives sqrt(eta)<grad V(x),p>+<x-y,p>/sqrt(eta)-<p,x-y>/sqrt(eta)-sqrt(eta)<p,grad V(r)>. The quadratic-force terms cancel exactly. Since max(0,a)-max(0,-a)=a, this derivative equals lambda_r(x,p)-lambda_r(x,-p). Both rates are continuous along every harmonic arc, hence integrable on every finite real interval, and FTC gives the energy increment. The proof includes either orientation and equal interval endpoints.
2Telescope the finite energy grid
For each adjacent grid interval assume, only inside this private lemma, that f and g are integrable and their integral difference is u_(j+1)-u_j. The empty grid has zero integral and zero energy increment. Append one interval: oriented interval additivity gives both integrals on the enlarged interval, and the intermediate energy cancels. Induction therefore yields the endpoint energy difference. The public proof below supplies all these local facts from the actual trajectory; this helper introduces no public premise.
3Preserve target energy at every actual bounce
The actual reflection preserves position and momentum norm, including a zero normal. Thus V(x), the quadratic position term and the kinetic term are all unchanged by S_r. Reuse the actual flow initial identity and the continuity of the actual rate and flow. The energy grid consists of U evaluated at the post-bounce states, with the final entry U(A). These are literal actual states, not supplied witnesses.
4Identify each open arc of the actual clamped path
Prepend zero to the strictly ordered event times and append T to form a monotone grid. On the open jth interval, the real-time clamp equals s. Earlier history records have already occurred and later records are strictly in the future. Apply the verified actual finite-count path law to obtain gamma(s)=Phi_(s-a_j)(z_j). Only open-interval equality is used, so right-continuous values at event times are not confused with incoming states; a finite set of endpoints does not affect the Lebesgue integrals.
5Match the energies at the ends of all arcs
At an internal grid point, finite recursion defines the next post-bounce state as S_r applied to the outgoing arc endpoint. Bounce energy preservation identifies the next grid energy. On the last interval, the independently verified actual terminal formula A=Phi_(T-a_n)(z_n) supplies the same identity. This handles zero events and zero horizon without adding a positive event rate or a nonzero normal assumption.
6Integrate the actual trajectory and exponentiate the balance
Continuous arc rates transfer their integrability to the actual path through equality on open intervals. Compose the proved arc derivative with s-a_j, apply FTC on each interval and use the endpoint energy identities. The finite telescoping lemma now proves both whole-path integrabilities and U(A)-U(z)=Iplus-Iminus. Rearranging gives -U(z)-Iplus=-U(A)-Iminus; exponentiating and exp(a+b)=exp(a)exp(b) yields the Gibbs/survival equality. Iminus uses momentum reversal along the same path. Reverse-event matching and invariant-probability averaging remain separate.

Full assumptions and notation

All objects and hypotheses

Finite-dimensional real inner-product Borel E, including rank zero.
alpha,beta≥0; alpha>0; alpha≤beta; V is C2; alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v; eta>0; beta*eta≤1.
Every y,r,z,n≥0,T≥0 and strictly ordered prescribed event tuple; no positive rate or nonzero-normal condition.
Actual Gamma, clamped real-time extension, momentum reversal, positive-part rate and exact U definitions are fixed; both integral finiteness assertions are conclusions.

Mathematical proof

1. Differentiate the actual target energy along a flow arc

Use the already proved actual ODE xdot=sqrt(eta)p and pdot=-(x-y)/sqrt(eta)-sqrt(eta)grad V(r). The chain rule gives sqrt(eta)<grad V(x),p>+<x-y,p>/sqrt(eta)-<p,x-y>/sqrt(eta)-sqrt(eta)<p,grad V(r)>. The quadratic-force terms cancel exactly. Since max(0,a)-max(0,-a)=a, this derivative equals lambda_r(x,p)-lambda_r(x,-p). Both rates are continuous along every harmonic arc, hence integrable on every finite real interval, and FTC gives the energy increment. The proof includes either orientation and equal interval endpoints.

\[\frac{d}{ds}U_y(\Phi_s z)=\sqrt\eta\langle p_s,\nabla V(x_s)-\nabla V(r)\rangle=\lambda_r(\Phi_s z)-\lambda_r(R\Phi_s z).\]

Corresponding Lean step

private theorem actual_arc_energy
    {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) :
    let c : E → E → E := fun y r => y - η • gradient V r
    let Φ : E → E → ℝ → (E × E) → (E × E) := fun y r t z =>
      (c y r + Real.cos t • (z.1 - c y r) +
          (Real.sqrt η * Real.sin t) • z.2,
       (-Real.sin t / Real.sqrt η) • (z.1 - c y r) + Real.cos t • z.2)
    let R : E × E → E × E := fun z => (z.1, -z.2)
    let rate : E → E × E → ℝ := fun r z =>
      Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V r))
    let U : E → E × E → ℝ := fun y z =>
      V z.1 + ‖z.1 - y‖ ^ 2 / (2 * η) + ‖z.2‖ ^ 2 / 2
    ∀ y r : E, ∀ z : E × E,
      (∀ s : ℝ, HasDerivAt (fun t => U y (Φ y r t z))
        (rate r (Φ y r s z) - rate r (R (Φ y r s z))) s) ∧
      (∀ a b : ℝ,
        IntervalIntegrable (fun s => rate r (Φ y r s z)) volume a b ∧
        IntervalIntegrable (fun s => rate r (R (Φ y r s z))) volume a b ∧
        U y (Φ y r b z) - U y (Φ y r a z) =
          (∫ s in a..b, rate r (Φ y r s z)) -
          (∫ s in a..b, rate r (R (Φ y r s z)))) := by
  intro c Φ R rate U y r z
  letI : CompleteSpace E := FiniteDimensional.complete ℝ E
  have hf := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow.actual_harmonic_flow_laws
    hα hαβ hV hH hη hβη
  rcases hf with ⟨hc, _, _, _, _, ho, _⟩
  have hb := AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate.actual_bounce_rate_energy_laws
    hα hαβ hV hH hη hβη
  have hrate : Continuous (fun q : E × (E × E) => rate q.1 q.2) := hb.2.1
  have hphi : Continuous (fun t => Φ y r t z) :=
    hc.comp ((continuous_const (y := (y,r))).prodMk
      (continuous_id.prodMk (continuous_const (y := z))))
  have hp : Continuous (fun t => rate r (Φ y r t z)) :=
    hrate.comp (continuous_const.prodMk hphi)
  have hm : Continuous (fun t => rate r (R (Φ y r t z))) :=
    hrate.comp (continuous_const.prodMk (hphi.fst.prodMk hphi.snd.neg))
  have hdiff (q : E × E) : rate r q - rate r (R q) =
      Real.sqrt η * inner ℝ q.2 (gradient V q.1 - gradient V r) := by
    dsimp [rate, R]
    rw [inner_neg_left]
    by_cases h : 0 ≤ inner ℝ q.2 (gradient V q.1 - gradient V r)
    · rw [max_eq_right h, max_eq_left (neg_nonpos.mpr h)]
      ring
    · rw [max_eq_left (le_of_not_ge h), max_eq_right (neg_nonneg.mpr (le_of_not_ge h))]
      ring
  have hd (s : ℝ) : HasDerivAt (fun t => U y (Φ y r t z))
      (rate r (Φ y r s z) - rate r (R (Φ y r s z))) s := by
    obtain ⟨hx, hv⟩ := ho y r s z
    have hx' : HasDerivAt (fun t => (Φ y r t z).1) (Real.sqrt η • (Φ y r s z).2) s := hx
    have hv' : HasDerivAt (fun t => (Φ y r t z).2)
        (-(Real.sqrt η)⁻¹ • ((Φ y r s z).1 - y) - Real.sqrt η • gradient V r) s := hv
    have hVd := ((hV.differentiable (by norm_num)).differentiableAt.hasGradientAt.hasFDerivAt).comp_hasDerivAt s hx'
    have hd0 := (hVd.add ((hx'.sub_const y).norm_sq.div_const (2 * η))).add
      (hv'.norm_sq.div_const 2)
    apply hd0.congr_deriv
    rw [hdiff]
    simp only [InnerProductSpace.toDual_apply_apply, real_inner_smul_right, real_inner_smul_left,
      inner_sub_right, inner_sub_left, real_inner_comm]
    have hs : (Real.sqrt η) ^ 2 = η := Real.sq_sqrt hη.le
    have hs0 : Real.sqrt η ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hη)
    field_simp [hs0, hη.ne']
    simp only [hs]
    ring
  refine ⟨hd, ?_⟩
  intro a b
  have hi : IntervalIntegrable (fun s => rate r (Φ y r s z)) volume a b := hp.intervalIntegrable a b
  have hj : IntervalIntegrable (fun s => rate r (R (Φ y r s z))) volume a b := hm.intervalIntegrable a b
  refine ⟨hi, hj, ?_⟩
  rw [← intervalIntegral.integral_sub hi hj]
  exact (intervalIntegral.integral_eq_sub_of_hasDerivAt (fun s _ => hd s) (hi.sub hj)).symm