AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain

- The actual reflected conditional law has the source curvature and sharp score derivative bound, with directional scores in L2 and the stated finite variance/gradient-energy domain. No Poincare inequality is assumed or proved.

theorem conditional_curvature_and_score_domain {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : NNReal} {η : ℝ}
    (hα : 0 < (α:ℝ)) (hαβ : α ≤ β) (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 < η) (hβη : (β:ℝ)*η ≤ 1) :
    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 W := fun y u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
    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 => -W y u) ∧
        ContDiff ℝ 2 (W y) ∧ ContDiff ℝ 1 (s y) ∧
        (∀ u v w,
          (fderiv ℝ (fderiv ℝ (W y)) u v) w =
            (1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w + (1/(4*η))*inner ℝ v w ∧
          (fderiv ℝ (s y) u v) w = (1/(4*η))*inner ℝ v w -
            (1/4:ℝ)*(fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w) ∧
        (∀ u v, (((α:ℝ)+1/η)/4)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ (W y)) u v) v) ∧
        (∀ u, ‖fderiv ℝ (s y) u‖ ≤ (1/η-(α:ℝ))/4) ∧
        ∀ a : E, ContDiff ℝ 1 (fun u => s y u a) ∧
          MemLp (fun u => s y u a) 2 (S y) ∧
          AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.Poincare.Admissible (S y) (fun u => s y u a) ∧
          ∀ u, ‖gradient (fun z => s y z a) u‖ ≤ ((1/η-(α:ℝ))/4)*‖a‖ := by
  have conditional_derivatives {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
      {V : E → ℝ} (hV : ContDiff ℝ 2 V) (η : ℝ) (y : E) :
      let W := fun u : E => V ((1/2:ℝ) • (y+u)) + ‖u-y‖^2/(8*η)
      let s := fun u : E => -(1/2:ℝ) • fderiv ℝ V ((1/2:ℝ) • (y+u)) -
        (1/(4*η)) • innerSL ℝ (y-u)
      ContDiff ℝ 2 W ∧ ContDiff ℝ 1 s ∧
        ∀ u v w : E,
          (fderiv ℝ (fderiv ℝ W) u v) w =
            (1/4:ℝ) * (fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w +
              (1/(4*η)) * inner ℝ v w ∧
          (fderiv ℝ s u v) w =
            (1/(4*η)) * inner ℝ v w -
              (1/4:ℝ) * (fderiv ℝ (fderiv ℝ V) ((1/2:ℝ) • (y+u)) v) w := by
    let mid := fun u : E => (1/2:ℝ) • (y+u)
    let W := fun u : E => V (mid u) + ‖u-y‖^2/(8*η)
    let s := fun u : E => -(1/2:ℝ) • fderiv ℝ V (mid u) -
        (1/(4*η)) • innerSL ℝ (y-u)
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalScoreDomain.lean:30published source at 0e31a3cda412

Excerpt truncated; the exact source link is authoritative.