Actual PBPS: detailed balance after independent reference averaging
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility.actual_half_turn_reversible · theorem · Teaching coverage
Mathematical statement
Let E be a finite-dimensional real inner-product Borel space. Assume V is C2, 0<alpha≤beta, alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for every x,v, eta>0 and beta eta≤1. For each y let q_y be the normalized law proportional to exp(-V(x)-||x-y||^2/(2 eta)) dx. Draw the reference r from q_y, momentum p from the standard Gaussian and unit exponential clocks independently. Run the actual fixed-reference flow to time pi and return its position. The SAME global jointly measurable probability kernel H(y,x) given by this literal pushforward satisfies detailed balance with q_y for EVERY y. The existing raw covered-arc and fallback equations, parameterwise clock-AE interval coverage, local zero-time law and half-turn initialization outputs are retained. None of these construction, normalization, probability or integrability facts is a new hypothesis.
Lean statement · actual_half_turn_reversible
Let E be a finite-dimensional real inner-product Borel space. Assume V is C2, 0<alpha<=beta, alpha||v||^2<=D2V(x)[v,v]<=beta||v||^2 for every x,v, eta>0 and beta eta<=1. For each y let q_y be the normalized law proportional to exp(-V(x)-||x-y||^2/(2 eta)) dx. Draw the reference r from q_y, momentum p from the standard Gaussian and unit exponential clocks independently. Run the actual fixed-reference flow to time pi and return its position. The SAME global jointly measurable probability kernel H(y,x) given by this literal pushforward satisfies detailed balance with q_y for EVERY y. The existing raw covered-arc and fallback equations, parameterwise clock-AE interval coverage, local zero-time law and half-turn initialization outputs are retained. None of these construction, normalization, probability or integrability facts is a new hypothesis.
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 actual_half_turn_reversible
{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_half_turn_reversibility_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_half_turn_reversibility_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.
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.
private def actual_half_turn_reversibility_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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun sample k => Real.toNNReal (sample k)
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 rate : E → (E × E) → ℝ := fun xRef z =>
Real.sqrt η * max 0 (inner ℝ z.2 (gradient V z.1 - gradient V xRef))
let Λ : E → E → (E × E) → ℝ≥0 → ℝ := fun y xRef z t =>
∫ s in (0 : ℝ)..(t : ℝ), rate xRef (Φ y xRef s z)
let τ : E → E → (E × E) → ℝ≥0 → WithTop ℝ≥0 := fun y xRef z e =>
MeasureTheory.hittingAfter
(fun t : ℝ≥0 => fun a : (E × E) × (E × E) × ℝ≥0 =>
Λ a.1.1 a.1.2 a.2.1 t - (a.2.2 : ℝ))
(Set.Ici (0 : ℝ)) 0 ((y, xRef), z, e)
let next : E → E → ℝ≥0 → ((ℝ≥0 × (E × E)) ⊕ Unit) →
((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef e r =>
match r with
| Sum.inr _ => Sum.inr ()
| Sum.inl a =>
if τ y xRef a.2 e = ⊤ then Sum.inr () else
Sum.inl (a.1 + (τ y xRef a.2 e).untopD 0,
S xRef (Φ y xRef (((τ y xRef a.2 e).untopD 0 : ℝ≥0) : ℝ) a.2))
let record : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ →
((ℝ≥0 × (E × E)) ⊕ Unit) := fun y xRef z₀ e n =>
Nat.rec (Sum.inl (0, z₀)) (fun k r => next y xRef (e k) r) n
let eventTime : E → E → (E × E) → (ℕ → ℝ≥0) → ℕ → WithTop ℝ≥0 :=
fun y xRef z₀ e n => (record y xRef z₀ e n).elim
(fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
let q : E → Measure E := fun y =>
(volume : Measure E).tilted (fun x => -V x - ‖x - y‖ ^ 2 / (2 * η))
let γ : Measure E := stdGaussian E
let M : E → Measure ((E × E) × (ℕ → ℝ)) := fun y => ((q y).prod γ).prod P
let tπ : ℝ≥0 := ⟨Real.pi, Real.pi_pos.le⟩
∃ Z : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → (E × E),
Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 × (ℕ → ℝ) =>
Z a.1.1.1 a.1.1.2 a.1.2 a.2.1 a.2.2) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
∀ n : ℕ, ∀ a : ℝ≥0 × (E × E),
eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) →
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) →
record y xRef z₀ (ε sample) n = Sum.inl a →
Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ sample : ℕ → ℝ, ∀ t : ℝ≥0,
(¬ ∃ n : ℕ, eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1)) →
Z y xRef z₀ t sample = z₀) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ sample ∂P,
(∀ t : ℝ≥0, ∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
eventTime y xRef z₀ (ε sample) n ≤ (t : WithTop ℝ≥0) ∧
(t : WithTop ℝ≥0) < eventTime y xRef z₀ (ε sample) (n + 1) ∧
record y xRef z₀ (ε sample) n = Sum.inl a ∧ a.1 ≤ t ∧
((t - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y xRef a.2 (ε sample n) ∧
Z y xRef z₀ t sample = Φ y xRef ((t - a.1 : ℝ≥0) : ℝ) a.2) ∧
Z y xRef z₀ 0 sample = z₀) ∧
∃ R : Kernel E E, IsMarkovKernel R ∧ (∀ y : E, R y = q y) ∧
∃ H : Kernel (E × E) E, IsMarkovKernel H ∧
(∀ y : E, (H.comap (fun x : E => (y, x)) (by fun_prop)).IsReversible (q y)) ∧
(∀ y x : E, H (y, x) = Measure.map
(fun w : (E × E) × (ℕ → ℝ) => (Z y w.1.1 (x, w.1.2) tπ w.2).1)
(M y)) ∧
(∀ y x : E, Measure.map
(fun w : (E × E) × (ℕ → ℝ) => Z y w.1.1 (x, w.1.2) 0 w.2)
(M y) = (Measure.dirac x).prod γ) ∧
(∀ y x : E, ∀ᵐ w ∂M y,
Z y w.1.1 (x, w.1.2) 0 w.2 = (x, w.1.2) ∧
∃ n : ℕ, ∃ a : ℝ≥0 × (E × E),
eventTime y w.1.1 (x, w.1.2) (ε w.2) n ≤ (tπ : WithTop ℝ≥0) ∧
(tπ : WithTop ℝ≥0) < eventTime y w.1.1 (x, w.1.2) (ε w.2) (n + 1) ∧
record y w.1.1 (x, w.1.2) (ε w.2) n = Sum.inl a ∧ a.1 ≤ tπ ∧
((tπ - a.1 : ℝ≥0) : WithTop ℝ≥0) < τ y w.1.1 a.2 (ε w.2 n) ∧
Z y w.1.1 (x, w.1.2) tπ w.2 = Φ y w.1.1 ((tπ - a.1 : ℝ≥0) : ℝ) a.2)Proof roadmap
- 1Identify the actual path, including exceptional raw clocks
The kernel construction and the signed-duality construction prescribe the same recursion. On a covered interval their live record gives the same harmonic arc; a dead record cannot bracket a finite time. When no interval covers the time, both use the existing initial-state fallback. The two global path witnesses therefore agree pointwise, before taking any expectation.
- 2Keep the literal independent-reference kernel
The existing reference kernel identifies q_y as a probability law for every y. Gaussian momentum and the clock product are also probability laws. Joint measurability of Z makes the returned-position map measurable in input, reference, momentum and clocks. Restrict the joint kernel to a fixed y; its fiber law is exactly the displayed pushforward, not an arbitrary reversible replacement.
- 3Remove both momentum flips from bounded position tests
Lift measurable functions f,g bounded in absolute value by1 to phase space using the position projection. The momentum flip leaves both lifts unchanged. Actual bounded signed phase duality therefore gives a symmetric pairing for each fixed reference r. The two written forms of the Gibbs potential are identified by real algebra.
- 4Average the reference only after proving signed Fubini conditions
Joint measurability gives a measurable clock expectation. Probability and |g|≤1 imply |E_w g|≤1; hence |f E_w g|≤1. These products are integrable under q_y times q_y times gamma, and the raw clock integrands are integrable under the corresponding product with P. Signed Fubini can now exchange input x and independent reference r. Integrating the fixed-reference symmetry yields symmetry of the actual kernel pairing.
- 5Convert measurable indicators to exact rectangle detailed balance
Choose f=1_A and g=1_B for measurable A,B. Each kernel fiber has finite mass one. Mathlib identifies the integral of an indicator with its real measure; nonnegative finite integration identifies its ofReal value with the ENNReal rectangle flux. Symmetry therefore gives the defining identity of Kernel.IsReversible on all measurable rectangles.
Full assumptions and notation
All objects and hypotheses
- Exactly the six analytic assumptions in the statement; finite real Hilbert Borel E includes dimension zero.
- Literal flow: c=y-eta grad V(r); x_t=c+cos(t)(x-c)+sqrt(eta)sin(t)p, p_t=-sin(t)(x-c)/sqrt(eta)+cos(t)p. Bounce reflects in grad V(x)-grad V(r), with identity at zero normal; rate sqrt(eta)max(0,<p,grad V(x)-grad V(r)>).
- Independent unit exponential thresholds, integrated-hazard hitting times and the existing raw initial-state fallback define Z. The full literal recursion and retained outputs are available in the folded proposition.
- Normalization, probability, joint measurability, integrability and detailed balance are derived, not extra source binders. AE initialization/coverage is parameterwise; no common null set uniform in every parameter is asserted.
Mathematical proof
1. Identify the actual path, including exceptional raw clocks
The kernel construction and the signed-duality construction prescribe the same recursion. On a covered interval their live record gives the same harmonic arc; a dead record cannot bracket a finite time. When no interval covers the time, both use the existing initial-state fallback. The two global path witnesses therefore agree pointwise, before taking any expectation.
Corresponding Lean step
obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hHlaw, hH0, hHgood⟩ :=
IdealHalfTurnKernel.ideal_half_turn_returned_position_kernel hα hαβ hV hH hη hβη
refine ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, ?_, hHlaw, hH0, hHgood⟩
obtain ⟨Zb, _hZbm, hZba, hZbf, _hZb0, hD⟩ :=
ActualBoundedGibbsDuality.actual_bounded_gibbs_duality hα hαβ hV hH hη hβη
have hZd : Zb = Z := by
funext y r z t w
by_cases hw : ∃ n : ℕ, eventTime y r z (ε w) n ≤ (t : WithTop ℝ≥0) ∧
(t : WithTop ℝ≥0) < eventTime y r z (ε w) (n + 1)
· obtain ⟨n, hn, hn'⟩ := hw
cases hr : record y r z (ε w) n with
| inl a =>
exact (hZba y r z w t n a (by exact ⟨hn, hn'⟩) hr).trans
(hZa y r z w t n a hn hn' hr).symm
| inr a =>
have hnot : ¬ (⊤ : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) :=
WithTop.not_top_le_coe t
apply False.elim
apply hnot
simpa only [eventTime, hr, Sum.elim_inr] using hn
· exact (hZbf y r z w t hw).trans (hZf y r z w t hw).symm
subst Zb
This is equality for all raw inputs, not an informal identification of laws or a common null event over all parameters.
2. Keep the literal independent-reference kernel
The existing reference kernel identifies q_y as a probability law for every y. Gaussian momentum and the clock product are also probability laws. Joint measurability of Z makes the returned-position map measurable in input, reference, momentum and clocks. Restrict the joint kernel to a fixed y; its fiber law is exactly the displayed pushforward, not an arbitrary reversible replacement.
Corresponding Lean step
letI : IsMarkovKernel R := hR
letI : IsMarkovKernel H := hHK
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))
intro y
letI : IsProbabilityMeasure (q y) := by
have he : R y = q y := hRq y
rw [← he]
infer_instance
let κ : Kernel E E := H.comap (fun x : E => (y, x)) (by fun_prop)
let F : E → E → E → (ℕ → ℝ) → E := fun r x p w => (Z y r (x, p) tπ w).1
have hFM : Measurable (fun a : ((E × E) × E) × (ℕ → ℝ) =>
F a.1.1.2 a.1.1.1 a.1.2 a.2) :=
(hZM.comp (((measurable_const.prodMk measurable_fst.fst.snd).prodMk
(measurable_fst.fst.fst.prodMk measurable_fst.snd)).prodMk
(measurable_const.prodMk measurable_snd))).fst
have hKl (x : E) : κ x = Measure.map
(fun a : (E × E) × (ℕ → ℝ) => F a.1.1 x a.1.2 a.2)
(((q y).prod γ).prod P) := hHlaw y x
apply reversible_of_reference_average (q y) γ P F hFM κ hKl
The reference distribution q_y does not depend on the current input x. Global warm-start initialization is not supplied or proved here.
3. Remove both momentum flips from bounded position tests
Lift measurable functions f,g bounded in absolute value by1 to phase space using the position projection. The momentum flip leaves both lifts unchanged. Actual bounded signed phase duality therefore gives a symmetric pairing for each fixed reference r. The two written forms of the Gibbs potential are identified by real algebra.
Corresponding Lean step
intro r f g hf hg hfb hgb
have hbd := (hD y r tπ).2 (fun z : E × E => f z.1)
(fun z : E × E => g z.1) 1 1 (hf.comp measurable_fst)
(hg.comp measurable_fst) zero_le_one zero_le_one
(fun z => hfb z.1) (fun z => hgb z.1)
have hflux := hbd.2.2
have hqeq : (volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η))) = q y := by
apply congrArg (fun U : E → ℝ => (volume : Measure E).tilted U)
funext x
ring
change (∫ z : E × E, f z.1 * (∫ w, g (Z y r z tπ w).1 ∂P)
∂((volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) =
(∫ z : E × E, g z.1 * (∫ w, f (Z y r z tπ w).1 ∂P)
∂((volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) at hflux
rw [hqeq] at hflux
exact hflux
This is the bounded-test adapter to the source operator proof, not a claim that a temporal semigroup has been constructed.
4. Average the reference only after proving signed Fubini conditions
Joint measurability gives a measurable clock expectation. Probability and |g|≤1 imply |E_w g|≤1; hence |f E_w g|≤1. These products are integrable under q_y times q_y times gamma, and the raw clock integrands are integrable under the corresponding product with P. Signed Fubini can now exchange input x and independent reference r. Integrating the fixed-reference symmetry yields symmetry of the actual kernel pairing.
Corresponding Lean step
private theorem pairing_eq_reference_average
{X Y W : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W]
(q : Measure X) (γ : Measure Y) (P : Measure W)
[IsProbabilityMeasure q] [IsProbabilityMeasure γ] [IsProbabilityMeasure P]
(F : X → X → Y → W → X)
(hF : Measurable (fun a : ((X × X) × Y) × W =>
F a.1.1.2 a.1.1.1 a.1.2 a.2))
(κ : Kernel X X)
(hlaw : ∀ x, κ x = Measure.map
(fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) ((q.prod γ).prod P))
(f g : X → ℝ) (hf : Measurable f) (hg : Measurable g)
(hfb : ∀ x, |f x| ≤ 1) (hgb : ∀ x, |g x| ≤ 1) :
(∫ x, f x * (∫ z, g z ∂κ x) ∂q) =
∫ r, (∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P)
∂q.prod γ) ∂q := by
let op : X → X → Y → ℝ := fun x r p => ∫ w, g (F r x p w) ∂P
have hopm : Measurable (fun a : (X × X) × Y => op a.1.1 a.1.2 a.2) :=
(hg.comp hF).stronglyMeasurable.integral_prod_right'.measurable
have hopb (x r : X) (p : Y) : |op x r p| ≤ 1 := by
have hh := norm_integral_le_of_norm_le_const (μ := P)
(f := fun w => g (F r x p w))
(Eventually.of_forall fun w => by
simpa only [Real.norm_eq_abs] using hgb (F r x p w))
simpa [op] using hh
have hdb (x r : X) (p : Y) : |f x * op x r p| ≤ 1 := by
calc
|f x * op x r p| = |f x| * |op x r p| := abs_mul _ _
_ ≤ 1 * 1 := mul_le_mul (hfb x) (hopb x r p) (abs_nonneg _) zero_le_one
_ = 1 := mul_one 1
have hdm : Measurable (fun a : (X × X) × Y =>
f a.1.1 * op a.1.1 a.1.2 a.2) := (hf.comp measurable_fst.fst).mul hopm
have hdi : Integrable (fun a : (X × X) × Y =>
f a.1.1 * op a.1.1 a.1.2 a.2) ((q.prod q).prod γ) :=
Integrable.of_bound hdm.aestronglyMeasurable 1
(Eventually.of_forall fun a => by
simpa only [Real.norm_eq_abs] using hdb a.1.1 a.1.2 a.2)
have hinner (x : X) : (∫ z, g z ∂κ x) = ∫ r, ∫ p, op x r p ∂γ ∂q := by
have hfx : Measurable (fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) :=
hF.comp (((measurable_const.prodMk measurable_fst.fst).prodMk
measurable_fst.snd).prodMk measurable_snd)
have hi : Integrable (fun a : (X × Y) × W => g (F a.1.1 x a.1.2 a.2))
((q.prod γ).prod P) :=
Integrable.of_bound (hg.comp hfx).aestronglyMeasurable 1
(Eventually.of_forall fun a => by
simpa only [Real.norm_eq_abs] using hgb (F a.1.1 x a.1.2 a.2))
rw [hlaw x, integral_map hfx.aemeasurable hg.aestronglyMeasurable,
integral_prod _ hi]
exact integral_prod _ hi.integral_prod_left
calc
(∫ x, f x * (∫ z, g z ∂κ x) ∂q) =
∫ x, ∫ r, ∫ p, f x * op x r p ∂γ ∂q ∂q := by
simp_rw [hinner, ← integral_const_mul]
_ = ∫ r, ∫ x, ∫ p, f x * op x r p ∂γ ∂q ∂q :=
integral_integral_swap hdi.integral_prod_left
_ = ∫ r, (∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P)
∂q.prod γ) ∂q := by
apply integral_congr_ae
exact Eventually.of_forall fun r => by
have hm : Measurable (fun z : X × Y => f z.1 * op z.1 r z.2) :=
hdm.comp ((measurable_fst.prodMk measurable_const).prodMk measurable_snd)
have hi : Integrable (fun z : X × Y => f z.1 * op z.1 r z.2)
(q.prod γ) :=
Integrable.of_bound hm.aestronglyMeasurable 1
(Eventually.of_forall fun z => by
simpa only [Real.norm_eq_abs] using hdb z.1 r z.2)
exact (integral_prod _ hi).symm
/-- Combine the exact raw returned law with fixed-reference bounded position duality. -/
private theorem reversible_of_reference_average
{X Y W : Type*} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace W]
(q : Measure X) (γ : Measure Y) (P : Measure W)
[IsProbabilityMeasure q] [IsProbabilityMeasure γ] [IsProbabilityMeasure P]
(F : X → X → Y → W → X)
(hF : Measurable (fun a : ((X × X) × Y) × W =>
F a.1.1.2 a.1.1.1 a.1.2 a.2))
(κ : Kernel X X) [IsMarkovKernel κ]
(hlaw : ∀ x, κ x = Measure.map
(fun a : (X × Y) × W => F a.1.1 x a.1.2 a.2) ((q.prod γ).prod P))
(hdual : ∀ r : X, ∀ f g : X → ℝ, Measurable f → Measurable g →
(∀ x, |f x| ≤ 1) → (∀ x, |g x| ≤ 1) →
(∫ z : X × Y, f z.1 * (∫ w, g (F r z.1 z.2 w) ∂P) ∂q.prod γ) =
∫ z : X × Y, g z.1 * (∫ w, f (F r z.1 z.2 w) ∂P) ∂q.prod γ) :
κ.IsReversible q := by
apply reversible_of_bounded_pairing q κ
intro f g hf hg hfb hgb
rw [pairing_eq_reference_average q γ P F hF κ hlaw f g hf hg hfb hgb,
pairing_eq_reference_average q γ P F hF κ hlaw g f hg hf hgb hfb]
exact integral_congr_ae (Eventually.of_forall fun r => hdual r f g hf hg hfb hgb)
No unbounded reference-energy moment, integration over y, or transfer of an unbounded cost by TV proximity is used.
5. Convert measurable indicators to exact rectangle detailed balance
Choose f=1_A and g=1_B for measurable A,B. Each kernel fiber has finite mass one. Mathlib identifies the integral of an indicator with its real measure; nonnegative finite integration identifies its ofReal value with the ENNReal rectangle flux. Symmetry therefore gives the defining identity of Kernel.IsReversible on all measurable rectangles.
Corresponding Lean step
private theorem flux_ofReal
{X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
(κ : Kernel X X) [IsMarkovKernel κ]
{A B : Set X} (hA : MeasurableSet A) (hB : MeasurableSet B) :
ENNReal.ofReal (∫ x, A.indicator (fun _ => (1 : ℝ)) x *
(∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) ∂μ) =
∫⁻ x in A, κ x B ∂μ := by
have hi : Integrable (fun x => (κ x).real B) (μ.restrict A) := by
apply Integrable.of_bound
(κ.measurable_coe hB).ennreal_toReal.aestronglyMeasurable 1
exact Eventually.of_forall fun x => by
simpa only [Real.norm_eq_abs, abs_of_nonneg ENNReal.toReal_nonneg,
Measure.real] using
(measureReal_le_one (μ := κ x) (s := B))
have hreal : (∫ x, A.indicator (fun _ => (1 : ℝ)) x *
(∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) ∂μ) =
∫ x in A, (κ x).real B ∂μ := by
have hIB (x : X) : (∫ z, B.indicator (fun _ => (1 : ℝ)) z ∂κ x) =
(κ x).real B := integral_indicator_one hB
simp_rw [hIB]
rw [← integral_indicator hA]
congr 1
funext x
by_cases hx : x ∈ A <;> simp [hx]
rw [hreal, ofReal_integral_eq_lintegral_ofReal hi
(Eventually.of_forall fun _ => measureReal_nonneg)]
apply lintegral_congr_ae
exact Eventually.of_forall fun x => ENNReal.ofReal_toReal (measure_ne_top (κ x) B)
/-- Test symmetry on measurable indicators; no countability/singleton criterion. -/
private theorem reversible_of_bounded_pairing
{X : Type*} [MeasurableSpace X] (μ : Measure X) [IsFiniteMeasure μ]
(κ : Kernel X X) [IsMarkovKernel κ]
(hsym : ∀ f g : X → ℝ, Measurable f → Measurable g →
(∀ x, |f x| ≤ 1) → (∀ x, |g x| ≤ 1) →
(∫ x, f x * (∫ z, g z ∂κ x) ∂μ) =
∫ x, g x * (∫ z, f z ∂κ x) ∂μ) : κ.IsReversible μ := by
intro A B hA hB
rw [← flux_ofReal μ κ hA hB, ← flux_ofReal μ κ hB hA]
congr 1
apply hsym _ _ (measurable_const.indicator hA) (measurable_const.indicator hB)
· intro x
by_cases hx : x ∈ A <;> simp [hx]
· intro x
by_cases hx : x ∈ B <;> simp [hx]
The criterion works on atomless E. The countable-state singleton-balance lemma is inapplicable. The private adapters below are not additional Registry leaves.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_half_turn_reversible
Same literal Z -> exact probability kernel -> position lifts absorb flips -> bounded signed reference Fubini -> measurable-rectangle detailed balance.
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 actual_half_turn_reversible
{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_half_turn_reversibility_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_half_turn_reversibility_statement
intro P ε c Φ S rate Λ τ next record eventTime q γ M tπ
obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hHlaw, hH0, hHgood⟩ :=
IdealHalfTurnKernel.ideal_half_turn_returned_position_kernel hα hαβ hV hH hη hβη
refine ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, ?_, hHlaw, hH0, hHgood⟩
obtain ⟨Zb, _hZbm, hZba, hZbf, _hZb0, hD⟩ :=
ActualBoundedGibbsDuality.actual_bounded_gibbs_duality hα hαβ hV hH hη hβη
have hZd : Zb = Z := by
funext y r z t w
by_cases hw : ∃ n : ℕ, eventTime y r z (ε w) n ≤ (t : WithTop ℝ≥0) ∧
(t : WithTop ℝ≥0) < eventTime y r z (ε w) (n + 1)
· obtain ⟨n, hn, hn'⟩ := hw
cases hr : record y r z (ε w) n with
| inl a =>
exact (hZba y r z w t n a (by exact ⟨hn, hn'⟩) hr).trans
(hZa y r z w t n a hn hn' hr).symm
| inr a =>
have hnot : ¬ (⊤ : WithTop ℝ≥0) ≤ (t : WithTop ℝ≥0) :=
WithTop.not_top_le_coe t
apply False.elim
apply hnot
simpa only [eventTime, hr, Sum.elim_inr] using hn
· exact (hZbf y r z w t hw).trans (hZf y r z w t hw).symm
subst Zb
letI : IsMarkovKernel R := hR
letI : IsMarkovKernel H := hHK
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
letI : IsProbabilityMeasure γ := inferInstanceAs (IsProbabilityMeasure (stdGaussian E))
intro y
letI : IsProbabilityMeasure (q y) := by
have he : R y = q y := hRq y
rw [← he]
infer_instance
let κ : Kernel E E := H.comap (fun x : E => (y, x)) (by fun_prop)
let F : E → E → E → (ℕ → ℝ) → E := fun r x p w => (Z y r (x, p) tπ w).1
have hFM : Measurable (fun a : ((E × E) × E) × (ℕ → ℝ) =>
F a.1.1.2 a.1.1.1 a.1.2 a.2) :=
(hZM.comp (((measurable_const.prodMk measurable_fst.fst.snd).prodMk
(measurable_fst.fst.fst.prodMk measurable_fst.snd)).prodMk
(measurable_const.prodMk measurable_snd))).fst
have hKl (x : E) : κ x = Measure.map
(fun a : (E × E) × (ℕ → ℝ) => F a.1.1 x a.1.2 a.2)
(((q y).prod γ).prod P) := hHlaw y x
apply reversible_of_reference_average (q y) γ P F hFM κ hKl
intro r f g hf hg hfb hgb
have hbd := (hD y r tπ).2 (fun z : E × E => f z.1)
(fun z : E × E => g z.1) 1 1 (hf.comp measurable_fst)
(hg.comp measurable_fst) zero_le_one zero_le_one
(fun z => hfb z.1) (fun z => hgb z.1)
have hflux := hbd.2.2
have hqeq : (volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η))) = q y := by
apply congrArg (fun U : E → ℝ => (volume : Measure E).tilted U)
funext x
ring
change (∫ z : E × E, f z.1 * (∫ w, g (Z y r z tπ w).1 ∂P)
∂((volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) =
(∫ z : E × E, g z.1 * (∫ w, f (Z y r z tπ w).1 ∂P)
∂((volume : Measure E).tilted
(fun x => -(V x + ‖x - y‖ ^ 2 / (2 * η)))).prod γ) at hflux
rw [hqeq] at hflux
exact hflux
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibilityScope and omitted-condition boundaries
- Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel.ideal_half_turn_returned_position_kernelAutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality.actual_bounded_gibbs_dualityAutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
Mathlib API called (external library)
- MeasureTheory.Integrable.of_bound
- MeasureTheory.integral_indicator_one
- MeasureTheory.ofReal_integral_eq_lintegral_ofReal
- MeasureTheory.integral_map
- MeasureTheory.integral_prod
- MeasureTheory.integral_integral_swap
- MeasureTheory.StronglyMeasurable.integral_prod_right
- ProbabilityTheory.Kernel.IsReversible
Mathematical sources
- Proposition3.2, A.1 bounded duality819-820 and A.2 proof832-853 — Conditional detailed balance for the same actual returned-position kernel only. No temporal restart/semigroup, augmented all-L2 operator, hypocoercive rate, capped implementation, error/cost, global warm start, composition or complete paper.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.