AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO

- Construct measurable state-dependent target, Gaussian observation and retained-state posterior kernels, with exact recovery of every ideal joint state-target law. This supplies kernel semantics for an RGO stage, not an approximate sampler or its costs.

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
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StateDependentRGO.lean:31published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.