EnhancedKLOneStep: mathematical reading route

Real Gibbs posterior recovery,actual conditional-reference alignment,KL mixture/chain and active/stopped execution branches.

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 one_step_kl_error {V : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hV : ContDiff ℝ 2 V)
    (hHess : ∀ x w : E, (α:ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ (β:ℝ)*‖w‖^2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (η τ : RefState E → ℝ) (hη : Measurable η) (hτ : Measurable τ)
    (hη0 : ∀ s, 0 < η s) (hτ0 : ∀ s, 0 < τ s)
    (M : Kernel (RefState E) E) [IsMarkovKernel M] (threshold : ℝ≥0) :
    let d : ℝ := Module.finrank ℝ E
    let v := fun s : RefState E => (η s+τ s)/((β:ℝ)+s.1)
    let bp := fun s : RefState E => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : RefState E × (E × E) => p.2.1+Real.sqrt (τ p.1/((β:ℝ)+p.1.1)) • p.2.2
    let center := fun p : RefState E × (E × E) => (bp p.1:ℝ)⁻¹ •
      ((p.1.1:ℝ) • p.1.2.1+(v p.1)⁻¹ • obs p)
    let F := fun p x => V x+(bp p.1:ℝ)/2*‖x-center p‖^2
    let T := fun p x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (F p) x
    let q := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex q (fun p => ((α:ℝ)+bp p.1)*d)
    let out := fun p => (T p)^[N p] p.2.1
    let update := fun p : RefState E × (E × E) =>
      (bp p.1,center p,out p,p.1.2.2.2.1+1,fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    let μ := (volume : Measure E).tilted (fun x => -V x)
    IsProbabilityMeasure μ ∧
    ∃ (T H : Kernel (RefState E) E) (P : Kernel (RefState E) (RefState E)),
      ∃ hT : IsMarkovKernel T, ∃ hH : IsMarkovKernel H, ∃ hP : IsMarkovKernel P,
      letI := hT
      letI := hH
      letI := hP
      (∀ s, T s=μ.tilted (fun x => -((s.1:ℝ)/2)*‖x-s.2.1‖^2)) ∧
      (∀ s, H s=AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        (T s) (Real.sqrt (v s))) ∧
      (∀ s, P s=if threshold ≤ s.1 then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
      let Q := fun s => AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        (M s) (Real.sqrt (τ s/((β:ℝ)+s.1)))
      let e := fun s => if threshold ≤ s.1 then 0 else klDiv (Q s) (H s)
      Measurable e ∧ ∀ (R : Kernel (RefState E) E) [IsMarkovKernel R],
        Measurable (fun s => klDiv (R s) (T s)) ∧ ∀ s,
        klDiv ((R ∘ₖ P) s) (T s) ≤ e s+∫⁻ t, klDiv (R t) (T t) ∂P s := by
  classical
  intro d v bp obs center F Tstep q N out update μ
  have hβ : 0 < (β:ℝ) := lt_of_lt_of_le (show 0 < (α:ℝ) from hα)
    (show (α:ℝ) ≤ β from hαβ)
  have hv (s : RefState E) : 0 < v s :=
    div_pos (add_pos (hη0 s) (hτ0 s)) (add_pos_of_pos_of_nonneg hβ s.1.coe_nonneg)
  have hvm : Measurable v := by dsimp [v]; fun_prop
  have hbp (s : RefState E) : (bp s:ℝ)=(s.1:ℝ)+(v s)⁻¹ := by
    simp only [bp,NNReal.coe_add,Real.coe_toNNReal _ (inv_pos.mpr (hv s)).le]
  obtain ⟨hμ,T,H,K,hT,hH,hK,hTf,hHf,hKf,hrec⟩ :=
    actual_gibbs_posterior hα hαβ hV hHess (fun s : RefState E => (s.1:ℝ)) v
      (fun s => s.2.1) (by fun_prop) hvm (by fun_prop) (fun s => s.1.coe_nonneg) hv
  let := hμ
  let := hT
  let := hH
  let := hK
  obtain ⟨J,hJ,hJs,hQ,hdis,hsupp,hfact,P,hP,hPs,hactive⟩ :=
    AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernel.observation_conditional_kernel
      hα hαβ hV hHess hd η τ hη hτ hη0 hτ0 M threshold
  let := hJ
  let := hP
  have href := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel.reference_carrying_kernel
    hα hαβ hV hHess hd η τ hη hτ hη0 hτ0 M threshold
  have hu : Measurable update := href.2.2.2.1
  have ho : Measurable obs := by dsimp [obs]; fun_prop
  have hJs' (s : RefState E) : J s=((M s).prod (stdGaussian E)).map
      (fun z => (obs (s,z),update (s,z))) := hJs s
  have hPs' (s : RefState E) : P s=if threshold ≤ s.1 then Measure.dirac s else
      ((M s).prod (stdGaussian E)).map (fun z => update (s,z)) := hPs s
  have halign (s : RefState E) : ∀ᵐ y ∂J.fst s, ∀ᵐ t ∂J.condKernel (s,y), T t=K (s,y) := by
    filter_upwards [hsupp s] with y hy
    filter_upwards [hy] with t ht
    rw [hTf,hKf,ht.1,ht.2,hbp]
  refine ⟨hμ,T,H,P,hT,hH,hP,hTf,hHf,hPs',?_⟩
  intro Q e
  have heq : e=(fun s => if threshold ≤ s.1 then 0 else klDiv (J.fst s) (H s)) := by
    funext s
    simp only [e,Q,hQ]
  have he : Measurable e := by
    rw [heq]
    exact Measurable.ite (measurableSet_le measurable_const (by fun_prop))
      measurable_const (measurable_fiber_kl J.fst H)
  refine ⟨he,fun R hR => ?_⟩
  let := hR
  have hmR := measurable_fiber_kl R T
  refine ⟨hmR,fun s => ?_⟩
  by_cases hs : threshold ≤ s.1
  · simp only [e,Kernel.comp_apply,hPs',if_pos hs,
      Measure.dirac_bind R.measurable,lintegral_dirac' s hmR,zero_add,le_refl]
  · have hPJ : P s=J.snd s := by
      have hf : Measurable (fun z : E × E => (obs (s,z),update (s,z))) :=
        (ho.prodMk hu).comp (measurable_const.prodMk measurable_id)
      rw [hPs',if_neg hs,Kernel.snd_apply,hJs',Measure.map_map measurable_snd hf]
      rfl
    have hc := conditional_step J P T H K R s hPJ (hrec s) (halign s)
    simpa only [e,Q,if_neg hs,hQ] using hc

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedKLOneStep

Exact module and namespace context