AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore

- The reflected actual backward Gaussian conditional kernel has the stated normalized density, and expectations of smooth compactly supported tests have the centered score derivative. Normalization and domination are consequences of the genuine Hessian bounds. Only positive eta is needed for this edge.

theorem reflected_conditional_covariance {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} {η : ℝ}
    (hα : 0 < (α : ℝ)) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E,
      (α : ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ V) x v) v ∧
      (fderiv ℝ (fderiv ℝ V) x v) v ≤ (β : ℝ)*‖v‖^2) (hη : 0 < η) :
    let μ := (volume : Measure E).tilted (fun x => -V x)
    let J := Measure.map (fun p : E × E => (p.1,p.1+Real.sqrt η • p.2))
      (μ.prod (stdGaussian E))
    let s := fun y u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
      (1/(4*η)) • innerSL ℝ (y-u)
    ∃ R S : Kernel E E, IsMarkovKernel R ∧ IsMarkovKernel S ∧
      (J.map Prod.swap).IsCondKernel R ∧
      (∀ y, S y = (R y).map (fun x => (2:ℝ) • x-y)) ∧
      (∀ y, S y = (volume : Measure E).tilted
        (fun u => -V ((1/2:ℝ) • (y+u)) - ‖y-u‖^2/(8*η))) ∧
      ∀ (f : E → ℝ), ContDiff ℝ ∞ f → HasCompactSupport f →
        ∀ y, Integrable (s y) (S y) ∧ Integrable (fun u => f u • s y u) (S y) ∧
          HasFDerivAt (fun z => ∫ u, f u ∂S z)
            ((∫ u, f u • s y u ∂S y) -
              (∫ u, f u ∂S y) • (∫ u, s y u ∂S y)) y := by
  have map_tilt {E F : Type u} [MeasurableSpace E] [MeasurableSpace F]
      (μ : Measure E) (e : E ≃ᵐ F) (f : E → ℝ) (hf : Measurable f) :
      (μ.tilted f).map e = (μ.map e).tilted (f ∘ e.symm) := by
    unfold Measure.tilted
    rw [AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodym.measurableEquiv_map_withDensity e _ (by fun_prop)]
    congr 1
    funext y
    have hi : (∫ y, Real.exp (f (e.symm y)) ∂(μ.map e)) = ∫ x, Real.exp (f x) ∂μ := by
      rw [integral_map_equiv e]
      simp only [e.symm_apply_apply]
    simp only [Function.comp_apply, hi]

  have smul_tilt {E : Type u} [MeasurableSpace E] (μ : Measure E) (f : E → ℝ)
      (hf : Measurable f) {c : ℝ} (hc : 0 < c) :
      (ENNReal.ofReal c • μ).tilted f = μ.tilted f := by
    unfold Measure.tilted
    rw [integral_smul_measure, ENNReal.toReal_ofReal hc.le, smul_eq_mul,
      withDensity_smul_measure, ← withDensity_smul _ (by fun_prop)]
    congr 1
    funext x
    simp only [Pi.smul_apply, smul_eq_mul]
    rw [← ENNReal.ofReal_mul hc.le]
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalScore.lean:36published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.