From an invariant Markov kernel to its genuine L2 observable operator

ASTIS standard source-neutral mathematical derivation built on pinned Mathlib (Apache2.0). PBPS by Fan Chen, Sinho Chewi, Jianfeng Lu and Matthew S. Zhang motivates the two actual adapters; no numbered paper theorem is attributed to this generic premise bundle.

Complete source statement (Samplinglib restatement)

Let \(X\) be an arbitrary measurable space, \(\mu\) a finite measure (possibly zero), and \(\kappa\) a measurable Markov kernel with \(\mu\kappa=\mu\). There exists ONE continuous real-linear operator \(P:L^2(\mu)\to L^2(\mu)\), of norm at most one, such that for EVERY real \(f\) with \(f\in L^2(\mu)\), its kernel fibers are integrable for \(\mu\)-almost every \(x\) and \((P[f])(x)=\int f(z)\,\kappa(x,dz)\) almost everywhere. The operator preserves almost-everywhere order positivity, the constant-one class and the genuine integral of every L2 observable. IF \(\kappa\) is reversible for \(\mu\), this SAME operator is self-adjoint. No topology, separability, Standard-Borel or nonempty hypothesis is imposed. Exceptional sets may depend on f.

One operator, all representatives; optional self-adjointness

Read the formalized proofs

Each statement and proof below has its own closed Lean disclosure. Samplinglib parents, Mathlib calls and external mathematical sources are distinguished in each proof.

Samplinglib mathematical lesson

From an invariant Markov kernel to its genuine L2 observable operator

AutoSamplingTheory.TechnicalLemmas.Probability.KernelL2.invariant_kernel_l2_operator · theorem · Teaching coverage

Read this first

Mathematical statement

\[\begin{gathered}(Pf)(x)=\int f(z)\,\kappa(x,dz)\quad(\mu\text{-a.e.}),\qquad\|P\|_{2\to2}\le1,\\ P1=1,\quad f\ge0\Rightarrow Pf\ge0\ (\mu\text{-a.e.}),\quad\int Pf\,d\mu=\int f\,d\mu,\\ \kappa\text{ reversible}\ \Longrightarrow\ P^*=P.\end{gathered}\]

Lean statement · invariant_kernel_l2_operator

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 invariant_kernel_l2_operator {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ] (hκ : κ.Invariant μ) :
    invariant_kernel_l2_statement μ κ hκ

Exact module and namespace context

Full Lean proposition (definition) · invariant_kernel_l2_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 invariant_kernel_l2_statement {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ] (hκ : κ.Invariant μ) : Prop :=
    ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
      (∀ f : X → ℝ, ∀ hf : MemLp f 2 μ,
        (∀ᵐ x ∂μ, Integrable f (κ x)) ∧
        (A (hf.toLp f) : X → ℝ) =ᵐ[μ] fun x => ∫ z, f z ∂κ x) ∧
      (∀ f : Lp ℝ 2 μ, (∀ᵐ x ∂μ, 0 ≤ f x) → ∀ᵐ x ∂μ, 0 ≤ A f x) ∧
      A (Lp.const 2 μ (1 : ℝ)) = Lp.const 2 μ (1 : ℝ) ∧
      (∀ f : Lp ℝ 2 μ, (∫ x, A f x ∂μ) = ∫ x, f x ∂μ) ∧
      (κ.IsReversible μ → IsSelfAdjoint A)

Exact module and namespace context

Proof roadmap

1Construct the operator from two marginal pullbacks
Put nu(dx,dz)=mu(dx)kappa(x,dz). Markovness gives the first marginal mu, and invariance gives the second marginal mu. Pullback by the two coordinates therefore gives L2 isometries Bf(x,z)=f(x) and Cf(x,z)=f(z). Set P=B* C. Both pullbacks have norm at most one, including when the L2 space is trivial. The adjoint identity gives the pairing formula.
2Identify the raw conditional integral, not just an abstract operator
Fix ANY MemLp representative G. Its second-coordinate pullback is L2 and therefore L1 under the finite joint measure. Invariance and kernel Fubini give genuinely integrable fibers almost everywhere and an integrable conditional mean u(x). To prove P[G]=u, pair with the indicator of every measurable set s of finite measure. The adjoint pairing, representative transport along both marginals, and Fubini identify every set integral. Equality of integrable functions then yields AE equality.
3Derive order positivity and the fixed-one class
Apply the representation to an arbitrary L2 quotient representative. If f≥0 mu-AE, invariance transports this property to kappa(x)-AE for mu-AE x. Its integral is nonnegative, so Pf≥0 AE. For the literal constant representative 1, each probability fiber integrates to one; quotient extensionality proves P1=1.
4Preserve the genuine mean
For any L2 class f, its second-coordinate pullback is integrable under the finite joint law. Integrate the AE representation, use kernel Fubini, then push forward along the second marginal. Because that marginal is mu, the mean is unchanged.
5Use detailed balance only when self-adjointness is requested
Assume now that kappa is reversible. The joint law and its coordinate swap agree on every measurable rectangle by detailed balance. Both are finite, so rectangle uniqueness makes them equal as measures. Swap the two coordinates in the pairing formula to obtain a symmetric operator, hence a bounded self-adjoint operator.

Full assumptions and notation

All objects and hypotheses

Finite measure is a mathematical premise of this shared interface, not a hidden paper hypothesis. Finite mass need not equal one; it makes every L2 representative L1, so the mean equality is genuine. The zero target and empty carrier are allowed.
A kernel is genuinely measurable and every fiber is a probability measure. Its invariance is a premise here; an actual PBPS adapter must PRODUCE that premise from the verified actual process/kernel, never add invariance as a new paper-level assumption.
Lp is a quotient by mu-almost-everywhere equality. The theorem quantifies over every MemLp representative and concludes both AE fiber integrability and the AE kernel-integral formula. It asserts neither everywhere integrability nor an exceptional set uniform in all observables.
Order positivity means f≥0 AE implies Pf≥0 AE. It does not assert the Hilbert positive-semidefinite inequality <f,Pf>≥0. Mere invariance does not imply detailed balance or self-adjointness.
This is a standard source-neutral library theorem motivated by PBPS A.2/A.9 and B.1, not a claim that either paper section or the actual L2 adapter has been completed.

Mathematical proof

1. Construct the operator from two marginal pullbacks

Put nu(dx,dz)=mu(dx)kappa(x,dz). Markovness gives the first marginal mu, and invariance gives the second marginal mu. Pullback by the two coordinates therefore gives L2 isometries Bf(x,z)=f(x) and Cf(x,z)=f(z). Set P=B* C. Both pullbacks have norm at most one, including when the L2 space is trivial. The adjoint identity gives the pairing formula.

\[\begin{aligned}\nu^X=\nu^Z&=\mu,\quad P=B^*C,\quad\|P\|\le\|B\|\|C\|\le1,\\ \langle f,Pg\rangle&=\int f(x)g(z)\,\nu(dx,dz).\end{aligned}\]

Corresponding Lean step

private lemma pair_operator {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ] (κ : Kernel X X) [IsMarkovKernel κ]
    (hκ : κ.Invariant μ) :
    ∃ A : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 μ, ‖A‖ ≤ 1 ∧
      ∀ f g : Lp ℝ 2 μ,
        ⟪f, A g⟫_ℝ = ∫ p : X × X, f p.1 * g p.2 ∂(μ ⊗ₘ κ) := by
  let ν := μ ⊗ₘ κ
  have hfst : MeasurePreserving Prod.fst ν μ :=
    ⟨measurable_fst, Measure.fst_compProd μ κ⟩
  have hsnd : MeasurePreserving Prod.snd ν μ :=
    ⟨measurable_snd, (Measure.snd_compProd μ κ).trans hκ.def⟩
  let B : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 ν :=
    (Lp.compMeasurePreservingₗᵢ ℝ Prod.fst hfst).toContinuousLinearMap
  let C : Lp ℝ 2 μ →L[ℝ] Lp ℝ 2 ν :=
    (Lp.compMeasurePreservingₗᵢ ℝ Prod.snd hsnd).toContinuousLinearMap
  let A := B.adjoint.comp C
  have hB : ‖B‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
  have hC : ‖C‖ ≤ 1 := LinearIsometry.norm_toContinuousLinearMap_le _
  refine ⟨A, ?_, ?_⟩
  · calc
      ‖A‖ ≤ ‖B.adjoint‖ * ‖C‖ := ContinuousLinearMap.opNorm_comp_le _ _
      _ = ‖B‖ * ‖C‖ := by rw [ContinuousLinearMap.adjoint.norm_map]
      _ ≤ 1 * 1 := mul_le_mul hB hC (norm_nonneg _) zero_le_one
      _ = 1 := one_mul 1
  · intro f g
    change ⟪f, B.adjoint (C g)⟫_ℝ = _
    rw [ContinuousLinearMap.adjoint_inner_right, L2.inner_def]
    have hb := Lp.coeFn_compMeasurePreserving f hfst
    have hc := Lp.coeFn_compMeasurePreserving g hsnd
    apply integral_congr_ae
    filter_upwards [hb, hc] with p hp hq
    change B f p = f p.1 at hp
    change C g p = g p.2 at hq
    rw [hp, hq]
    simp [RCLike.inner_apply, mul_comm]

The proof adapts the existing private actual-process adjoint technology, but the new public interface has no actual-process or product-noise witness. This is an alternative standard realization, not paper-author proof topology.

2. Identify the raw conditional integral, not just an abstract operator

Fix ANY MemLp representative G. Its second-coordinate pullback is L2 and therefore L1 under the finite joint measure. Invariance and kernel Fubini give genuinely integrable fibers almost everywhere and an integrable conditional mean u(x). To prove P[G]=u, pair with the indicator of every measurable set s of finite measure. The adjoint pairing, representative transport along both marginals, and Fubini identify every set integral. Equality of integrable functions then yields AE equality.

\[\begin{aligned}\int_sP[G],d\mu&=\langle1_s,P[G]\rangle=\int1_s(x)G(z)\,d\nu\\ &=\int_s\left[\int G(z)\,\kappa(x,dz)\right]d\mu,\\ P[G]&=u\quad\mu\text{-a.e.}\end{aligned}\]

Corresponding Lean step

  have hrep : ∀ G : X → ℝ, ∀ hG : MemLp G 2 μ,
      (∀ᵐ x ∂μ, Integrable G (κ x)) ∧
      (A (hG.toLp G) : X → ℝ) =ᵐ[μ] fun x => ∫ z, G z ∂κ x := by
    intro G hG
    have hprod : Integrable (fun p : X × X => G p.2) ν :=
      (hG.comp_measurePreserving hsnd).integrable (by norm_num)
    have hc : Integrable G ((κ ∘ₖ Kernel.const Unit μ) ()) := by
      simpa only [Kernel.comp_const, Kernel.const_apply, hκ.def] using
        hG.integrable (by norm_num)
    have hop : Integrable (fun x => ∫ z, G z ∂κ x) μ := by
      simpa only [Kernel.const_apply] using hc.integral_comp
    have hAg : Integrable (A (hG.toLp G) : X → ℝ) μ :=
      (Lp.memLp _).integrable (by norm_num)
    refine ⟨Measure.ae_integrable_of_integrable_comp (by
      simpa only [hκ.def] using hG.integrable (by norm_num)), ?_⟩
    apply Integrable.ae_eq_of_forall_setIntegral_eq _ _ hAg hop
    intro s hs hms
    let i : Lp ℝ 2 μ := indicatorConstLp 2 hs hms.ne (1 : ℝ)
    have hi : (i : X → ℝ) =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) :=
      indicatorConstLp_coeFn
    have hi' := hfst.quasiMeasurePreserving.ae_eq hi
    have hg' := hsnd.quasiMeasurePreserving.ae_eq hG.coeFn_toLp
    let F : X × X → ℝ := fun p => s.indicator (fun _ => (1 : ℝ)) p.1 * G p.2
    have hF : Integrable F ν := by
      have he : F = (Prod.fst ⁻¹' s).indicator (fun p : X × X => G p.2) := by
        funext p
        by_cases hp : p.1 ∈ s <;> simp [F, Set.indicator, hp]
      rw [he]
      exact hprod.indicator (hs.preimage measurable_fst)
    calc
      (∫ x in s, A (hG.toLp G) x ∂μ) = ⟪i, A (hG.toLp G)⟫_ℝ :=
        (L2.inner_indicatorConstLp_one hs hms.ne _).symm
      _ = ∫ p : X × X, i p.1 * (hG.toLp G) p.2 ∂ν := hpair i (hG.toLp G)
      _ = ∫ p, F p ∂ν := by
        apply integral_congr_ae
        filter_upwards [hi', hg'] with p hp hq
        change i p.1 = s.indicator (fun _ => (1 : ℝ)) p.1 at hp
        change (hG.toLp G) p.2 = G p.2 at hq
        simp only [F, hp, hq]
      _ = ∫ x, ∫ z, F (x, z) ∂κ x ∂μ := Measure.integral_compProd hF
      _ = ∫ x, s.indicator (fun _ => (1 : ℝ)) x * (∫ z, G z ∂κ x) ∂μ := by
        simp only [F, integral_const_mul]
      _ = ∫ x in s, (∫ z, G z ∂κ x) ∂μ := by
        rw [← integral_indicator hs]
        congr 1
        funext x
        by_cases hx : x ∈ s <;> simp [Set.indicator, hx]

Indicator functions belong to L2 because mu is finite. The Fubini step has an explicit integrable indicator-weighted joint integrand. This proves the meaning of the totalized Lean integral on a full-measure set, rather than silently assuming integrability.

3. Derive order positivity and the fixed-one class

Apply the representation to an arbitrary L2 quotient representative. If f≥0 mu-AE, invariance transports this property to kappa(x)-AE for mu-AE x. Its integral is nonnegative, so Pf≥0 AE. For the literal constant representative 1, each probability fiber integrates to one; quotient extensionality proves P1=1.

\[\begin{aligned}f\ge0\ \mu\text{-a.e.}&\Longrightarrow f\ge0\ \kappa(x)\text{-a.e. for }\mu\text{-a.e. }x\\ &\Longrightarrow Pf\ge0\ \mu\text{-a.e.},\qquad P1(x)=\int1\,d\kappa(x)=1.\end{aligned}\]

Corresponding Lean step

  have hrepLp (f : Lp ℝ 2 μ) :
      (A f : X → ℝ) =ᵐ[μ] fun x => ∫ z, f z ∂κ x := by
    simpa only [Lp.toLp_coeFn] using (hrep f (Lp.memLp f)).2
  refine ⟨A, hA, hrep, ?_, ?_, ?_, ?_⟩
  · intro f hf
    have hp : ∀ᵐ x ∂μ, ∀ᵐ z ∂κ x, 0 ≤ f z :=
      Measure.ae_ae_of_ae_comp (by simpa only [hκ.def] using hf)
    filter_upwards [hrepLp f, hp] with x hx hp
    rw [hx]
    exact integral_nonneg_of_ae hp
  · have hc := (hrep (fun _ : X => (1 : ℝ)) (memLp_const (1 : ℝ))).2
    rw [MemLp.toLp_const] at hc
    apply Lp.ext
    filter_upwards [hc, Lp.coeFn_const (p := 2) (μ := μ) (c := (1 : ℝ))] with x hx h1
    calc
      A (Lp.const 2 μ (1 : ℝ)) x = 1 := by simpa [measureReal_def] using hx
      _ = Lp.const 2 μ (1 : ℝ) x := h1.symm

Null sets are transported by the exact invariant law; positivity is not concluded pointwise from a chosen quotient representative. Order positivity is different from positive-semidefinite Hilbert positivity.

4. Preserve the genuine mean

For any L2 class f, its second-coordinate pullback is integrable under the finite joint law. Integrate the AE representation, use kernel Fubini, then push forward along the second marginal. Because that marginal is mu, the mean is unchanged.

\[\int Pf\,d\mu=\int\!\int f(z)\,\kappa(x,dz)\,\mu(dx)=\int f(z)\,d\nu=\int f\,d\mu.\]

Corresponding Lean step

  · intro f
    have hprod : Integrable (fun p : X × X => f p.2) ν :=
      ((Lp.memLp f).comp_measurePreserving hsnd).integrable (by norm_num)
    calc
      (∫ x, A f x ∂μ) = ∫ x, ∫ z, f z ∂κ x ∂μ := integral_congr_ae (hrepLp f)
      _ = ∫ p : X × X, f p.2 ∂ν := (Measure.integral_compProd hprod).symm
      _ = ∫ x, f x ∂ν.map Prod.snd :=
        (integral_map_of_stronglyMeasurable measurable_snd (Lp.stronglyMeasurable f)).symm
      _ = ∫ x, f x ∂μ := by rw [hsnd.map_eq]

All these real integrals are genuine L1 integrals. In particular, the argument is not relying on the totalized convention that an undefined Bochner integral equals zero.

5. Use detailed balance only when self-adjointness is requested

Assume now that kappa is reversible. The joint law and its coordinate swap agree on every measurable rectangle by detailed balance. Both are finite, so rectangle uniqueness makes them equal as measures. Swap the two coordinates in the pairing formula to obtain a symmetric operator, hence a bounded self-adjoint operator.

\[\begin{aligned}\nu(A\times B)&=\int_A\kappa(x,B)\,d\mu=\int_B\kappa(x,A)\,d\mu=\nu(B\times A),\\ \langle Pf,g\rangle&=\int g(x)f(z)\,d\nu=\int f(x)g(z)\,d\nu=\langle f,Pg\rangle.\end{aligned}\]

Corresponding Lean step

  · intro hrev
    have hswap : ν.map Prod.swap = ν := by
      apply Measure.ext_prod
      intro s t hs ht
      rw [Measure.map_apply measurable_swap (hs.prod ht)]
      have he : Prod.swap ⁻¹' (s ×ˢ t) = t ×ˢ s := by ext p; simp [and_comm]
      rw [he, Measure.compProd_apply_prod ht hs, Measure.compProd_apply_prod hs ht]
      exact hrev ht hs
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro f g
    calc
      ⟪A f, g⟫_ℝ = ⟪g, A f⟫_ℝ := real_inner_comm _ _
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν := hpair g f
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν.map Prod.swap := by rw [hswap]
      _ = ∫ p : X × X, g p.2 * f p.1 ∂ν := by
        have hm : StronglyMeasurable (fun p : X × X => g p.1 * f p.2) :=
          ((Lp.stronglyMeasurable g).comp_measurable measurable_fst).mul
            ((Lp.stronglyMeasurable f).comp_measurable measurable_snd)
        exact integral_map_of_stronglyMeasurable measurable_swap hm
      _ = ∫ p : X × X, f p.1 * g p.2 ∂ν := by simp only [mul_comm]
      _ = ⟪f, A g⟫_ℝ := (hpair f g).symm

Finite-measure rectangle uniqueness works on arbitrary measurable spaces; no countably generated or Standard-Borel premise is introduced. The actual full PBPS one-step kernel is NOT assumed reversible.

Lean verification

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

Lean proof · invariant_kernel_l2_operator

Finite invariant joint marginals -> pullback adjoint -> integrable indicator pairings -> order/one/mean -> conditional reversible swap symmetry.

Download module (.lean)

theorem invariant_kernel_l2_operator {X : Type*} [MeasurableSpace X]
    (μ : Measure X) [IsFiniteMeasure μ]
    (κ : Kernel X X) [IsMarkovKernel κ] (hκ : κ.Invariant μ) :
    invariant_kernel_l2_statement μ κ hκ := by
  classical
  obtain ⟨A, hA, hpair⟩ := pair_operator μ κ hκ
  let ν := μ ⊗ₘ κ
  have hfst : MeasurePreserving Prod.fst ν μ :=
    ⟨measurable_fst, Measure.fst_compProd μ κ⟩
  have hsnd : MeasurePreserving Prod.snd ν μ :=
    ⟨measurable_snd, (Measure.snd_compProd μ κ).trans hκ.def⟩
  have hrep : ∀ G : X → ℝ, ∀ hG : MemLp G 2 μ,
      (∀ᵐ x ∂μ, Integrable G (κ x)) ∧
      (A (hG.toLp G) : X → ℝ) =ᵐ[μ] fun x => ∫ z, G z ∂κ x := by
    intro G hG
    have hprod : Integrable (fun p : X × X => G p.2) ν :=
      (hG.comp_measurePreserving hsnd).integrable (by norm_num)
    have hc : Integrable G ((κ ∘ₖ Kernel.const Unit μ) ()) := by
      simpa only [Kernel.comp_const, Kernel.const_apply, hκ.def] using
        hG.integrable (by norm_num)
    have hop : Integrable (fun x => ∫ z, G z ∂κ x) μ := by
      simpa only [Kernel.const_apply] using hc.integral_comp
    have hAg : Integrable (A (hG.toLp G) : X → ℝ) μ :=
      (Lp.memLp _).integrable (by norm_num)
    refine ⟨Measure.ae_integrable_of_integrable_comp (by
      simpa only [hκ.def] using hG.integrable (by norm_num)), ?_⟩
    apply Integrable.ae_eq_of_forall_setIntegral_eq _ _ hAg hop
    intro s hs hms
    let i : Lp ℝ 2 μ := indicatorConstLp 2 hs hms.ne (1 : ℝ)
    have hi : (i : X → ℝ) =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) :=
      indicatorConstLp_coeFn
    have hi' := hfst.quasiMeasurePreserving.ae_eq hi
    have hg' := hsnd.quasiMeasurePreserving.ae_eq hG.coeFn_toLp
    let F : X × X → ℝ := fun p => s.indicator (fun _ => (1 : ℝ)) p.1 * G p.2
    have hF : Integrable F ν := by
      have he : F = (Prod.fst ⁻¹' s).indicator (fun p : X × X => G p.2) := by
        funext p
        by_cases hp : p.1 ∈ s <;> simp [F, Set.indicator, hp]
      rw [he]
      exact hprod.indicator (hs.preimage measurable_fst)
    calc
      (∫ x in s, A (hG.toLp G) x ∂μ) = ⟪i, A (hG.toLp G)⟫_ℝ :=
        (L2.inner_indicatorConstLp_one hs hms.ne _).symm
      _ = ∫ p : X × X, i p.1 * (hG.toLp G) p.2 ∂ν := hpair i (hG.toLp G)
      _ = ∫ p, F p ∂ν := by
        apply integral_congr_ae
        filter_upwards [hi', hg'] with p hp hq
        change i p.1 = s.indicator (fun _ => (1 : ℝ)) p.1 at hp
        change (hG.toLp G) p.2 = G p.2 at hq
        simp only [F, hp, hq]
      _ = ∫ x, ∫ z, F (x, z) ∂κ x ∂μ := Measure.integral_compProd hF
      _ = ∫ x, s.indicator (fun _ => (1 : ℝ)) x * (∫ z, G z ∂κ x) ∂μ := by
        simp only [F, integral_const_mul]
      _ = ∫ x in s, (∫ z, G z ∂κ x) ∂μ := by
        rw [← integral_indicator hs]
        congr 1
        funext x
        by_cases hx : x ∈ s <;> simp [Set.indicator, hx]
  have hrepLp (f : Lp ℝ 2 μ) :
      (A f : X → ℝ) =ᵐ[μ] fun x => ∫ z, f z ∂κ x := by
    simpa only [Lp.toLp_coeFn] using (hrep f (Lp.memLp f)).2
  refine ⟨A, hA, hrep, ?_, ?_, ?_, ?_⟩
  · intro f hf
    have hp : ∀ᵐ x ∂μ, ∀ᵐ z ∂κ x, 0 ≤ f z :=
      Measure.ae_ae_of_ae_comp (by simpa only [hκ.def] using hf)
    filter_upwards [hrepLp f, hp] with x hx hp
    rw [hx]
    exact integral_nonneg_of_ae hp
  · have hc := (hrep (fun _ : X => (1 : ℝ)) (memLp_const (1 : ℝ))).2
    rw [MemLp.toLp_const] at hc
    apply Lp.ext
    filter_upwards [hc, Lp.coeFn_const (p := 2) (μ := μ) (c := (1 : ℝ))] with x hx h1
    calc
      A (Lp.const 2 μ (1 : ℝ)) x = 1 := by simpa [measureReal_def] using hx
      _ = Lp.const 2 μ (1 : ℝ) x := h1.symm
  · intro f
    have hprod : Integrable (fun p : X × X => f p.2) ν :=
      ((Lp.memLp f).comp_measurePreserving hsnd).integrable (by norm_num)
    calc
      (∫ x, A f x ∂μ) = ∫ x, ∫ z, f z ∂κ x ∂μ := integral_congr_ae (hrepLp f)
      _ = ∫ p : X × X, f p.2 ∂ν := (Measure.integral_compProd hprod).symm
      _ = ∫ x, f x ∂ν.map Prod.snd :=
        (integral_map_of_stronglyMeasurable measurable_snd (Lp.stronglyMeasurable f)).symm
      _ = ∫ x, f x ∂μ := by rw [hsnd.map_eq]
  · intro hrev
    have hswap : ν.map Prod.swap = ν := by
      apply Measure.ext_prod
      intro s t hs ht
      rw [Measure.map_apply measurable_swap (hs.prod ht)]
      have he : Prod.swap ⁻¹' (s ×ˢ t) = t ×ˢ s := by ext p; simp [and_comm]
      rw [he, Measure.compProd_apply_prod ht hs, Measure.compProd_apply_prod hs ht]
      exact hrev ht hs
    apply ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric.mpr
    intro f g
    calc
      ⟪A f, g⟫_ℝ = ⟪g, A f⟫_ℝ := real_inner_comm _ _
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν := hpair g f
      _ = ∫ p : X × X, g p.1 * f p.2 ∂ν.map Prod.swap := by rw [hswap]
      _ = ∫ p : X × X, g p.2 * f p.1 ∂ν := by
        have hm : StronglyMeasurable (fun p : X × X => g p.1 * f p.2) :=
          ((Lp.stronglyMeasurable g).comp_measurable measurable_fst).mul
            ((Lp.stronglyMeasurable f).comp_measurable measurable_snd)
        exact integral_map_of_stronglyMeasurable measurable_swap hm
      _ = ∫ p : X × X, f p.1 * g p.2 ∂ν := by simp only [mul_comm]
      _ = ⟪f, A g⟫_ℝ := (hpair f g).symm

end
end AutoSamplingTheory.TechnicalLemmas.Probability.KernelL2

Exact module and namespace context

Source assumptions versus formal assumptions

Source	Actual Lean	Difference kind	Why it matters
Source-neutral finite invariant Markov-kernel interface; no numbered paper theorem is claimed.	Arbitrary measurable X; finite mu; Markov kappa; exact kappa.Invariant mu.	same	These are precisely the mathematical premises of this shared theorem; they must be discharged by real paper adapters.
An integral formula should define one operator on L2 equivalence classes.	AE fiber integrability and equality for every MemLp representative; fixed one, preserved mean, and self-adjointness only IF reversible.	source-implicit	Finiteness, invariant null-set transport, kernel Fubini and rectangle uniqueness establish the hidden quotient obligations, without adding representative or integrability hypotheses.
Actual paper operator and quantitative convergence.	One standard shared operator bridge only; no process Markov/restart/semigroup, density-forward identity, rate, cap/error/expected cost, warm start/composition or full paper. It will be published as a shared prerequisite, not as completion of A.2/B.1.	unresolved	This library node does not itself supply actual kernel producers, an iterate estimate, density-forward identity or expected cost.

One standard shared operator bridge only; no process Markov/restart/semigroup, density-forward identity, rate, cap/error/expected cost, warm start/composition or full paper. It will be published as a shared prerequisite, not as completion of A.2/B.1.

Encoder–denoiser: accepted · equivalent-after-elaboration

A generalization is not a source correction. Proposed missing conditions require separate independent repair review. No proposed repair silently changes the original theorem.

Scope and omitted-condition boundaries

One standard shared operator bridge only; no process Markov/restart/semigroup, density-forward identity, rate, cap/error/expected cost, warm start/composition or full paper. It will be published as a shared prerequisite, not as completion of A.2/B.1.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

MeasureTheory.Measure.fst_compProd
MeasureTheory.Measure.snd_compProd
MeasureTheory.Lp.compMeasurePreservingₗᵢ
ContinuousLinearMap.adjoint_inner_right
MeasureTheory.Integrable.ae_eq_of_forall_setIntegral_eq
MeasureTheory.Measure.ae_integrable_of_integrable_comp
MeasureTheory.Measure.integral_compProd
MeasureTheory.Measure.ext_prod
ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric

Mathematical sources

Pinned Mathlib invariant-kernel and compProd definitions; standard derived L2 theorem — One standard shared operator bridge only; no process Markov/restart/semigroup, density-forward identity, rate, cap/error/expected cost, warm start/composition or full paper. It will be published as a shared prerequisite, not as completion of A.2/B.1.
PBPS A.2/A.9 and B.1: motivating consumers only — Actual operator adapters remain red.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

From an invariant Markov kernel to its genuine L2 observable operator

Complete source statement (Samplinglib restatement)

One operator, all representatives; optional self-adjointness

Read the formalized proofs

From an invariant Markov kernel to its genuine L2 observable operator

Mathematical statement

Proof roadmap

All objects and hypotheses

Mathematical proof

1. Construct the operator from two marginal pullbacks

2. Identify the raw conditional integral, not just an abstract operator

3. Derive order positivity and the fixed-one class

4. Preserve the genuine mean

5. Use detailed balance only when self-adjointness is requested

Lean verification

Source assumptions versus formal assumptions

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

Mathematical sources

Which proof obligations and prerequisites are covered?