Actual terminal reference, FORS kernel and source program

Genuine terminal firsthit and residual; fixed auxiliary Markov program; true-law cached cost; scaled mean identity; source RN comparison; full infinite-product reparameterization and AE defaults.

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 terminal_fors_kernel {V : E → ℝ} {α β : ℝ≥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αβ : α ≤ β) (hβ : 0 < (β:ℝ)) (hd : 0 < (Module.finrank ℝ E : ℝ))
    {b : S → ℝ} {u initial : S → E} (hb : Measurable b)
    (hb0 : ∀ s, 0 < b s) (hu : Measurable u) (hi : Measurable initial)
    (ell eps : ℝ) (hell : 2 ≤ ell) (heps : 0 < eps) (heps1 : eps ≤ 1/2)
    (hstep : ∀ s, 64*(β:ℝ)*(Real.sqrt ((Module.finrank ℝ E:ℝ)*(ell+Real.log (1/eps)))+
      (ell+Real.log (1/eps))) ≤ b s) :
    let d : ℝ := Module.finrank ℝ E
    let F := fun s x => V x+b s/2*‖x-u s‖^2
    let T := fun s x => x-((β:ℝ)+b s)⁻¹ • gradient (F s) x
    let Qn := fun n s => ‖gradient (F s) ((T s)^[n] (initial s))‖^2
    let N := firstIndex Qn (fun s => d*b s)
    let xp := fun s => (T s)^[N s] (initial s)
    let A := fun s => (b s)⁻¹
    let g := fun s => gradient V (xp s)
    let h := fun s => u s-A s • g s
    let ν := (volume.restrict (Ioc (0 : ℝ) 1)).prod (stdGaussian E)
    let W := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (scaledCached V A h g ((s,p.1),p.2)))
    let q := fun s => (stdGaussian E).map (fun z => h s+Real.sqrt (A s) • z)
    let ρ := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (q s) ν 1 (by norm_num))
    let π := fun s => ((stdGaussian E).map (fun z => u s+Real.sqrt (A s) • z)).tilted (fun x => -V x)
    let νa := fun s => (volume.restrict (Ioc (0 : ℝ) 1)).prod ((stdGaussian E).map (fun z => Real.sqrt (A s) • z))
    let Wa := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (cachedEstimator V (h s) (g s) p))
    let ρa := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (q s) (νa s) 1 (by norm_num))
    let Φ := fun s (ω : ℕ → Attempt E (ℝ × E)) n =>
      Stream.attemptMap (fun p : ℝ × E => (p.1,Real.sqrt (A s) • p.2)) (ω n)
    Measurable N ∧ Measurable xp ∧
    (∀ s, Qn (N s) s ≤ d*b s ∧ (∀ j < N s, d*b s < Qn j s) ∧
      ‖h s-xp s‖ ≤ Real.sqrt (d*A s)) ∧
    ∃ R : Kernel S E, IsMarkovKernel R ∧ ∀ s,
      (Measurable (output (W s) 1 0) ∧ (ρ s).map (output (W s) 1 0)=R s ∧
        ρ s {ω | ∀ n, ω n ∉ accepted (W s) 1}=0 ∧
        (∫⁻ ω, 1+queryCount (W s) 1 ω ∂ρ s) ≤ ENNReal.ofReal (1+2*Real.exp 2)) ∧
      IsProbabilityMeasure (π s) ∧ π s ≪ R s ∧ R s ≪ π s ∧
      Integrable (fun x => ((π s).rnDeriv (R s) x).toReal^ell) (R s) ∧
      Integrable (fun x => ((R s).rnDeriv (π s) x).toReal^ell) (π s) ∧
      0 < (∫ x, ((π s).rnDeriv (R s) x).toReal^ell ∂R s) ∧
      0 < (∫ x, ((R s).rnDeriv (π s) x).toReal^ell ∂π s) ∧
      (∫ x, ((π s).rnDeriv (R s) x).toReal^ell ∂R s) ≤ 1+eps^2 ∧
      (∫ x, ((R s).rnDeriv (π s) x).toReal^ell ∂π s) ≤ 1+eps^2 ∧
      Real.log (∫ x, ((π s).rnDeriv (R s) x).toReal^ell ∂R s)/(ell-1) ≤ eps^2 ∧
      Real.log (∫ x, ((R s).rnDeriv (π s) x).toReal^ell ∂π s)/(ell-1) ≤ eps^2 ∧
      (ρ s).map (Φ s)=ρa s ∧
      (∀ ω n, Φ s ω n ∈ accepted (Wa s) 1 ↔ ω n ∈ accepted (W s) 1) ∧
      (∀ ω, queryCount (Wa s) 1 (Φ s ω)=queryCount (W s) 1 ω) ∧
      (fun ω => output (Wa s) 1 (u s) (Φ s ω)) =ᵐ[ρ s] output (W s) 1 0 := by
  let d : ℝ := Module.finrank ℝ E
  let F := fun s x => V x+b s/2*‖x-u s‖^2
  let T := fun s x => x-((β:ℝ)+b s)⁻¹ • gradient (F s) x
  let Qn := fun n s => ‖gradient (F s) ((T s)^[n] (initial s))‖^2
  let N := firstIndex Qn (fun s => d*b s)
  let xp := fun s => (T s)^[N s] (initial s)
  let A := fun s => (b s)⁻¹
  let g := fun s => gradient V (xp s)
  let h := fun s => u s-A s • g s
  let ν := (volume.restrict (Ioc (0 : ℝ) 1)).prod (stdGaussian E)
  let W := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (scaledCached V A h g ((s,p.1),p.2)))
  let q := fun s => (stdGaussian E).map (fun z => h s+Real.sqrt (A s) • z)
  let ρ := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (q s) ν 1 (by norm_num))
  let π := fun s => ((stdGaussian E).map (fun z => u s+Real.sqrt (A s) • z)).tilted (fun x => -V x)
  let νa := fun s => (volume.restrict (Ioc (0 : ℝ) 1)).prod ((stdGaussian E).map (fun z => Real.sqrt (A s) • z))
  let Wa := fun s (p : E × (ℝ × E)) => min 1 (max (-1) (cachedEstimator V (h s) (g s) p))
  let ρa := fun s => Measure.infinitePi (fun _ : ℕ => attemptLaw (q s) (νa s) 1 (by norm_num))
  let Φ := fun s (ω : ℕ → Attempt E (ℝ × E)) n =>
    Stream.attemptMap (fun p : ℝ × E => (p.1,Real.sqrt (A s) • p.2)) (ω n)
  have href := variable_reference hV hH hαβ hd hb hb0 hu hi
  have hxp : Measurable xp := href.2.1
  have hVm : Measurable (gradient V) :=
    (TechnicalLemmas.Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
      (hV.of_le (by norm_num))).measurable
  have hAm : Measurable A := hb.inv
  have hgm : Measurable g := hVm.comp hxp
  have hhm : Measurable h := hu.sub (hAm.smul hgm)
  have hlip : LipschitzWith β (gradient V) := by
    have hh := (TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      (r:=0) hV hH (0 : E)).2
    simpa using hh
  obtain ⟨R,hR,hRs⟩ := actual_kernel_program hVm hAm hhm hgm
  refine ⟨href.1,hxp,href.2.2.2,R,hR,fun s => ?_⟩
  have hs := hRs s
  refine ⟨⟨hs.1,hs.2.1,hs.2.2.2.1,hs.2.2.2.2⟩,?_⟩
  have hcenter : ‖(u s-A s • gradient V (xp s))-xp s‖ ≤ Real.sqrt (d*A s) :=
    (href.2.2.2 s).2.2
  have ht := TerminalSamplerAccuracyCost.terminal_sampler_accuracy_cost V
    (hV.differentiable (by norm_num)) (A s) (β:ℝ) ell eps
    (inv_pos.mpr (hb0 s)) hβ hell heps heps1 hd hlip (u s) (xp s) hcenter
    (by simpa only [A,one_div,inv_inv] using hstep s)
  have hr := hs.2.2.1
  change R s = (q s).tilted (fun x => ∫ z,
    min 1 (max (-1) (scaledCached V A h g ((s,x),z))) ∂ν) at hr
  dsimp only [ν] at hr
  simp_rw [scaled_mean hVm A h g s] at hr
  rw [hr]
  rcases ht with ⟨_,_,_,_,_,hpi,hpq,hqp,hfi,hri,hfp,hrp,hfb,hrb,hfl,hrl,_,_⟩
  have hc := source_correspondence V (A s) (h s) (g s) (u s)
  refine ⟨hpi,hpq,hqp,hfi,hri,hfp,hrp,hfb,hrb,hfl,hrl,hc.1,hc.2.1,hc.2.2.1,?_⟩
  exact hc.2.2.2 hs.2.2.2.1

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalFORSKernel

Exact module and namespace context