Actual terminal reference by gradient descent

Derive regularized curvature and gradient, contract adjacent actual iterates, construct a finite ceiling certificate, prove measurable first hit, convert its residual and integrate a logarithmic tangent bound.

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_reference_gradient_descent [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {m b : ℝ≥0}
    (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (m:ℝ)*‖v‖^2 ≤ (fderiv ℝ (fderiv ℝ U) x v) v ∧
      (fderiv ℝ (fderiv ℝ U) x v) v ≤ (b:ℝ)*‖v‖^2)
    (hmb : m ≤ b) {A d : ℝ} (hA : 0 < A) (hd : 0 < d)
    (_hdim : d = Module.finrank ℝ E) (u : E) :
    let F := fun x => U x+A⁻¹/2*‖x-u‖^2
    let a := (m:ℝ)+A⁻¹
    let c := (b:ℝ)+A⁻¹
    let k := c/a
    let T := fun x => x-c⁻¹ • gradient F x
    let N := firstIndex T F (d/A)
    let xp := fun v => T^[N v] v
    0 < a ∧ 0 < c ∧ 1 ≤ k ∧
    (∀ x, gradient F x=gradient U x+A⁻¹ • (x-u)) ∧
    Measurable N ∧ Measurable xp ∧
    (∀ v, ‖gradient F (xp v)‖^2 ≤ d/A ∧
      ‖u-A • gradient U (xp v)-xp v‖=A*‖gradient F (xp v)‖ ∧
      ‖u-A • gradient U (xp v)-xp v‖ ≤ Real.sqrt (d*A) ∧
      (∀ j < N v, d/A < ‖gradient F (T^[j] v)‖^2) ∧
      N v ≤ Nat.ceil (k*Real.log (1+A*‖gradient F v‖^2/d)) ∧
      (N v:ℝ)+1 ≤ k*Real.log (1+A*‖gradient F v‖^2/d)+2) ∧
    (∀ (μ : Measure E), IsProbabilityMeasure μ → ∀ M : ℝ,
      Integrable (fun v => ‖gradient F v‖^2) μ →
      (∫ v, ‖gradient F v‖^2 ∂μ) ≤ M →
      Integrable (fun v => (N v:ℝ)+1) μ ∧
      (∫ v, (N v:ℝ)+1 ∂μ) ≤ 2+k*Real.log (1+A*M/d)) := by
  let r : ℝ≥0 := ⟨A⁻¹,inv_nonneg.mpr hA.le⟩
  let F := fun x => U x+A⁻¹/2*‖x-u‖^2
  let a := (m:ℝ)+A⁻¹
  let c := (b:ℝ)+A⁻¹
  let k := c/a
  let T := fun x => x-c⁻¹ • gradient F x
  let N := firstIndex T F (d/A)
  let xp := fun v => T^[N v] v
  have ha : 0 < a := add_pos_of_nonneg_of_pos m.coe_nonneg (inv_pos.mpr hA)
  have hc : 0 < c := add_pos_of_nonneg_of_pos b.coe_nonneg (inv_pos.mpr hA)
  have hk : 1 ≤ k := by
    apply (le_div_iff₀ ha).mpr
    have hmb' : (m:ℝ) ≤ b := hmb
    dsimp [a,c]
    linarith
  have hdata := regularized_data (r:=r) hU hH u
  have hF : ContDiff ℝ 2 F := hdata.1
  have hsc : StrongConvexOn univ a F := hdata.2.1
  have hg (x : E) : gradient F x=gradient U x+A⁻¹ • (x-u) := hdata.2.2.2.1 x
  have hu : ∀ x y, F y ≤ F x+inner ℝ (gradient F x) (y-x)+c/2*‖y-x‖^2 :=
    hdata.2.2.2.2
  have hp := stopped_program (hF.of_le (by norm_num)) ha hc
    (div_pos hd hA) hsc hu
  have ratio (z : ℝ) : z/(d/A)=A*z/d := by field_simp
  have hres (x : E) : ‖u-A • gradient U x-x‖=A*‖gradient F x‖ := by
    have he : u-A • gradient U x-x=-(A • gradient F x) := by
      rw [hg,smul_add,smul_smul,mul_inv_cancel₀ hA.ne',one_smul]
      abel
    rw [he,norm_neg,norm_smul,Real.norm_eq_abs,abs_of_pos hA]
  refine ⟨ha,hc,hk,hg,hp.1,hp.2.1,?_,?_⟩
  · intro v
    have hv := hp.2.2 v
    have hstop : ‖gradient F (xp v)‖^2 ≤ d/A := hv.1
    have hr : ‖u-A • gradient U (xp v)-xp v‖ ≤ Real.sqrt (d*A) := by
      apply Real.le_sqrt_of_sq_le
      rw [hres,mul_pow]
      have hh := mul_le_mul_of_nonneg_left hstop (sq_nonneg A)
      have he : A^2*(d/A)=d*A := by field_simp
      rw [he] at hh
      exact hh
    refine ⟨hstop,hres _,hr,hv.2.1,?_,?_⟩
    · simpa only [ratio] using hv.2.2.1
    · simpa only [ratio] using hv.2.2.2
  · intro μ hμ M hgi hM
    let : IsProbabilityMeasure μ := hμ
    have hgm : Measurable (fun v => ‖gradient F v‖^2) :=
      ((TechnicalLemmas.Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
        (hF.of_le (by norm_num))).norm.pow 2).measurable
    have he := expected_count μ (fun v => ‖gradient F v‖^2) N (div_pos hc ha)
      (div_pos hd hA) hgm hgi (fun v => sq_nonneg _) hp.1 hM (fun v => (hp.2.2 v).2.2.2)
    simpa only [ratio] using he







end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalReferenceGradientDescent

Exact module and namespace context