AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel

- The normalized quadratic tilt is a measurable Markov kernel and a backward conditional law of the actual Gaussian augmentation, for every positive noise variance. The input law may be singular and need not have any finite moments.

theorem exists_tilted_isCondKernel (μ : Measure E) [IsProbabilityMeasure μ]
    {η : ℝ} (hη : 0 < η) :
    let J := Measure.map
      (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    ∃ R : Kernel E E, IsMarkovKernel R ∧
      (∀ y, R y = μ.tilted (fun x => -‖x - y‖ ^ 2 / (2 * η))) ∧
      (J.map Prod.swap).IsCondKernel R := by
  classical
  let J := Measure.map
    (fun p : E × E => (p.1, p.1 + Real.sqrt η • p.2))
    (μ.prod (stdGaussian E))
  let w : E → E → ℝ := fun y x => Real.exp (-‖x - y‖ ^ 2 / (2 * η))
  let Z : E → ℝ := fun y => ∫ x, w y x ∂μ
  have hw : Measurable (Function.uncurry w) := by fun_prop
  have hI (y : E) : Integrable (w y) μ := 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
      (div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) (by positivity))
  have hZpos (y : E) : 0 < Z y := integral_exp_pos (hI y)
  have hZ : Measurable Z := hw.stronglyMeasurable.integral_prod_right.measurable
  let d : E → E → ℝ≥0∞ := fun y x => ENNReal.ofReal (w y x / Z y)
  have hd : Measurable (Function.uncurry d) :=
    (hw.div (hZ.comp measurable_fst)).ennreal_ofReal
  let R : Kernel E E := (Kernel.const E μ).withDensity d
  have hRfiber (y : E) : R y = μ.tilted (fun x => -‖x - y‖ ^ 2 / (2 * η)) := by
    rw [show R = (Kernel.const E μ).withDensity d from rfl,
      Kernel.withDensity_apply _ hd]
    rfl
  have hR : IsMarkovKernel R := ⟨fun y => by
    rw [hRfiber]
    exact isProbabilityMeasure_tilted (hI y)⟩
  let C : ℝ := ((Real.sqrt (2 * Real.pi * η))⁻¹) ^ Module.finrank ℝ E
  have hC : 0 ≤ C := by positivity
  let a : E → ℝ≥0∞ := fun y => ENNReal.ofReal (C * Z y)
  have ha : Measurable a := (measurable_const.mul hZ).ennreal_ofReal
  let ν : Measure E := volume.withDensity a
  have hJ : J.map Prod.swap = (volume.prod μ).withDensity
      (fun p : E × E => ENNReal.ofReal (C * w p.1 p.2)) := by
    dsimp only [J]
    rw [ExampleCases.ProximalBPS.GaussianAugmentation.augmentation_eq_withDensity μ η hη]
    change ((μ.prod volume).withDensity _).map
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/Probability/GaussianConditionalKernel.lean:35published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.