ASTIS mathematical exposition

Joint posterior recovery with measurable state-dependent RGO parameters

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO.state_dependent_recovery · theorem · Teaching coverage

Statement

Let E be a finite-dimensional real inner-product Borel space, S any measurable space, and mu a probability measure on E. Let b,a:S to R and u:S to E be measurable, with b(s)>=0 and a(s)>0 everywhere. There exist Markov kernels T,H:S to E and B:S times E to S times E, chosen before every probability state law nu. Every T(s) is the normalized mu tilt by -b(s)*norm(x-u(s))^2/2; H(s) is its actual Gaussian smoothing at standard deviation sqrt(a(s)). Every B(s,y) retains s and draws x from the actual backward tilt of T(s) by -norm(x-y)^2/(2a(s)). Equivalently, it uses the original mu tilt with precision b(s)+1/a(s) and center (b(s)*u(s)+y/a(s))/(b(s)+1/a(s)). For every probability nu, B composed with nu compProd H equals nu compProd T.

\[B\circ_m(\nu\otimes_m H)=\nu\otimes_m T,\qquad T(s)=\mu.\mathrm{tilted}\!\left(-\frac{b(s)}2\|x-u(s)\|^2\right).\]

All objects and hypotheses

E is a finite-dimensional real inner-product space with its Borel measurable structure, including dimension zero; mu is an arbitrary probability measure.
S has only a measurable-space structure. No topology, standard Borel condition, or moment condition on the state law is needed.
b,a,u are measurable on S, with b nonnegative and a strictly positive at every state. No fixed or deterministic schedule is imposed.
All global kernels precede the universally quantified probability state law. Both posterior formulas hold at every state and observation.
Recovery assumes the actual ideal input nu compProd H. State may encode past history and its parameters are fixed conditional on the current call input. This does not assume one predetermined schedule for all calls or construct the actual approximate sampler.

Mathematical proof

1. Normalize a jointly measurable quadratic weight

On the parameter space of nonnegative precision and center, the quadratic exponential weight is jointly measurable, strictly positive and at most one. Its integral against the probability base is therefore finite and strictly positive. The parameter integral is measurable. Divide by this integral to construct one global Markov kernel through withDensity, including zero precision.

\[w_{q,v}(x)=e^{-q\|x-v\|^2/2},\quad 0<Z(q,v)=\int w_{q,v}\,d\mu\le1,\quad R(q,v)=\frac{w_{q,v}}{Z(q,v)}\mu.\]

Corresponding Lean step

Local universalTilt: integrable_const domination, integral_exp_pos, StronglyMeasurable.integral_prod_right, Kernel.withDensity, isProbabilityMeasure_tilted.

2. Use measurable current and updated parameters

Compose the same global parameter kernel with the current-state map to obtain T and with the updated state-observation map to obtain K. The new precision is positive and the weighted center is measurable. This proves joint measurability; separate existential kernels for each parameter would not suffice.

\[q^+(s)=b(s)+a(s)^{-1}>0,\quad c(s,y)=q^+(s)^{-1}\bigl(b(s)u(s)+a(s)^{-1}y\bigr),\quad K(s,y)=R(q^+(s),c(s,y)).\]

Corresponding Lean step

Measurable.subtype_mk, Measurable.prodMk, Kernel.comap; local t,q,c,r and hKupdated.

3. Construct the state-dependent Gaussian observation

Retain the input state and draw an independent standard Gaussian. Map this pair to sqrt(a(s)) times the Gaussian to form N. The product of T and N followed by addition defines H. Product and pushforward formulas establish the exact smoothing fiber and Markov property.

\[N(s)=\operatorname{Law}(\sqrt{a(s)}G),\qquad H(s)=\operatorname{Law}(X+\sqrt{a(s)}G),\quad X\sim T(s),\ G\sim\mathsf N(0,I)\text{ independently}.\]

Corresponding Lean step

Kernel.deterministic, Kernel.const, Kernel.prod, Kernel.map, Kernel.IsMarkovKernel.map; Measure.dirac_prod and Measure.map_map.

4. Identify the actual posterior and retain the state

Quadratic tilt closure identifies K with the backward tilt of T for every state and observation. Pair K with the deterministic state coordinate to form B. The already constructed section K(s,.) is identified with the existing pointwise recovery theorem; no measurable choice over pointwise witnesses is used.

\[K(s,y)=T(s).\mathrm{tilted}\!\left(-\frac{\|x-y\|^2}{2a(s)}\right),\quad B(s,y)=(x\mapsto(s,x))_\#K(s,y),\quad K(s,\cdot)\circ_mH(s)=T(s).\]

Corresponding Lean step

RGOClosure.quadratic_tilt_tilt, RGOBackward.rgo_backward_recovery; local hKf,hBf,hrec and kernel extensionality.

5. Recover the complete joint state-target law

For each measurable event in S times E, take its measurable section at a fixed state. The bind and compProd identities give the output event mass as an iterated nonnegative integral. Section recovery replaces the inner integral by T(s) of the section, yielding nu compProd T. No state coordinate or dependence is discarded.

\[\int_S\!\int_E B(s,y)(A)\,H(s)(dy)\,\nu(ds)=\int_S T(s)(A_s)\,\nu(ds).\]

Corresponding Lean step

Measure.bind_apply, Measure.lintegral_compProd, Measure.compProd_apply, Measure.map_apply, lintegral_congr.

Lean statement · state_dependent_recovery

Globally measurable state-dependent RGO target, Gaussian observation and retained-state posterior with actual joint recovery.

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 state_dependent_recovery (μ : Measure E) [IsProbabilityMeasure μ]
    (b a : S → ℝ) (u : S → E) (hb : Measurable b) (ha : Measurable a)
    (hu : Measurable u) (hb0 : ∀ s, 0 ≤ b s) (ha0 : ∀ s, 0 < a s) :
    ∃ (T H : Kernel S E) (B : Kernel (S × E) (S × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ s, T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2)) ∧
      (∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        ((T s).tilted (fun x => -‖x-y‖^2/(2*a s)))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        (μ.tilted (fun x => -((b s+(a s)⁻¹)/2)*
          ‖x-(b s+(a s)⁻¹)⁻¹ • (b s • u s+(a s)⁻¹ • y)‖^2))) ∧
      ∀ (ν : Measure S), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T

Exact module and namespace context

Lean proof · state_dependent_recovery

Construct a normalized parameter kernel, comap along measurable current and updated states, construct actual variable Gaussian noise, identify posterior fibers and integrate section recovery.

theorem state_dependent_recovery (μ : Measure E) [IsProbabilityMeasure μ]
    (b a : S → ℝ) (u : S → E) (hb : Measurable b) (ha : Measurable a)
    (hu : Measurable u) (hb0 : ∀ s, 0 ≤ b s) (ha0 : ∀ s, 0 < a s) :
    ∃ (T H : Kernel S E) (B : Kernel (S × E) (S × E)),
      IsMarkovKernel T ∧ IsMarkovKernel H ∧ IsMarkovKernel B ∧
      (∀ s, T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2)) ∧
      (∀ s, H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        ((T s).tilted (fun x => -‖x-y‖^2/(2*a s)))) ∧
      (∀ s y, B (s,y) = Measure.map (Prod.mk s)
        (μ.tilted (fun x => -((b s+(a s)⁻¹)/2)*
          ‖x-(b s+(a s)⁻¹)⁻¹ • (b s • u s+(a s)⁻¹ • y)‖^2))) ∧
      ∀ (ν : Measure S), IsProbabilityMeasure ν → B ∘ₘ (ν ⊗ₘ H) = ν ⊗ₘ T := by
  have universalTilt : ∃ R : Kernel (ℝ≥0 × E) E, IsMarkovKernel R ∧
      ∀ s, R s = μ.tilted (fun x => -((s.1 : ℝ)/2)*‖x-s.2‖^2) := by
    let w : (ℝ≥0 × E) → E → ℝ := fun s x => Real.exp (-((s.1 : ℝ) / 2) * ‖x-s.2‖^2)
    have hw : Measurable (Function.uncurry w) := by
      dsimp [w, Function.uncurry]
      fun_prop
    have hI (s : (ℝ≥0 × E)) : Integrable (w s) μ := by
      refine (integrable_const (1 : ℝ)).mono' (by fun_prop) ?_
      filter_upwards with x
      rw [Real.norm_eq_abs, abs_of_pos (Real.exp_pos _)]
      exact Real.exp_le_one_iff.mpr (mul_nonpos_of_nonpos_of_nonneg
        (neg_nonpos.mpr (div_nonneg s.1.coe_nonneg (by positivity))) (sq_nonneg _))
    let Z : (ℝ≥0 × E) → ℝ := fun s => ∫ x, w s x ∂μ
    have hZpos (s : (ℝ≥0 × E)) : 0 < Z s := integral_exp_pos (hI s)
    have hZ : Measurable Z := hw.stronglyMeasurable.integral_prod_right.measurable
    let d : (ℝ≥0 × E) → E → ℝ≥0∞ := fun s x => ENNReal.ofReal (w s x / Z s)
    have hd : Measurable (Function.uncurry d) :=
      (hw.div (hZ.comp measurable_fst)).ennreal_ofReal
    let T : Kernel (ℝ≥0 × E) E := (Kernel.const (ℝ≥0 × E) μ).withDensity d
    have hf (s : (ℝ≥0 × E)) : T s = μ.tilted (fun x => -((s.1 : ℝ) / 2) * ‖x-s.2‖^2) := by
      rw [show T = (Kernel.const (ℝ≥0 × E) μ).withDensity d from rfl,
        Kernel.withDensity_apply _ hd]
      rfl
    refine ⟨T, ⟨fun s => ?_⟩, hf⟩
    rw [hf]
    exact isProbabilityMeasure_tilted (hI s)
  obtain ⟨R,hR,hRf⟩ := universalTilt
  let := hR
  let t : S → ℝ≥0 × E := fun s => (⟨b s, hb0 s⟩, u s)
  have ht : Measurable t := (hb.subtype_mk).prodMk hu
  let T := R.comap t ht
  have hT : IsMarkovKernel T := inferInstance
  have hTf (s : S) : T s = μ.tilted (fun x => -(b s/2)*‖x-u s‖^2) := hRf (t s)
  let := hT
  let q : S × E → ℝ := fun p => b p.1 + (a p.1)⁻¹
  let c : S × E → E := fun p => (b p.1+(a p.1)⁻¹)⁻¹ •
    (b p.1 • u p.1+(a p.1)⁻¹ • p.2)
  have hq : Measurable q := by dsimp [q]; fun_prop
  have hc : Measurable c := by dsimp [c]; fun_prop
  have hq0 (p : S × E) : 0 ≤ q p :=
    le_of_lt (add_pos_of_nonneg_of_pos (hb0 p.1) (inv_pos.mpr (ha0 p.1)))
  let r : S × E → ℝ≥0 × E := fun p => (⟨q p, hq0 p⟩, c p)
  have hr : Measurable r := (hq.subtype_mk).prodMk hc
  let K := R.comap r hr
  have hK : IsMarkovKernel K := inferInstance
  have hKupdated (p : S × E) : K p = μ.tilted (fun x => -(q p/2)*‖x-c p‖^2) := hRf (r p)
  let := hK
  let N : Kernel S E :=
    ((Kernel.deterministic (id : S → S) measurable_id) ×ₖ Kernel.const S (stdGaussian E)).map
      (fun p : S × E => Real.sqrt (a p.1) • p.2)
  have hN : IsMarkovKernel N := by
    dsimp only [N]
    exact Kernel.IsMarkovKernel.map _ (by fun_prop)
  let := hN
  have hNf (s : S) : N s = GaussianSmoothing.scaledStdGaussian (E := E) (Real.sqrt (a s)) := by
    dsimp only [N]
    rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, Kernel.deterministic_apply,
      Kernel.const_apply, Measure.dirac_prod, Measure.map_map (by fun_prop) (by fun_prop)]
    rfl
  let H := (T ×ₖ N).map (fun p : E × E => p.1+p.2)
  have hH : IsMarkovKernel H := by
    dsimp only [H]
    exact Kernel.IsMarkovKernel.map _ (by fun_prop)
  let := hH
  have hHf (s : S) : H s = GaussianSmoothing.gaussianSmoothing (T s) (Real.sqrt (a s)) := by
    dsimp only [H]
    rw [Kernel.map_apply _ (by fun_prop), Kernel.prod_apply, hNf]
    rfl
  have hKf (s : S) (y : E) : K (s,y) =
      (T s).tilted (fun x => -‖x-y‖^2/(2*a s)) := by
    rw [hKupdated,hTf]
    have heq : (fun x : E => -‖x-y‖^2/(2*a s)) =
        (fun x => -((a s)⁻¹/2)*‖x-y‖^2) := by
      funext x
      field_simp
    rw [heq]
    exact (RGOClosure.quadratic_tilt_tilt μ (hb0 s) (inv_pos.mpr (ha0 s)) (u s) y).symm
  let B := (Kernel.deterministic (Prod.fst : S × E → S) measurable_fst) ×ₖ K
  have hB : IsMarkovKernel B := inferInstance
  let := hB
  have hBf (s : S) (y : E) : B (s,y) = Measure.map (Prod.mk s) (K (s,y)) := by
    dsimp only [B]
    rw [Kernel.prod_apply, Kernel.deterministic_apply, Measure.dirac_prod]
  have hrec (s : S) : (K.comap (Prod.mk s) measurable_prodMk_left) ∘ₘ H s = T s := by
    obtain ⟨_,R,hR,hRf,_,hrecover,_⟩ :=
      RGOBackward.rgo_backward_recovery μ (b s) (a s) (hb0 s) (ha0 s) (u s)
    have heq : K.comap (Prod.mk s) measurable_prodMk_left = R := by
      ext y : 1
      change K (s,y) = R y
      rw [hKf,hTf,hRf]
    rw [heq,hHf,hTf]
    exact hrecover
  refine ⟨T,H,B,hT,hH,hB,hTf,hHf,?_,?_,?_⟩
  · intro s y
    rw [hBf,hKf]
  · intro s y
    rw [hBf,hKupdated]
  · intro ν hν
    let := hν
    ext t ht
    rw [Measure.bind_apply ht B.aemeasurable, Measure.lintegral_compProd (B.measurable_coe ht),
      Measure.compProd_apply ht]
    apply lintegral_congr
    intro s
    have ht' := ht.preimage (measurable_prodMk_left (x := s))
    have heq := congrArg (fun m : Measure E => m ((Prod.mk s) ⁻¹' t)) (hrec s)
    rw [Measure.bind_apply ht' (K.comap (Prod.mk s) measurable_prodMk_left).aemeasurable] at heq
    rw [← heq]
    apply lintegral_congr
    intro y
    rw [hBf,Measure.map_apply measurable_prodMk_left ht]
    rfl

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO

Exact module and namespace context

Scope and omitted-condition boundaries

Fixed probability base, arbitrary measurable state space and measurable current-state parameters. Exact ideal joint observation law only. The source interface selects a smoothing level for each fixed call input; this theorem does not construct its actual output sampler, recursive stopping, FORS, numerical accuracy or expected query costs.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_exp_pos
MeasureTheory.isProbabilityMeasure_tilted
ProbabilityTheory.Kernel.withDensity
ProbabilityTheory.Kernel.comap
ProbabilityTheory.Kernel.prod
ProbabilityTheory.Kernel.map
MeasureTheory.Measure.lintegral_compProd
MeasureTheory.Measure.bind_apply

Mathematical sources

SPHMC v1 Algorithm 3.3 and Theorem 6.5 — Expanded ideal stage semantics with measurable state-dependent parameters; not the full recursive algorithm.

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