Actual finite-output KL with terminal residual discharged

Same actual P,derived target identity and RN-moment terminal KL,finite actual-chain accumulation and support/cap reduction.

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 finite_output_kl {V : E → ℝ} (κ : ℝ≥0) (hκ : 1 ≤ κ)
    (hV : ContDiff ℝ 2 V)
    (hH : ∀ x w : E, (κ:ℝ)⁻¹*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ ‖w‖^2)
    (hd : 0 < Module.finrank ℝ E)
    (η : S → ℝ) (hηm : Measurable η) (c Δ : ℝ)
    (hc : 0 < c) (hc1 : c < 1/4) (hη : ∀ s, 0 < η s ∧ η s ≤ c)
    (hΔ : 0 < Δ) (hΔ1 : Δ ≤ 1/2)
    (s0 : S) (M : Kernel S E) [IsMarkovKernel M] :
    let d : ℝ := Module.finrank ℝ E
    let K := fun r : ℝ => (1+r)/((κ:ℝ)⁻¹+r)
    let τ := fun s : S => if 2 ≤ K s.1 then K s.1 else c
    let L := (2:ℝ)+Real.log (K s0.1*d*(2:ℝ)/Δ)
    let B := (1/1024)/(Real.sqrt (d*L)+L)
    let J := Nat.ceil (8*Real.log (Real.exp 1*K s0.1/B))
    let _eps := Δ/Real.sqrt ((J:ℝ)+1)
    let v := fun s : S => (η s+τ s)/(1+s.1)
    let bp := fun s : S => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : S × (E × E) => p.2.1+Real.sqrt (τ p.1/(1+p.1.1)) • p.2.2
    let center := fun p : S × (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-(1+(bp p.1:ℝ))⁻¹ • gradient (F p) x
    let Qn := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex Qn (fun p => ((κ:ℝ)⁻¹+bp p.1)*d)
    let update := fun p : S × (E × E) =>
      (bp p.1,center p,(T p)^[N p] p.2.1,p.1.2.2.2.1+1,
        fun n => Nat.casesOn n (obs p) p.1.2.2.2.2)
    let bb := fun s : S => max (s.1:ℝ) B⁻¹
    let TF := fun s x => V x+bb s/2*‖x-s.2.1‖^2
    let TT := fun s x => x-(1+bb s)⁻¹ • gradient (TF s) x
    let TQn := fun n s => ‖gradient (TF s) ((TT s)^[n] (s.2.2.1))‖^2
    let TN := firstIndex TQn (fun s => d*bb s)
    let txp := fun s => (TT s)^[TN s] (s.2.2.1)
    let TA := fun s => (bb s)⁻¹
    let tg := fun s => gradient V (txp s)
    let th := fun s => s.2.1-TA s • tg s
    let tnu := (volume.restrict (Ioc (0 : ℝ) 1)).prod (stdGaussian E)
    let tW := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (scaledCached V TA th tg ((s,p.1),p.2)))
    let tproposal := fun s => (stdGaussian E).map (fun z => th s+Real.sqrt (TA s) • z)
    let trho := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (tproposal s) tnu 1 (by norm_num))
    let _tpi := fun s => ((stdGaussian E).map (fun z => s.2.1+Real.sqrt (TA s) • z)).tilted (fun x => -V x)
    let μV := (volume : Measure E).tilted (fun x => -V x)
    IsProbabilityMeasure μV ∧
    ∃ (Lt : Kernel S E) (P : Kernel S S) (TG H : Kernel S E),
      IsMarkovKernel Lt ∧ IsMarkovKernel P ∧ IsMarkovKernel TG ∧ IsMarkovKernel H ∧
      (∀ s, P s=if B⁻¹ ≤ (s.1:ℝ) then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
      (∀ s, (trho s).map (output (tW s) 1 0)=Lt s) ∧
      (∀ s, TG s=μV.tilted (fun x => -((s.1:ℝ)/2)*‖x-s.2.1‖^2)) ∧
      (∀ s, H s=AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        (TG s) (Real.sqrt (v s))) ∧
      let Q := fun s => AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        (M s) (Real.sqrt (τ s/(1+s.1)))
      let e := fun s => if B⁻¹ ≤ (s.1:ℝ) then 0 else klDiv (Q s) (H s)
      Measurable e ∧ ∀ m : ℕ,
        klDiv ((Lt ∘ₖ (P^(J+m))) s0) (TG s0) ≤
          (∑ j ∈ Finset.range J, ∫⁻ s, e s ∂(P^j) s0)+
          ENNReal.ofReal (Δ^2/((J:ℝ)+1)) := by
  classical
  intro d K τ L B J eps v bp obs center F T Qn N update bb TF TT TQn TN txp TA tg th tnu tW tproposal trho tpi μV
  have ht := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution.enhanced_terminal_execution
    κ hκ hV hH hd η hηm c 2 Δ hc hc1 hη (by norm_num) hΔ hΔ1 s0 M
  obtain ⟨hB,heps,heps1,hbb,hn,hxp,hres,Lt,P,hLt,hP,hPs,hmass,hstable,hacc⟩ := ht
  let := hLt
  let := hP
  have hk0 : (0:ℝ≥0) < κ := lt_of_lt_of_le (by norm_num) hκ
  have ha0 : (0:ℝ≥0) < κ⁻¹ := inv_pos.2 hk0
  have ha1 : κ⁻¹ ≤ (1:ℝ≥0) := (inv_le_one₀ hk0).2 hκ
  have hHm : ∀ x w : E, ((κ⁻¹:ℝ≥0):ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ ((1:ℝ≥0):ℝ)*‖w‖^2 := by simpa using hH
  have hdR : 0 < (Module.finrank ℝ E:ℝ) := by exact_mod_cast hd
  have hτm : Measurable τ := by
    have hKm : Measurable (fun s : S => K s.1) := by dsimp [K]; fun_prop
    exact Measurable.ite (measurableSet_le measurable_const hKm) hKm measurable_const
  have hτ0 (s : S) : 0 < τ s := by
    dsimp only [τ]
    split_ifs with h
    · linarith
    · exact hc
  have hs := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedKLOneStep.one_step_kl_error
    ha0 ha1 hV hHm hdR η τ hηm hτm (fun s => (hη s).1) hτ0 M (Real.toNNReal B⁻¹)
  obtain ⟨hμ,TG,H,P',hTG,hHG,hP',hTGf,hHf,hPsf,he',hsteps⟩ := hs
  let := hμ
  let := hTG
  let := hHG
  let := hP'
  have hstop (s : S) : Real.toNNReal B⁻¹ ≤ s.1 ↔ B⁻¹ ≤ (s.1:ℝ) := by
    change ((Real.toNNReal B⁻¹:ℝ≥0):ℝ) ≤ (s.1:ℝ) ↔ B⁻¹ ≤ (s.1:ℝ)
    rw [Real.coe_toNNReal _ (inv_pos.2 hB).le]
  have hPeq : P'=P := by
    apply Kernel.ext
    intro s
    have hx := hPsf s
    simp only [NNReal.coe_one,NNReal.coe_inv] at hx
    have hy : P s=if B⁻¹ ≤ (s.1:ℝ) then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z)) := hPs s
    by_cases hs : B⁻¹ ≤ (s.1:ℝ)
    · have hs' := (hstop s).2 hs
      simp only [if_pos hs'] at hx
      simp only [if_pos hs] at hy
      exact hx.trans hy.symm
    · have hs' : ¬Real.toNNReal B⁻¹ ≤ s.1 := fun h => hs ((hstop s).1 h)
      simp only [if_neg hs'] at hx
      simp only [if_neg hs] at hy
      exact hx.trans hy.symm
  subst P'
  refine ⟨hμ,Lt,P,TG,H,hLt,hP,hTG,hHG,hPs,?_,hTGf,?_,?_⟩
  · intro s
    exact (hacc s).1.2.1
  · intro s
    simpa only [NNReal.coe_one] using hHf s
  intro Q e
  have heq : (fun s : S => if Real.toNNReal B⁻¹ ≤ s.1 then 0 else
      klDiv (AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        (M s) (Real.sqrt (τ s/(1+s.1)))) (H s)) = e := by
    funext s
    by_cases hs : B⁻¹ ≤ (s.1:ℝ)
    · have hs' := (hstop s).2 hs
      simp only [if_pos hs',e,if_pos hs]
    · have hs' : ¬Real.toNNReal B⁻¹ ≤ s.1 := fun h => hs ((hstop s).1 h)
      simp only [if_neg hs',e,Q,if_neg hs]
  have he : Measurable e := by
    simp only [NNReal.coe_one] at he'
    rw [heq] at he'
    exact he'
  have hstep : ∀ R : Kernel S E, IsMarkovKernel R →
      Measurable (fun s => klDiv (R s) (TG s)) ∧
      ∀ s, klDiv ((R ∘ₖ P) s) (TG s) ≤ e s+∫⁻ t, klDiv (R t) (TG t) ∂P s := by
    intro R hR
    let := hR
    have hh := hsteps R
    simp only [NNReal.coe_one] at hh
    refine ⟨hh.1,fun s => ?_⟩
    have hh' := hh.2 s
    have heqs := congrFun heq s
    rw [heqs] at hh'
    exact hh' 
  refine ⟨he,?_⟩
  have hd1 : 1 ≤ d := by
    have hn1 : 1 ≤ Module.finrank ℝ E := hd
    dsimp only [d]
    exact_mod_cast hn1
  have hBlarge : 1 < B⁻¹ := (terminal_precision_large κ s0.1 hκ d Δ hd1 hΔ hΔ1).2
  have hlip : LipschitzWith (1:ℝ≥0) (gradient V) := by
    have hh := (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      (r:=0) hV hHm (0:E)).2
    simpa using hh
  have hterminal (s : S) (hs : B⁻¹ ≤ (s.1:ℝ)) : klDiv (Lt s) (TG s) ≤ ENNReal.ofReal (eps^2) := by
    have hb1 : 1 < (s.1:ℝ) := lt_of_lt_of_le hBlarge hs
    have hb0 : 0 < (s.1:ℝ) := lt_trans zero_lt_one hb1
    have hbstep : ((1:ℝ≥0):ℝ)*(s.1:ℝ)⁻¹ < 1 := by
      simpa using (inv_lt_one₀ hb0).2 hb1
    have heqt : TG s=tpi s := by
      rw [hTGf]
      have hh := actual_terminal_target V (hV.differentiable (by norm_num)) 1 hlip
        (s.1:ℝ) hb0 hbstep s.2.1
      have hbs : bb s=(s.1:ℝ) := hbb s hs
      dsimp only [tpi,TA]
      rw [hbs]
      simpa only [neg_div] using hh
    obtain ⟨_,hpi,_,hac,_,hI,_,_,_,hbound,_,_⟩ := hacc s
    let := hpi
    rw [heqt]
    apply kl_le_second_moment (Lt s) (tpi s) hac eps
    · simpa only [Real.rpow_two] using hI
    · simpa only [Real.rpow_two] using hbound
  have hPJ : IsMarkovKernel (P^J) := by
    induction J with
    | zero => change IsMarkovKernel Kernel.id; infer_instance
    | succ n ih =>
      let := ih
      rw [pow_succ]
      change IsMarkovKernel ((P^n) ∘ₖ P)
      infer_instance
  let := hPJ
  have hD : ∀ᵐ s ∂(P^J) s0, B⁻¹ ≤ (s.1:ℝ) := by
    rw [ae_iff]
    have hbMeas : Measurable (fun s : S => (s.1:ℝ)) := by fun_prop
    have hm : MeasurableSet {s : S | B⁻¹ ≤ (s.1:ℝ)} := measurableSet_le measurable_const hbMeas
    change (P^J) s0 {s : S | B⁻¹ ≤ (s.1:ℝ)}ᶜ=0
    rw [measure_compl hm (measure_ne_top _ _), hmass, measure_univ, tsub_self]
  have hresidual : (∫⁻ s, klDiv (Lt s) (TG s) ∂(P^J) s0) ≤ ENNReal.ofReal (eps^2) := by
    calc
      _ ≤ ∫⁻ _s, ENNReal.ofReal (eps^2) ∂(P^J) s0 :=
        lintegral_mono_ae (hD.mono fun s hs => hterminal s hs)
      _ = _ := by rw [lintegral_const, measure_univ, mul_one]
  have hepssq : eps^2=Δ^2/((J:ℝ)+1) := by
    dsimp only [eps]
    rw [div_pow, Real.sq_sqrt (by positivity)]
  intro m
  rw [hstable m]
  have hf := composed_error_sum P TG Lt e he hstep J s0
  exact hf.trans (add_le_add le_rfl (by simpa only [hepssq] using hresidual))

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL

Exact module and namespace context