Actual enhanced-state termination and terminal FORS execution

Source precision bound, full-state absorbed path comparison, kernel support induction, actual terminal construction and finite cap stability.

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 enhanced_terminal_execution {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 q Δ : ℝ)
    (hc : 0 < c) (hc1 : c < 1/4) (hη : ∀ s, 0 < η s ∧ η s ≤ c)
    (hq : 2 ≤ q) (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 := q+Real.log (K s0.1*d*q/Δ)
    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)
    0 < B ∧ 0 < eps ∧ eps ≤ 1/2 ∧
    (∀ s : S, B⁻¹ ≤ (s.1:ℝ) → bb s=(s.1:ℝ)) ∧
    Measurable TN ∧ Measurable txp ∧
    (∀ s, TQn (TN s) s ≤ d*bb s ∧ (∀ j < TN s, d*bb s < TQn j s) ∧
      ‖th s-txp s‖ ≤ Real.sqrt (d*TA s)) ∧
    ∃ (Lt : Kernel S E) (P : Kernel S S), IsMarkovKernel Lt ∧ IsMarkovKernel P ∧
      (∀ s, P s=if B⁻¹ ≤ (s.1:ℝ) then Measure.dirac s else
        ((M s).prod (stdGaussian E)).map (fun z => update (s,z))) ∧
      (P^J) s0 {s | B⁻¹ ≤ (s.1:ℝ)}=1 ∧
      (∀ m, (Lt ∘ₖ (P^(J+m))) s0=(Lt ∘ₖ (P^J)) s0) ∧
      ∀ s,
      (Measurable (output (tW s) 1 0) ∧ (trho s).map (output (tW s) 1 0)=Lt s ∧
        trho s {ω | ∀ n, ω n ∉ accepted (tW s) 1}=0 ∧
        (∫⁻ ω, 1+queryCount (tW s) 1 ω ∂trho s) ≤ ENNReal.ofReal (1+2*Real.exp 2)) ∧
      IsProbabilityMeasure (tpi s) ∧ tpi s ≪ Lt s ∧ Lt s ≪ tpi s ∧
      Integrable (fun x => ((tpi s).rnDeriv (Lt s) x).toReal^q) (Lt s) ∧
      Integrable (fun x => ((Lt s).rnDeriv (tpi s) x).toReal^q) (tpi s) ∧
      0 < (∫ x, ((tpi s).rnDeriv (Lt s) x).toReal^q ∂Lt s) ∧
      0 < (∫ x, ((Lt s).rnDeriv (tpi s) x).toReal^q ∂tpi s) ∧
      (∫ x, ((tpi s).rnDeriv (Lt s) x).toReal^q ∂Lt s) ≤ 1+eps^2 ∧
      (∫ x, ((Lt s).rnDeriv (tpi s) x).toReal^q ∂tpi s) ≤ 1+eps^2 ∧
      Real.log (∫ x, ((tpi s).rnDeriv (Lt s) x).toReal^q ∂Lt s)/(q-1) ≤ eps^2 ∧
      Real.log (∫ x, ((Lt s).rnDeriv (tpi s) x).toReal^q ∂tpi s)/(q-1) ≤ eps^2 := 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
  let L0 : Kernel S E := Kernel.const _ (stdGaussian E)
  have hL0 : IsMarkovKernel L0 := by dsimp [L0]; infer_instance
  have hfirst := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution.Actual.execution κ hκ hV hH hd η hηm c q Δ hc hc1 hη hq hΔ hΔ1 s0 M L0
  obtain ⟨hB,heps,heps1,hstep,_⟩ := hfirst
  have hκ0 : (0:ℝ≥0) < κ := lt_of_lt_of_le (by norm_num) hκ
  have hαβ : κ⁻¹ ≤ (1:ℝ≥0) := (inv_le_one₀ hκ0).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 hbound : 64*((1:ℝ≥0):ℝ)*(Real.sqrt (d*(q+Real.log (1/eps)))+(q+Real.log (1/eps))) ≤ B⁻¹ := by
    simpa only [NNReal.coe_one,mul_one] using hstep
  have ht := terminal_extension hV hHm hαβ (by norm_num)
    (show 0 < (Module.finrank ℝ E:ℝ) by exact_mod_cast hd)
    (fun s : S => (s.1:ℝ)) (fun s : S => s.2.1) (fun s : S => s.2.2.1)
    (by fun_prop) (by fun_prop) (by fun_prop) B⁻¹ q eps (inv_pos.2 hB) hq heps heps1 hbound
  obtain ⟨heq,hn,hx,hres,Lt,hLt,hacc⟩ := ht
  let := hLt
  have hactual := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution.Actual.execution κ hκ hV hH hd η hηm c q Δ hc hc1 hη hq hΔ hΔ1 s0 M Lt
  obtain ⟨_,_,_,_,P,hP,hPs,hmass,hstable⟩ := hactual
  exact ⟨hB,heps,heps1,heq,hn,hx,hres,Lt,P,hLt,hP,hPs,hmass,hstable,hacc⟩
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution

Exact module and namespace context