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.
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.
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.
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.
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.
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.
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) = ν ⊗ₘ TLean 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.
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 := 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.StateDependentRGOScope 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
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosure.quadratic_tilt_tiltAutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward.rgo_backward_recovery
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.