Actual PBPS: one probability kernel and its real-L2 operator
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualKernelL2Realization.actual_kernel_l2_realization · theorem · Teaching coverage
Mathematical statement
Assume the six displayed analytic hypotheses. Put V_y(x)=V(x)+||x-y||^2/(2 eta), pi_y=volume.tilted(-V_y), gamma=stdGaussian(E), nu_y=pi_y times gamma and P=Exp(1)^N. Use the literal fixed-reference PBPS flow with center c=y-eta grad V(r), position c+cos(t)(x-c)+sqrt(eta)sin(t)p and momentum -sin(t)(x-c)/sqrt(eta)+cos(t)p. The bounce reflects momentum in grad V(x)-grad V(r), with the identity for a zero normal; its rate is sqrt(eta) max(0,<p,grad V(x)-grad V(r)>). Independent exponential thresholds determine integrated-hazard waiting times, post-bounce records and between-jump interpolation. The existing raw initial-state fallback outside covered intervals is retained, not introduced anew. There is one global jointly measurable actual process Z with the every-raw-input arc/fallback rules and parameterwise clock-AE zero-time initialization. Its endpoint sends nu_y times P to nu_y; bounded signed flip duality and jointly measurable bounded-Borel clock expectations retain their integrability and uniform bounds. A single joint-index probability kernel Kphase has every fiber exactly map(Z(y,r,z,t))P. For every fixed y,r,t the state-kernel z → Kphase(((y,r),z),t) preserves nu_y as an exact measure equality. For each y,r the SAME continuous real-linear L2(nu_y) family A_t satisfies A_0=I, ||A_t||≤1 and A_t f → f at zero for every f. Every canonical L2 representative f-sharp is integrable on almost every kernel fiber, and (A_t f)-sharp(z)=integral f-sharp(z') Kphase(((y,r),z),t)(dz') for nu_y-almost every z. A_t preserves AE nonnegativity and fixes every real constant class, whose L2 membership is produced. All earlier arbitrary-MemLp clock representation and square-integral bounds remain. The momentum flip J is an involutive isometry and A_t*=J A_t J. The position pullback B is isometric; M=B* equals Gaussian integration for arbitrary MemLp representatives, MB=I, JB=B, MJ=M. Kpos_t=M A_t B remains a self-adjoint contraction with Kpos_0=I and its Gaussian-outer/clock-inner representative, including both nested AE integrability obligations. This identifies a phase probability kernel and its existing operator, not a restart law or a position probability kernel.
Lean statement · actual_kernel_l2_realization
Assume the six displayed analytic hypotheses. Put V_y(x)=V(x)+||x-y||^2/(2 eta), pi_y=volume.tilted(-V_y), gamma=stdGaussian(E), nu_y=pi_y times gamma and P=Exp(1)^N. Use the literal fixed-reference PBPS flow with center c=y-eta grad V(r), position c+cos(t)(x-c)+sqrt(eta)sin(t)p and momentum -sin(t)(x-c)/sqrt(eta)+cos(t)p. The bounce reflects momentum in grad V(x)-grad V(r), with the identity for a zero normal; its rate is sqrt(eta) max(0,<p,grad V(x)-grad V(r)>). Independent exponential thresholds determine integrated-hazard waiting times, post-bounce records and between-jump interpolation. The existing raw initial-state fallback outside covered intervals is retained, not introduced anew. There is one global jointly measurable actual process Z with the every-raw-input arc/fallback rules and parameterwise clock-AE zero-time initialization. Its endpoint sends nu_y times P to nu_y; bounded signed flip duality and jointly measurable bounded-Borel clock expectations retain their integrability and uniform bounds. A single joint-index probability kernel Kphase has every fiber exactly map(Z(y,r,z,t))P. For every fixed y,r,t the state-kernel z -> Kphase(((y,r),z),t) preserves nu_y as an exact measure equality. For each y,r the SAME continuous real-linear L2(nu_y) family A_t satisfies A_0=I, ||A_t||<=1 and A_t f -> f at zero for every f. Every canonical L2 representative f-sharp is integrable on almost every kernel fiber, and (A_t f)-sharp(z)=integral f-sharp(z') Kphase(((y,r),z),t)(dz') for nu_y-almost every z. A_t preserves AE nonnegativity and fixes every real constant class, whose L2 membership is produced. All earlier arbitrary-MemLp clock representation and square-integral bounds remain. The momentum flip J is an involutive isometry and A_t*=J A_t J. The position pullback B is isometric; M=B* equals Gaussian integration for arbitrary MemLp representatives, MB=I, JB=B, MJ=M. Kpos_t=M A_t B remains a self-adjoint contraction with Kpos_0=I and its Gaussian-outer/clock-inner representative, including both nested AE integrability obligations. This identifies a phase probability kernel and its existing operator, not a restart law or a position probability kernel.
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_kernel_l2_realization
{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_kernel_l2_realization_statement hα hαβ hV hH hη hβηFull Lean proposition (definition) · actual_kernel_l2_realization_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_kernel_l2_realization_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 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 P : Measure (ℕ → ℝ) := Measure.infinitePi (fun _ : ℕ => expMeasure (1 : ℝ))
let ε : (ℕ → ℝ) → ℕ → ℝ≥0 := fun w k => Real.toNNReal (w k)
let history : E → E → (E × E) → (n : ℕ) → (ℕ → ℝ) →
(Fin (n + 1) → ((ℝ≥0 × (E × E)) ⊕ Unit)) :=
fun y xRef z₀ n w j => record y xRef z₀ (ε w) j.val
let Rec := (ℝ≥0 × (E × E)) ⊕ Unit
let Hist : ℕ → Type _ := fun n => Fin (n + 1) → Rec
let readTime : Rec → ℝ := fun r => match r with
| Sum.inl q => (q.1 : ℝ)
| Sum.inr _ => 0
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 qReal : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
Prefix n T → ℝ := fun y xRef z₀ n T t =>
∏ i : Fin n,
rate xRef (Φ y xRef (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)
(zAt y xRef z₀ n T t i.castSucc)) *
Real.exp (-Λ y xRef (zAt y xRef z₀ n T t i.castSucc)
(Real.toNNReal (t.val i - (Fin.cons (0 : ℝ) (t.val : Fin n → ℝ) : Fin (n + 1) → ℝ) i.castSucc)))
let q : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) →
Prefix n T → ℝ≥0∞ := fun y xRef z₀ n T t =>
ENNReal.ofReal (qReal y xRef z₀ n T t)
let A : (n : ℕ) → ℝ≥0 → Set (Hist n) := fun n T =>
{h | (∀ j, ∃ a : ℝ≥0 × (E × E), h j = Sum.inl a) ∧
StrictMono (fun j => readTime (h j)) ∧
∀ i : Fin n, readTime (h i.succ) < (T : ℝ)}
let eventTime : E → E → (E × E) → (ℕ → ℝ) → ℕ → WithTop ℝ≥0 :=
fun y xRef z₀ w j => (record y xRef z₀ (ε w) j).elim
(fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤)
let I : E → E → (E × E) → ℝ≥0 → ℕ → Set (ℕ → ℝ) :=
fun y xRef z₀ T n => {w | eventTime y xRef z₀ w n ≤ (T : WithTop ℝ≥0) ∧
(T : WithTop ℝ≥0) < eventTime y xRef z₀ w (n + 1)}
let N : E → E → (E × E) → ℝ≥0 → (ℕ → ℝ) → ℕ := fun y xRef z₀ T w =>
if h : ∃ n, w ∈ I y xRef z₀ T n then Nat.find h else 0
let liveTime : Rec → ℝ≥0 := fun r => r.elim Prod.fst (fun _ => 0)
let d : (n : ℕ) → ℝ≥0 → Hist n → ℝ≥0 :=
fun n T h => T - liveTime (h ⟨n, Nat.lt_succ_self n⟩)
let survival : E → E → Rec → ℝ≥0 → ℝ → Prop :=
fun y xRef r u e => r.elim
(fun a => (u : WithTop ℝ≥0) < τ y xRef a.2 (Real.toNNReal e)) (fun _ => False)
let weight : E → E → Rec → ℝ≥0 → ℝ≥0∞ :=
fun y xRef r u => r.elim
(fun a => ENNReal.ofReal (Real.exp (-Λ y xRef a.2 u))) (fun _ => 0)
let C : E → E → (E × E) → (n : ℕ) → ℝ≥0 → Set (ℕ → ℝ) :=
fun y xRef z₀ n T => {w | history y xRef z₀ n w ∈ A n T ∧
survival y xRef (record y xRef z₀ (ε w) n) (d n T (history y xRef z₀ n w)) (w n)}
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 ρ : E → E → (E × E) → (n : ℕ) → (T : ℝ≥0) → Prefix n T → ℝ≥0∞ :=
fun y xRef z₀ n T t => q y xRef z₀ n T t *
weight y xRef ((K y xRef z₀ n T t) ⟨n, Nat.lt_succ_self n⟩)
(d n T (K y xRef z₀ n T t))
let R : E × E → E × E := fun z => (z.1, -z.2)
let Vy : E → E → ℝ := fun y x => V x + ‖x - y‖ ^ 2 / (2 * η)
let nu : E → Measure (E × E) := fun y =>
((volume : Measure E).tilted (fun x => -Vy y x)).prod
(ProbabilityTheory.stdGaussian E)
∃ 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, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
∀ n : ℕ, ∀ a : ℝ≥0 × (E × E), w ∈ I y xRef z₀ s n →
record y xRef z₀ (ε w) n = Sum.inl a →
Z y xRef z₀ s w = Φ y xRef ((s - a.1 : ℝ≥0) : ℝ) a.2) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ w : ℕ → ℝ, ∀ s : ℝ≥0,
(¬ ∃ n, w ∈ I y xRef z₀ s n) → Z y xRef z₀ s w = z₀) ∧
(∀ y xRef : E, ∀ z₀ : E × E, ∀ᵐ w ∂P, Z y xRef z₀ 0 w = z₀) ∧
(∀ y xRef : E, ∀ T : ℝ≥0,
let op : ((E × E) → ℝ) → (E × E) → ℝ :=
fun G z => ∫ w, G (Z y xRef z T w) ∂P
let endpoint : (E × E) × (ℕ → ℝ) → E × E :=
fun a => Z y xRef a.1 T a.2
MeasurePreserving endpoint ((nu y).prod P) (nu y) ∧
∀ F G : (E × E) → ℝ, ∀ C_F C_G : ℝ,
Measurable F → Measurable G → 0 ≤ C_F → 0 ≤ C_G →
(∀ z, |F z| ≤ C_F) → (∀ z, |G z| ≤ C_G) →
Integrable (fun z => F z * op G z) (nu y) ∧
Integrable (fun z => G (R z) * op (fun a => F (R a)) z) (nu y) ∧
(∫ z, F z * op G z ∂nu y) =
∫ z, G (R z) * op (fun a => F (R a)) z ∂nu y) ∧
(∀ G : (E × E) → ℝ, Measurable G →
Measurable (fun a : ((E × E) × (E × E)) × ℝ≥0 =>
∫ w, G (Z a.1.1.1 a.1.1.2 a.1.2 a.2 w) ∂P) ∧
∀ C : ℝ, 0 ≤ C → (∀ z, |G z| ≤ C) →
∀ y xRef : E, ∀ z : E × E, ∀ T : ℝ≥0,
Integrable (fun w => G (Z y xRef z T w)) P ∧
|∫ w, G (Z y xRef z T w) ∂P| ≤ C) ∧
(∃ Kphase : Kernel (((E × E) × (E × E)) × ℝ≥0) (E × E),
IsMarkovKernel Kphase ∧
(∀ y xRef : E, ∀ z : E × E, ∀ T : ℝ≥0,
Kphase (((y, xRef), z), T) = Measure.map (Z y xRef z T) P) ∧
(∀ y xRef : E, ∀ T : ℝ≥0,
(Kphase.comap (fun z : E × E => (((y, xRef), z), T))
(by fun_prop)).Invariant (nu y)) ∧
(∀ y xRef : E,
∃ A : ℝ≥0 → (Lp ℝ 2 (nu y) →L[ℝ] Lp ℝ 2 (nu y)),
A 0 = ContinuousLinearMap.id ℝ (Lp ℝ 2 (nu y)) ∧
(∀ f : Lp ℝ 2 (nu y),
Tendsto (fun t : ℝ≥0 => A t f) (𝓝 0) (𝓝 f)) ∧
(∀ T : ℝ≥0, ∀ f : Lp ℝ 2 (nu y),
(∀ᵐ z ∂nu y, Integrable (f : (E × E) → ℝ)
(Kphase (((y, xRef), z), T))) ∧
(A T f : (E × E) → ℝ) =ᵐ[nu y]
fun z => ∫ z', f z' ∂Kphase (((y, xRef), z), T)) ∧
(∀ T : ℝ≥0, ∀ f : Lp ℝ 2 (nu y),
(∀ᵐ z ∂nu y, 0 ≤ f z) → ∀ᵐ z ∂nu y, 0 ≤ A T f z) ∧
(∀ T : ℝ≥0, ∀ r : ℝ,
∃ hr : MemLp (fun _ : E × E => r) 2 (nu y),
A T (hr.toLp (fun _ : E × E => r)) =
hr.toLp (fun _ : E × E => r)) ∧
(∀ T : ℝ≥0, ‖A T‖ ≤ 1 ∧
∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 (nu y),
let opG : (E × E) → ℝ := fun z => ∫ w, G (Z y xRef z T w) ∂P
(∀ᵐ z ∂nu y, Integrable (fun w => G (Z y xRef z T w)) P) ∧
(∃ hOp : MemLp opG 2 (nu y), A T (hG.toLp G) = hOp.toLp opG) ∧
(∫ z, |opG z| ^ 2 ∂nu y) ≤ ∫ z, |G z| ^ 2 ∂nu y) ∧
∃ hR : MeasurePreserving R (nu y) (nu y),
let J : Lp ℝ 2 (nu y) →ₗᵢ[ℝ] Lp ℝ 2 (nu y) :=
Lp.compMeasurePreservingₗᵢ ℝ R hR
(∀ f : Lp ℝ 2 (nu y),
(J f : (E × E) → ℝ) =ᵐ[nu y] fun z => f (R z)) ∧
(∀ f : Lp ℝ 2 (nu y), J (J f) = f) ∧
(∀ T : ℝ≥0, (A T).adjoint =
J.toContinuousLinearMap.comp ((A T).comp J.toContinuousLinearMap)) ∧
let mu : Measure E := (volume : Measure E).tilted (fun x => -Vy y x)
∃ hfst : MeasurePreserving Prod.fst (nu y) mu,
let B : Lp ℝ 2 mu →ₗᵢ[ℝ] Lp ℝ 2 (nu y) :=
Lp.compMeasurePreservingₗᵢ ℝ Prod.fst hfst
let M : Lp ℝ 2 (nu y) →L[ℝ] Lp ℝ 2 mu := B.toContinuousLinearMap.adjoint
(∀ f : Lp ℝ 2 mu, (B f : (E × E) → ℝ) =ᵐ[nu y] fun z => f z.1) ∧
‖B.toContinuousLinearMap‖ ≤ 1 ∧ ‖M‖ ≤ 1 ∧
M.comp B.toContinuousLinearMap = ContinuousLinearMap.id ℝ (Lp ℝ 2 mu) ∧
(∀ G : (E × E) → ℝ, ∀ hG : MemLp G 2 (nu y),
let gbar : E → ℝ := fun x => ∫ p, G (x, p) ∂stdGaussian E
(∀ᵐ x ∂mu, Integrable (fun p => G (x, p)) (stdGaussian E)) ∧
∃ hbar : MemLp gbar 2 mu, M (hG.toLp G) = hbar.toLp gbar) ∧
(∀ f : Lp ℝ 2 mu, J (B f) = B f) ∧
M.comp J.toContinuousLinearMap = M ∧
let Kpos : ℝ≥0 → (Lp ℝ 2 mu →L[ℝ] Lp ℝ 2 mu) :=
fun T => M.comp ((A T).comp B.toContinuousLinearMap)
Kpos 0 = ContinuousLinearMap.id ℝ (Lp ℝ 2 mu) ∧
∀ T : ℝ≥0, (Kpos T).adjoint = Kpos T ∧ ‖Kpos T‖ ≤ 1 ∧
∀ f : E → ℝ, ∀ hf : MemLp f 2 mu,
let kTf : E → ℝ := fun x =>
∫ p, (∫ w, f ((Z y xRef (x, p) T w).1) ∂P) ∂stdGaussian E
(∀ᵐ x ∂mu, ∀ᵐ p ∂stdGaussian E,
Integrable (fun w => f ((Z y xRef (x, p) T w).1)) P) ∧
(∀ᵐ x ∂mu, Integrable
(fun p => ∫ w, f ((Z y xRef (x, p) T w).1) ∂P) (stdGaussian E)) ∧
∃ hk : MemLp kTf 2 mu, Kpos T (hf.toLp f) = hk.toLp kTf))
set_option maxHeartbeats 2200000
set_option maxRecDepth 12000Proof roadmap
- 1Use one actual path
The two parents prescribe identical live-record recursion. A covered interval has a live record and both paths follow the same harmonic arc. Outside coverage both use the old raw fallback. Thus the chosen paths agree pointwise for every raw clock sequence before the kernel is joined to the operator.
- 2Turn endpoint stationarity into kernel invariance
For a measurable set C integrate the fiber pushforward formula against nu_y. The product-measure formula identifies it with the endpoint preimage under nu_y times P. The existing endpoint measure-preserving identity gives nu_y(C), hence an equality of measures.
- 3Realize every L2 class by a genuine fiber integral
For Mathlib's strongly measurable representative f-sharp, the same-family parent supplies clock integrability and AE identification of A_t f. Integral-map transfers integrability to the exact kernel fiber. Lp.toLp_coeFn removes the redundant quotient construction; the integral-map identity then gives the kernel representation.
- 4Transport nonnegativity through the invariant kernel
If f-sharp is nonnegative nu_y-AE, invariance makes it nonnegative under nu_y followed by the kernel. The measure-composition AE theorem gives nonnegativity on almost every fiber. Nonnegative integration and the representation prove A_t f is nonnegative AE.
- 5Fix constant classes without pretending representatives are pointwise constant
Probability of nu_y makes every real constant c square integrable. Its Lp representative equals c only AE. Invariance transports that equality to almost every fiber. AE integral congruence and probability mass one give integral c=c. Lp.ext identifies the two classes.
Full assumptions and notation
All objects and hypotheses
- E is a finite-dimensional real inner-product Borel space with canonical volume; dimension zero is allowed.
- V is C2; alpha,beta are nonnegative with 0<alpha≤beta, and alpha||v||^2≤D2V(x)[v,v]≤beta||v||^2 for all x,v. Also eta>0 and beta eta≤1.
- Process, Gibbs probability, kernel, invariance, L2 realization, integrability, positivity and constants are conclusions, not supplied assumptions.
- Each AE assertion is for fixed parameters/time/observable. Lp coercion chooses a strongly measurable representative of an AE class. Positivity preserves AE nonnegativity, not a Hilbert quadratic form.
Mathematical proof
1. Use one actual path
The two parents prescribe identical live-record recursion. A covered interval has a live record and both paths follow the same harmonic arc. Outside coverage both use the old raw fallback. Thus the chosen paths agree pointwise for every raw clock sequence before the kernel is joined to the operator.
Corresponding Lean step
obtain ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, h110⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity.actual_l2_strong_continuity
hα hαβ hV hH hη hβη
obtain ⟨Zk, _hZkm, hZka, hZkf, _hZkgood,
Kphase, hK, hfiber, _hset, _hinit, _hbounded⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel.actual_phase_transition_kernel
hα hαβ hV hH hη hβη
-- Same literal recursion and raw fallback identify the two path witnesses.
have hZeq : Zk = Z := by
funext y xRef z t w
by_cases hx : ∃ n, w ∈ I y xRef z t n
· obtain ⟨n, hn⟩ := hx
obtain ⟨a, ha⟩ : ∃ a, record y xRef z (ε w) n = Sum.inl a := by
cases hr : record y xRef z (ε w) n with
| inl a => exact ⟨a, rfl⟩
| inr u =>
have hh := hn.1
change (record y xRef z (ε w) n).elim
(fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤) ≤ (t : WithTop ℝ≥0) at hh
rw [hr] at hh
exact False.elim ((WithTop.not_top_le_coe t) hh)
exact (hZka y xRef z w t n a hn.1 hn.2 ha).trans
(hZa y xRef z w t n a hn ha).symm
· exact (hZkf y xRef z w t hx).trans (hZf y xRef z w t hx).symm
rw [hZeq] at hfiber
Existential witnesses are identified, not assumed equal. No new fallback semantics is introduced.
2. Turn endpoint stationarity into kernel invariance
For a measurable set C integrate the fiber pushforward formula against nu_y. The product-measure formula identifies it with the endpoint preimage under nu_y times P. The existing endpoint measure-preserving identity gives nu_y(C), hence an equality of measures.
Corresponding Lean step
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
letI : IsMarkovKernel Kphase := hK
have hzM (y xRef : E) (z : E × E) (T : ℝ≥0) :
Measurable (Z y xRef z T) := hZm.comp
(show Measurable (fun w : ℕ → ℝ => (((y, xRef), z), T, w)) from
measurable_const.prodMk (measurable_const.prodMk measurable_id))
-- A fixed-time endpoint pushforward, not a restart/Markov argument.
have hInv (y xRef : E) (T : ℝ≥0) :
(Kphase.comap (fun z : E × E => (((y, xRef), z), T))
(by fun_prop)).Invariant (nu y) := by
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have he := (h106 y xRef T).1
change (nu y).bind κ = nu y
calc
(nu y).bind κ =
Measure.map (fun a : (E × E) × (ℕ → ℝ) => Z y xRef a.1 T a.2)
((nu y).prod P) := by
ext s hs
rw [Measure.bind_apply hs κ.aemeasurable, Measure.map_apply he.measurable hs,
Measure.prod_apply (he.measurable hs)]
apply lintegral_congr_ae
filter_upwards with z
change Kphase (((y, xRef), z), T) s =
P ((Z y xRef z T) ⁻¹' s)
rw [hfiber, Measure.map_apply (hzM y xRef z T) hs]
_ = nu y := he.map_eq
Kernel.comap fixes y,r,t. Probability fibers do not prove process Markovness or restart. No generator-domain or integration-by-parts shortcut is used.
3. Realize every L2 class by a genuine fiber integral
For Mathlib's strongly measurable representative f-sharp, the same-family parent supplies clock integrability and AE identification of A_t f. Integral-map transfers integrability to the exact kernel fiber. Lp.toLp_coeFn removes the redundant quotient construction; the integral-map identity then gives the kernel representation.
Corresponding Lean step
refine ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, Kphase, hK, hfiber, hInv, ?_⟩
intro y xRef
obtain ⟨L, hL0, hSC, hL, hRest⟩ := h110 y xRef
have hnorm := ActualPhaseNormalization.actual_phase_gibbs_normalization
hα hαβ hV hH hη hβη y
letI : IsProbabilityMeasure (nu y) := by
have hp := hnorm.2.2.2.2.2.1
rw [hnorm.2.2.2.2.2.2] at hp
exact hp
have hreal (T : ℝ≥0) (f : Lp ℝ 2 (nu y)) :
(∀ᵐ z ∂nu y, Integrable (f : (E × E) → ℝ)
(Kphase (((y, xRef), z), T))) ∧
(L T f : (E × E) → ℝ) =ᵐ[nu y]
fun z => ∫ z', f z' ∂Kphase (((y, xRef), z), T) := by
let opG : (E × E) → ℝ := fun z => ∫ w, f (Z y xRef z T w) ∂P
have hclock := (hL T).2 (f : (E × E) → ℝ) (Lp.memLp f)
obtain ⟨hOp, heq⟩ := hclock.2.1
have heq' : L T f = hOp.toLp opG := by
simpa only [Lp.toLp_coeFn] using heq
have hae : (L T f : (E × E) → ℝ) =ᵐ[nu y] opG := by
rw [heq']
exact hOp.coeFn_toLp
have hinter (z : E × E) :
(∫ z', f z' ∂Kphase (((y, xRef), z), T)) = opG z := by
rw [hfiber]
exact integral_map (hzM y xRef z T).aemeasurable
(Lp.stronglyMeasurable f).aestronglyMeasurable
refine ⟨?_, ?_⟩
· filter_upwards [hclock.1] with z hz
rw [hfiber]
exact (integrable_map_measure
(Lp.stronglyMeasurable f).aestronglyMeasurable (hzM y xRef z T).aemeasurable).2 hz
· filter_upwards [hae] with z hz
exact hz.trans (hinter z).symm
refine ⟨L, hL0, hSC, hreal, ?_, ?_, hL, hRest⟩
Integrability is a separate output, not inferred from totalized integral syntax. Representatives agree AE, not pointwise.
4. Transport nonnegativity through the invariant kernel
If f-sharp is nonnegative nu_y-AE, invariance makes it nonnegative under nu_y followed by the kernel. The measure-composition AE theorem gives nonnegativity on almost every fiber. Nonnegative integration and the representation prove A_t f is nonnegative AE.
Corresponding Lean step
· intro T f hf
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have hcomp : ∀ᵐ z ∂((nu y).bind κ), 0 ≤ f z := by
rw [(hInv y xRef T).def]
exact hf
have hfib := Measure.ae_ae_of_ae_comp (κ := κ) hcomp
filter_upwards [(hreal T f).2, hfib] with z hz hzz
rw [hz]
exact integral_nonneg_of_ae hzz
Positivity preserving is not Loewner positivity or phase self-adjointness.
5. Fix constant classes without pretending representatives are pointwise constant
Probability of nu_y makes every real constant c square integrable. Its Lp representative equals c only AE. Invariance transports that equality to almost every fiber. AE integral congruence and probability mass one give integral c=c. Lp.ext identifies the two classes.
Corresponding Lean step
· intro T r
have hr : MemLp (fun _ : E × E => r) 2 (nu y) := memLp_const r
let f : Lp ℝ 2 (nu y) := hr.toLp (fun _ : E × E => r)
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have hcae : (f : (E × E) → ℝ) =ᵐ[nu y] fun _ => r := hr.coeFn_toLp
have hcomp : ∀ᵐ z ∂((nu y).bind κ), f z = r := by
rw [(hInv y xRef T).def]
exact hcae
have hfib := Measure.ae_ae_of_ae_comp (κ := κ) hcomp
refine ⟨hr, ?_⟩
change L T f = f
apply Lp.ext
filter_upwards [(hreal T f).2, hcae, hfib] with z hz hzr hfz
calc
L T f z = ∫ z', f z' ∂Kphase (((y, xRef), z), T) := hz
_ = ∫ _ : E × E, r ∂Kphase (((y, xRef), z), T) := integral_congr_ae hfz
_ = r := by simp
_ = f z := hzr.symm
The AE equality is transported before the constant integral is simplified.
Lean verification
The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.
Lean proof · actual_kernel_l2_realization
Same literal path -> endpoint pushforward -> invariant kernel -> quotient-safe all-L2 representation -> AE positivity and constants.
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_kernel_l2_realization
{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_kernel_l2_realization_statement hα hαβ hV hH hη hβη := by
classical
unfold actual_kernel_l2_realization_statement
intro c Φ S rate Λ τ next record P ε history Rec Hist readTime Δ Prefix m zAt K qReal q A eventTime I N liveTime d survival weight C Path Ψ Γ ρ R Vy nu
obtain ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, h110⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity.actual_l2_strong_continuity
hα hαβ hV hH hη hβη
obtain ⟨Zk, _hZkm, hZka, hZkf, _hZkgood,
Kphase, hK, hfiber, _hset, _hinit, _hbounded⟩ :=
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel.actual_phase_transition_kernel
hα hαβ hV hH hη hβη
-- Same literal recursion and raw fallback identify the two path witnesses.
have hZeq : Zk = Z := by
funext y xRef z t w
by_cases hx : ∃ n, w ∈ I y xRef z t n
· obtain ⟨n, hn⟩ := hx
obtain ⟨a, ha⟩ : ∃ a, record y xRef z (ε w) n = Sum.inl a := by
cases hr : record y xRef z (ε w) n with
| inl a => exact ⟨a, rfl⟩
| inr u =>
have hh := hn.1
change (record y xRef z (ε w) n).elim
(fun a => (a.1 : WithTop ℝ≥0)) (fun _ => ⊤) ≤ (t : WithTop ℝ≥0) at hh
rw [hr] at hh
exact False.elim ((WithTop.not_top_le_coe t) hh)
exact (hZka y xRef z w t n a hn.1 hn.2 ha).trans
(hZa y xRef z w t n a hn ha).symm
· exact (hZkf y xRef z w t hx).trans (hZf y xRef z w t hx).symm
rw [hZeq] at hfiber
letI : IsProbabilityMeasure P :=
AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws.1
letI : IsMarkovKernel Kphase := hK
have hzM (y xRef : E) (z : E × E) (T : ℝ≥0) :
Measurable (Z y xRef z T) := hZm.comp
(show Measurable (fun w : ℕ → ℝ => (((y, xRef), z), T, w)) from
measurable_const.prodMk (measurable_const.prodMk measurable_id))
-- A fixed-time endpoint pushforward, not a restart/Markov argument.
have hInv (y xRef : E) (T : ℝ≥0) :
(Kphase.comap (fun z : E × E => (((y, xRef), z), T))
(by fun_prop)).Invariant (nu y) := by
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have he := (h106 y xRef T).1
change (nu y).bind κ = nu y
calc
(nu y).bind κ =
Measure.map (fun a : (E × E) × (ℕ → ℝ) => Z y xRef a.1 T a.2)
((nu y).prod P) := by
ext s hs
rw [Measure.bind_apply hs κ.aemeasurable, Measure.map_apply he.measurable hs,
Measure.prod_apply (he.measurable hs)]
apply lintegral_congr_ae
filter_upwards with z
change Kphase (((y, xRef), z), T) s =
P ((Z y xRef z T) ⁻¹' s)
rw [hfiber, Measure.map_apply (hzM y xRef z T) hs]
_ = nu y := he.map_eq
refine ⟨Z, hZm, hZa, hZf, hZ0, h106, hBorel, Kphase, hK, hfiber, hInv, ?_⟩
intro y xRef
obtain ⟨L, hL0, hSC, hL, hRest⟩ := h110 y xRef
have hnorm := ActualPhaseNormalization.actual_phase_gibbs_normalization
hα hαβ hV hH hη hβη y
letI : IsProbabilityMeasure (nu y) := by
have hp := hnorm.2.2.2.2.2.1
rw [hnorm.2.2.2.2.2.2] at hp
exact hp
have hreal (T : ℝ≥0) (f : Lp ℝ 2 (nu y)) :
(∀ᵐ z ∂nu y, Integrable (f : (E × E) → ℝ)
(Kphase (((y, xRef), z), T))) ∧
(L T f : (E × E) → ℝ) =ᵐ[nu y]
fun z => ∫ z', f z' ∂Kphase (((y, xRef), z), T) := by
let opG : (E × E) → ℝ := fun z => ∫ w, f (Z y xRef z T w) ∂P
have hclock := (hL T).2 (f : (E × E) → ℝ) (Lp.memLp f)
obtain ⟨hOp, heq⟩ := hclock.2.1
have heq' : L T f = hOp.toLp opG := by
simpa only [Lp.toLp_coeFn] using heq
have hae : (L T f : (E × E) → ℝ) =ᵐ[nu y] opG := by
rw [heq']
exact hOp.coeFn_toLp
have hinter (z : E × E) :
(∫ z', f z' ∂Kphase (((y, xRef), z), T)) = opG z := by
rw [hfiber]
exact integral_map (hzM y xRef z T).aemeasurable
(Lp.stronglyMeasurable f).aestronglyMeasurable
refine ⟨?_, ?_⟩
· filter_upwards [hclock.1] with z hz
rw [hfiber]
exact (integrable_map_measure
(Lp.stronglyMeasurable f).aestronglyMeasurable (hzM y xRef z T).aemeasurable).2 hz
· filter_upwards [hae] with z hz
exact hz.trans (hinter z).symm
refine ⟨L, hL0, hSC, hreal, ?_, ?_, hL, hRest⟩
· intro T f hf
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have hcomp : ∀ᵐ z ∂((nu y).bind κ), 0 ≤ f z := by
rw [(hInv y xRef T).def]
exact hf
have hfib := Measure.ae_ae_of_ae_comp (κ := κ) hcomp
filter_upwards [(hreal T f).2, hfib] with z hz hzz
rw [hz]
exact integral_nonneg_of_ae hzz
· intro T r
have hr : MemLp (fun _ : E × E => r) 2 (nu y) := memLp_const r
let f : Lp ℝ 2 (nu y) := hr.toLp (fun _ : E × E => r)
let κ : Kernel (E × E) (E × E) :=
Kphase.comap (fun z : E × E => (((y, xRef), z), T)) (by fun_prop)
have hcae : (f : (E × E) → ℝ) =ᵐ[nu y] fun _ => r := hr.coeFn_toLp
have hcomp : ∀ᵐ z ∂((nu y).bind κ), f z = r := by
rw [(hInv y xRef T).def]
exact hcae
have hfib := Measure.ae_ae_of_ae_comp (κ := κ) hcomp
refine ⟨hr, ?_⟩
change L T f = f
apply Lp.ext
filter_upwards [(hreal T f).2, hcae, hfib] with z hz hzr hfz
calc
L T f z = ∫ z', f z' ∂Kphase (((y, xRef), z), T) := hz
_ = ∫ _ : E × E, r ∂Kphase (((y, xRef), z), T) := integral_congr_ae hfz
_ = r := by simp
_ = f z := hzr.symm
end
end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualKernelL2RealizationScope and omitted-condition boundaries
- Only same-witness phase probability-kernel/L2 realization, invariant state sections, AE positivity and constant classes are added. Process Markovness/restart, Chapman–Kolmogorov/semigroup, adjoint density evolution/fixed constants, position probability-kernel realization, independent-reference averaging, hypocoercivity, simulation errors, actual-input expected costs, composition and all four full papers remain open.
Sources, dependencies, and reuse
Source and reuse
Samplinglib parents called
AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity.actual_l2_strong_continuityAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel.actual_phase_transition_kernelAutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization.actual_phase_gibbs_normalizationAutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct.unit_exponential_product_laws
Mathlib API called (external library)
- MeasureTheory.Measure.bind_apply
- MeasureTheory.Measure.prod_apply
- MeasureTheory.Measure.map_apply
- MeasureTheory.Measure.ae_ae_of_ae_comp
- MeasureTheory.integrable_map_measure
- MeasureTheory.integral_map
- MeasureTheory.Lp.toLp_coeFn
- MeasureTheory.Lp.stronglyMeasurable
- MeasureTheory.MemLp.coeFn_toLp
- MeasureTheory.Lp.ext
- MeasureTheory.integral_nonneg_of_ae
- MeasureTheory.integral_congr_ae
- MeasureTheory.memLp_const
Mathematical sources
- Appendix A.1 and Definition D.2, phase-kernel realization component — Only same-witness phase probability-kernel/L2 realization, invariant state sections, AE positivity and constant classes are added. Process Markovness/restart, Chapman–Kolmogorov/semigroup, adjoint density evolution/fixed constants, position probability-kernel realization, independent-reference averaging, hypocoercivity, simulation errors, actual-input expected costs, composition and all four full papers remain open.
Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.