AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance

Samplinglib mathematical lesson

Actual PBPS: why the reflected augmented transition preserves its target

AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance.actual_augmented_kernel_invariant · theorem · Teaching coverage

Read this first

Mathematical statement

Let \(E\) be a finite-dimensional real inner-product Borel space, including dimension zero. Suppose \(V\in C^2\), \(0<\alpha\le\beta\), \(\alpha\|v\|^2\le D^2V(x)[v,v]\le\beta\|v\|^2\) for all \(x,v\), \(\eta>0\), \(\beta\eta\le1\), and a fixed scalar \(0<\rho<1\). Let \(\mu(dx)\propto e^{-V(x)}dx\) and let \(J\) be the law of \((X,X+\sqrt\eta G)\) for independent \(X\sim\mu\), \(G\sim\mathcal N(0,I)\). Let \(q_y(dx)\propto e^{-V(x)-\|x-y\|^2/(2\eta)}dx\) and let \(H_y(x,\cdot)\) be the actual time-pi returned-position kernel, with an independent reference from \(q_y\), Gaussian momentum and iid unit exponential clocks. Reflect \(y\) to \(y\prime=2x-y\), draw the next position from \(\rho q_{y\prime}+(1-\rho)H_{y\prime}(x,\cdot)\), and retain \(y\prime\). This defines a Markov kernel \(K\) preserving \(J\). All probability normalizations and the conditional-kernel certificate are conclusions. The same literal clock recursion, covered-arc/fallback laws, parameterwise AE coverage/initialization, and actual H witness are retained in the folded full statement.

\[\begin{aligned} y\prime&=2x-y,\\ K((x,y),dx\prime\,dy\prime)&=\bigl[\rho q_{y\prime}(dx\prime)+(1-\rho)H(y\prime,x)(dx\prime)\bigr]\,\delta_{2x-y}(dy\prime),\\ J K&=J.\end{aligned}\]

Lean statement · actual_augmented_kernel_invariant

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_augmented_kernel_invariant
    {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)
    (ρ : ℝ) (hρpos : 0 < ρ) (hρlt : ρ < 1) :
    actual_augmented_kernel_invariance_statement hα hαβ hV hH hη hβη ρ hρpos hρlt

Exact module and namespace context

Full Lean proposition (definition) · actual_augmented_kernel_invariance_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_augmented_kernel_invariance_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)
    (ρ : ℝ) (hρpos : 0 < ρ) (hρlt : ρ < 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⟩
    let μ : Measure E := (volume : Measure E).tilted (fun x => -V x)
    let J : Measure (E × E) := Measure.map
      (fun z : E × E => (z.1, z.1 + Real.sqrt η • z.2)) (μ.prod γ)
    IsProbabilityMeasure μ ∧ IsProbabilityMeasure J ∧
    ∃ 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) ∧
      (J.map Prod.swap).IsCondKernel R ∧
      ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧ K.Invariant J ∧
        (∀ z : E × E, K z =
          (ENNReal.ofReal ρ • q ((2 : ℝ) • z.1 - z.2) +
            ENNReal.ofReal (1 - ρ) • H ((2 : ℝ) • z.1 - z.2, z.1)).prod
          (Measure.dirac ((2 : ℝ) • z.1 - z.2)))

Exact module and namespace context

Proof roadmap

1Normalize the real target and identify the SAME conditional kernel
The genuine Hessian lower bound gives a finite positive Gibbs normalizer. The existing Gaussian augmentation is therefore a probability law. Its explicit backward conditional is a quadratic exponential tilt of mu. The nested-tilt identity turns it into the literal volume tilt q_y. Both conditional kernels have this fiber at every y, so they are equal as kernels; we transfer the disintegration certificate to the R retained by the actual half-turn producer.
2Mix two probability updates at fixed auxiliary coordinate
The actual half-turn is reversible for q_y, hence invariant. Exact resampling has the constant output law q_y and also preserves it. Construct their jointly measurable fixed two-component mixture F using the existing finite-mixture API. The nonnegative weights sum to one, so F is Markov; its restriction to each y preserves q_y.
3Explain the omitted retained-coordinate Tonelli argument
Work in the order (y,x), with nu=J.swap. For any measurable set S, write S_y for its measurable section. The lifted update L keeps y and draws xprime from F_y(x). Disintegrate nu; Tonelli applies to these nonnegative measurable probabilities. Fiber invariance replaces the inner integral by q_y(S_y), and the same disintegration recovers nu(S). Thus L preserves the entire joint law, not only its marginals.
4Swap coordinates back, then apply reflection first
Conjugating L by the measurable swap returns to the order (x,y), giving an invariant Markov kernel B. The existing Gaussian reflection U(x,y)=(x,2x-y) preserves J. Define K as first U, then B. Composition of two J-preserving kernels preserves J. Evaluating the kernel removes the deterministic input and swaps the product factors, giving exactly the displayed transition law.
5Connect every adapter to the actual process, with no supplied invariant law
The public proof retains the actual jointly measurable Z and its exact H pushforward, covered-arc/fallback equations and local initialization. It derives the fiber invariant input from the retained every-y detailed balance, obtains reflection from the owned Gaussian producer, and invokes the private construction. Finally replace the exact R fibers by q_y to obtain the paper transition, without replacing H by an arbitrary convenient kernel.

Full assumptions and notation

All objects and hypotheses

The six standing analytic binders are unchanged: genuine C2/Hessian bounds, positive alpha and eta, alpha≤beta and beta eta≤1. The only new source binders are the fixed scalar rho and 0<rho<1; weights do not depend on state.
The potential, Gaussian, canonical volume and Hilbert-space assumptions match the actual half-turn producer. fderiv is totalized in Lean, but C2 supplies genuine differentiability; no derivative-zero fallback is used to infer regularity.
Gibbs integrability/positive normalizer, probability, explicit everywhere-defined q_y, joint measurable kernels, conditional disintegration, mixture mass one and invariant measures are internally derived, not supplied premises.
Conditional R is the explicit normalized quadratic tilt at EVERY y. Its equality to the retained R follows from their explicit fiber laws, not from almost-everywhere uniqueness of arbitrary conditional versions.
All old path coverage/initialization null sets remain parameterwise. This one-step law does not assert a temporal Markov/restart/semigroup property or any convergence rate.

Mathematical proof

1. Normalize the real target and identify the SAME conditional kernel

The genuine Hessian lower bound gives a finite positive Gibbs normalizer. The existing Gaussian augmentation is therefore a probability law. Its explicit backward conditional is a quadratic exponential tilt of mu. The nested-tilt identity turns it into the literal volume tilt q_y. Both conditional kernels have this fiber at every y, so they are equal as kernels; we transfer the disintegration certificate to the R retained by the actual half-turn producer.

\[\begin{aligned}(\mu^{\rm tilt(-\|\cdot-y\|^2/(2\eta))})(dx)&=q_y(dx),\\ R_y=q_y,\qquad J^{\rm swap}&=J^Y\otimes R.\end{aligned}\]

Corresponding Lean step

  obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hrev, hHlaw, hH0, hHgood⟩ :=
    ActualHalfTurnReversibility.actual_half_turn_reversible hα hαβ hV hH hη hβη
  letI : IsMarkovKernel R := hR
  letI : IsMarkovKernel H := hHK
  have hnorm := GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x v => (hH x v).1) hη
  have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
    Integrable.of_integral_ne_zero hnorm.1.ne'
  letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
  letI : IsProbabilityMeasure J := hnorm.2.1
  obtain ⟨Rc, hRc, hRctilt, hcond⟩ :=
    TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
  have hRcq (y : E) : Rc y = q y := by
    rw [hRctilt y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
      tilted_tilted hi]
    congr 1
    funext x
    dsimp only [Pi.add_apply]
    ring
  have hRcR : Rc = R := by
    ext y : 1
    rw [hRcq y, hRq y]
  subst Rc
  change (J.map Prod.swap).IsCondKernel R at hcond
  letI : (J.map Prod.swap).IsCondKernel R := hcond

This is pointwise identity of explicitly chosen versions, not a pointwise claim obtained from AE conditional uniqueness. Integrability is established before applying the normalized nested-tilt identity.

2. Mix two probability updates at fixed auxiliary coordinate

The actual half-turn is reversible for q_y, hence invariant. Exact resampling has the constant output law q_y and also preserves it. Construct their jointly measurable fixed two-component mixture F using the existing finite-mixture API. The nonnegative weights sum to one, so F is Markov; its restriction to each y preserves q_y.

\[\begin{aligned}q_y H_y&=q_y,\quad q_y R_y=q_y,\\ F_y(x)&=\rho q_y+(1-\rho)H_y(x),\qquad q_y F_y=q_y.\end{aligned}\]

Corresponding Lean step

private theorem reflected_conditional_mixture
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    (J : Measure (E × E)) [IsProbabilityMeasure J]
    (R : Kernel E E) [IsMarkovKernel R] [(J.map Prod.swap).IsCondKernel R]
    (H : Kernel (E × E) E) [IsMarkovKernel H]
    (hH : ∀ y, (H.comap (fun x => (y, x)) (by fun_prop)).Invariant (R y))
    (ρ : ℝ) (hρpos : 0 < ρ) (hρlt : ρ < 1)
    (hreflection : J.map (fun z => (z.1, (2 : ℝ) • z.1 - z.2)) = J) :
    ∃ K : Kernel (E × E) (E × E), IsMarkovKernel K ∧ K.Invariant J ∧
      ∀ z, K z = (ENNReal.ofReal ρ • R ((2 : ℝ) • z.1 - z.2) +
        ENNReal.ofReal (1 - ρ) • H ((2 : ℝ) • z.1 - z.2, z.1)).prod
        (Measure.dirac ((2 : ℝ) • z.1 - z.2)) := by
  classical
  let w : Fin 2 → ℝ≥0 := ![Real.toNNReal ρ, Real.toNNReal (1 - ρ)]
  have hw : ∑ i, w i = 1 := by
    apply NNReal.coe_injective
    simp only [Fin.sum_univ_two, w, Matrix.cons_val_zero, Matrix.cons_val_one,
      NNReal.coe_add, NNReal.coe_one, Real.coe_toNNReal ρ hρpos.le,
      Real.coe_toNNReal (1 - ρ) (sub_nonneg.mpr hρlt.le)]
    ring
  let A : Kernel (E × E) E := R.comap Prod.fst measurable_fst
  let ks : Fin 2 → Kernel (E × E) E := ![A, H]
  letI : ∀ i, IsMarkovKernel (ks i) := by
    intro i
    fin_cases i <;> dsimp [ks, A] <;> infer_instance
  let F := AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture w ks
  letI : IsMarkovKernel F :=
    AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture_isMarkovKernel w ks hw
  have hFlaw (z : E × E) : F z = ENNReal.ofReal ρ • R z.1 +
      ENNReal.ofReal (1 - ρ) • H z := by
    rw [AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture_apply,
      Fin.sum_univ_two]
    rfl
  have hF (y : E) : (F.comap (fun x => (y, x)) (by fun_prop)).Invariant (R y) := by
    let sy : Fin 2 → Kernel E E :=
      ![Kernel.const E (R y), H.comap (fun x => (y, x)) (by fun_prop)]
    letI : ∀ i, IsMarkovKernel (sy i) := by
      intro i
      fin_cases i <;> dsimp [sy] <;> infer_instance
    have hsy : ∀ i, (sy i).Invariant (R y) := by
      intro i
      fin_cases i
      · change (R y).bind (fun _ => R y) = R y
        simp [Measure.bind_const]
      · exact hH y
    have heq : F.comap (fun x => (y, x)) (by fun_prop) =
        AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture w sy := by
      ext x : 1
      rw [Kernel.comap_apply, hFlaw,
        AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture_apply,
        Fin.sum_univ_two]
      rfl
    rw [heq]
    exact AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixture.finiteMixture_invariant
      w sy (R y) hw hsy

The excerpt implements the mixture adapter: its private hH input is discharged from actual reversibility in the public proof. It is not a new public hypothesis. State-dependent selection weights would invalidate this inference.

3. Explain the omitted retained-coordinate Tonelli argument

Work in the order (y,x), with nu=J.swap. For any measurable set S, write S_y for its measurable section. The lifted update L keeps y and draws xprime from F_y(x). Disintegrate nu; Tonelli applies to these nonnegative measurable probabilities. Fiber invariance replaces the inner integral by q_y(S_y), and the same disintegration recovers nu(S). Thus L preserves the entire joint law, not only its marginals.

\[\begin{aligned}(\nu L)(S)&=\int J^Y(dy)\int q_y(dx)F_y(x,S_y)\\&=\int J^Y(dy)q_y(S_y)=\nu(S),\\ S_y&=\{x:(y,x)\in S\}.\end{aligned}\]

Corresponding Lean step

private theorem retained_invariant {A B : Type*} [MeasurableSpace A] [MeasurableSpace B]
    (ν : Measure (A × B)) [IsProbabilityMeasure ν]
    (R : Kernel A B) [IsMarkovKernel R] [ν.IsCondKernel R]
    (F : Kernel (A × B) B) [IsMarkovKernel F]
    (hF : ∀ a, (F.comap (fun b => (a, b)) (by fun_prop)).Invariant (R a)) :
    ((Kernel.deterministic Prod.fst measurable_fst) ×ₖ F).Invariant ν := by
  let L := (Kernel.deterministic Prod.fst measurable_fst) ×ₖ F
  change ν.bind L = ν
  ext s hs
  calc
    (ν.bind L) s = ∫⁻ z, L z s ∂ν :=
      Measure.bind_apply hs L.aemeasurable
    _ = ∫⁻ a, ∫⁻ b, L (a, b) s ∂R a ∂ν.fst := by
      rw [← Measure.lintegral_compProd (L.measurable_coe hs), ν.disintegrate R]
    _ = ∫⁻ a, R a (Prod.mk a ⁻¹' s) ∂ν.fst := by
      apply lintegral_congr
      intro a
      simp_rw [show ∀ b, L (a, b) s = F (a, b) (Prod.mk a ⁻¹' s) from
        fun b => Kernel.deterministic_prod_apply' measurable_fst F (a, b) hs]
      have ht : MeasurableSet (Prod.mk a ⁻¹' s) := hs.preimage measurable_prodMk_left
      have hi := congrArg (fun m : Measure B => m (Prod.mk a ⁻¹' s)) (hF a).def
      rw [Measure.bind_apply ht (Kernel.aemeasurable _)] at hi
      exact hi
    _ = (ν.fst ⊗ₘ R) s := (Measure.compProd_apply hs).symm
    _ = ν s := congrArg (fun m : Measure (A × B) => m s) (ν.disintegrate R)

No unbounded signed integral, moment assumption or extra domination premise is needed. Kernel measurability and section measurability are explicit; the implementation uses ENNReal lintegrals and the exact conditional certificate.

4. Swap coordinates back, then apply reflection first

Conjugating L by the measurable swap returns to the order (x,y), giving an invariant Markov kernel B. The existing Gaussian reflection U(x,y)=(x,2x-y) preserves J. Define K as first U, then B. Composition of two J-preserving kernels preserves J. Evaluating the kernel removes the deterministic input and swaps the product factors, giving exactly the displayed transition law.

\[\begin{aligned} U_\#J&=J,\quad JB=J,\\ JK&=(U_\#J)B=JB=J,\\K(z)&=B(U(z)).\end{aligned}\]

Corresponding Lean step

  letI : IsProbabilityMeasure (J.map Prod.swap) :=
    Measure.isProbabilityMeasure_map measurable_swap.aemeasurable
  let L : Kernel (E × E) (E × E) :=
    (Kernel.deterministic Prod.fst measurable_fst) ×ₖ F
  have hL : L.Invariant (J.map Prod.swap) := retained_invariant (J.map Prod.swap) R F hF
  let B : Kernel (E × E) (E × E) := (L.comap Prod.swap measurable_swap).map Prod.swap
  letI : IsMarkovKernel B := Kernel.IsMarkovKernel.map _ measurable_swap
  have hB : B.Invariant J := by
    have ht := AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransport.invariant_map_comap
      (MeasurableEquiv.prodComm : E × E ≃ᵐ E × E) hL
    change B.Invariant ((J.map Prod.swap).map Prod.swap) at ht
    rw [Measure.map_map measurable_swap measurable_swap] at ht
    simpa only [Prod.swap_swap_eq, Measure.map_id] using ht
  let U : E × E → E × E := fun z => (z.1, (2 : ℝ) • z.1 - z.2)
  have hU : Measurable U := by
    dsimp only [U]
    fun_prop
  have hUinv : (Kernel.deterministic U hU).Invariant J := by
    change (Kernel.deterministic U hU) ∘ₘ J = J
    rw [Measure.deterministic_comp_eq_map]
    exact hreflection
  let K := B ∘ₖ Kernel.deterministic U hU
  refine ⟨K, inferInstance, hB.comp hUinv, ?_⟩
  intro z
  change (B ∘ₖ Kernel.deterministic U hU) z = _
  rw [Kernel.comp_deterministic_eq_comap, Kernel.comap_apply, Kernel.map_apply _ measurable_swap,
    Kernel.comap_apply, Kernel.prod_apply, Kernel.deterministic_apply]
  rw [Measure.prod_swap, hFlaw]
  rfl

The order matters: the conditional mixture is evaluated at the reflected auxiliary coordinate, not the original y. Kernel.map can totalize to zero for nonmeasurable maps; here genuine swap/reflection measurability is proved, and Markovness is checked separately.

5. Connect every adapter to the actual process, with no supplied invariant law

The public proof retains the actual jointly measurable Z and its exact H pushforward, covered-arc/fallback equations and local initialization. It derives the fiber invariant input from the retained every-y detailed balance, obtains reflection from the owned Gaussian producer, and invokes the private construction. Finally replace the exact R fibers by q_y to obtain the paper transition, without replacing H by an arbitrary convenient kernel.

\[\begin{aligned} y\prime&=2x-y,\\ K((x,y),dx\prime\,dy\prime)&=\bigl[\rho q_{y\prime}(dx\prime)+(1-\rho)H(y\prime,x)(dx\prime)\bigr]\,\delta_{2x-y}(dy\prime),\\ J K&=J.\end{aligned}\]

Corresponding Lean step

  refine ⟨inferInstance, inferInstance, Z, hZM, hZa, hZf, hgood, R, hR, hRq,
    H, hHK, hrev, hHlaw, hH0, hHgood, hcond, ?_⟩
  have hHinv (y : E) : (H.comap (fun x => (y, x)) (by fun_prop)).Invariant (R y) := by
    rw [hRq y]
    exact (hrev y).invariant
  have href : J.map (fun z => (z.1, (2 : ℝ) • z.1 - z.2)) = J :=
    (GaussianReflection.reflection_preserves_augmentation μ η hη).2
  obtain ⟨K, hK, hKinv, hKlaw⟩ :=
    reflected_conditional_mixture J R H hHinv ρ hρpos hρlt href
  refine ⟨K, hK, hKinv, ?_⟩
  intro z
  simpa only [hRq] using hKlaw z

Local compilation proves this proposition. Independent source review, integration and purification are separately tracked. In particular, invariant law alone supplies none of the later hypocoercivity or actual expected-cost conclusions.

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · actual_augmented_kernel_invariant

Normalize and identify explicit conditional -> fixed conditional mixture -> measurable-section Tonelli lift -> swap transport -> reflection-first composition -> same actual K law.

Download module (.lean)

theorem actual_augmented_kernel_invariant
    {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)
    (ρ : ℝ) (hρpos : 0 < ρ) (hρlt : ρ < 1) :
    actual_augmented_kernel_invariance_statement hα hαβ hV hH hη hβη ρ hρpos hρlt := by
  classical
  unfold actual_augmented_kernel_invariance_statement
  intro P ε c Φ S rate Λ τ next record eventTime q γ M tπ μ J
  obtain ⟨Z, hZM, hZa, hZf, hgood, R, hR, hRq, H, hHK, hrev, hHlaw, hH0, hHgood⟩ :=
    ActualHalfTurnReversibility.actual_half_turn_reversible hα hαβ hV hH hη hβη
  letI : IsMarkovKernel R := hR
  letI : IsMarkovKernel H := hHK
  have hnorm := GibbsAugmentation.normalized_augmentation_density
    hα hV (fun x v => (hH x v).1) hη
  have hi : Integrable (fun x : E => Real.exp (-V x)) (volume : Measure E) :=
    Integrable.of_integral_ne_zero hnorm.1.ne'
  letI : IsProbabilityMeasure μ := isProbabilityMeasure_tilted hi
  letI : IsProbabilityMeasure J := hnorm.2.1
  obtain ⟨Rc, hRc, hRctilt, hcond⟩ :=
    TechnicalLemmas.Probability.GaussianConditionalKernel.exists_tilted_isCondKernel μ hη
  have hRcq (y : E) : Rc y = q y := by
    rw [hRctilt y, show μ = (volume : Measure E).tilted (fun x => -V x) from rfl,
      tilted_tilted hi]
    congr 1
    funext x
    dsimp only [Pi.add_apply]
    ring
  have hRcR : Rc = R := by
    ext y : 1
    rw [hRcq y, hRq y]
  subst Rc
  change (J.map Prod.swap).IsCondKernel R at hcond
  letI : (J.map Prod.swap).IsCondKernel R := hcond
  refine ⟨inferInstance, inferInstance, Z, hZM, hZa, hZf, hgood, R, hR, hRq,
    H, hHK, hrev, hHlaw, hH0, hHgood, hcond, ?_⟩
  have hHinv (y : E) : (H.comap (fun x => (y, x)) (by fun_prop)).Invariant (R y) := by
    rw [hRq y]
    exact (hrev y).invariant
  have href : J.map (fun z => (z.1, (2 : ℝ) • z.1 - z.2)) = J :=
    (GaussianReflection.reflection_preserves_augmentation μ η hη).2
  obtain ⟨K, hK, hKinv, hKlaw⟩ :=
    reflected_conditional_mixture J R H hHinv ρ hρpos hρlt href
  refine ⟨K, hK, hKinv, ?_⟩
  intro z
  simpa only [hRq] using hKlaw z

end AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance

Exact module and namespace context

Scope and omitted-condition boundaries

Exact one-step invariance of the literal augmented transition only. No process restart/semigroup, augmented all-L2 operator, hypocoercivity or quantitative convergence, implementation error/caps/cost, warm-start initialization, composition or complete paper.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.tilted_tilted
MeasureTheory.Measure.disintegrate
MeasureTheory.Measure.lintegral_compProd
MeasureTheory.Measure.compProd_apply
MeasureTheory.Measure.bind_apply
ProbabilityTheory.Kernel.IsReversible.invariant
ProbabilityTheory.Kernel.Invariant.comp
ProbabilityTheory.Kernel.deterministic_prod_apply'

Mathematical sources

Proposition3.4, equation3.11 and Algorithm2; standing1.1/scale2.2; reflectionProp2.1iii and conditional reversibilityProp3.2 — Exact one-step invariance of the literal augmented transition only. No process restart/semigroup, augmented all-L2 operator, hypocoercivity or quantitative convergence, implementation error/caps/cost, warm-start initialization, 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.

ActualAugmentedKernelInvariance: mathematical reading route

Actual PBPS: why the reflected augmented transition preserves its target

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Normalize the real target and identify the SAME conditional kernel

2. Mix two probability updates at fixed auxiliary coordinate

3. Explain the omitted retained-coordinate Tonelli argument

4. Swap coordinates back, then apply reflection first

5. Connect every adapter to the actual process, with no supplied invariant law

Lean verification

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources