Actual joint inner reference stopping and expected count

Joint iteration continuity, strict terminal witness for actual inner first hitting, measurable choice, genuine residual identity, same-potential moment consumption and integrable logarithmic tangent.

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 joint_reference_gradient_descent [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
      fderiv ℝ (fderiv ℝ U) x v v ≤ (β:ℝ)*‖v‖^2)
    {η τ r : ℝ} (hη : 0 ≤ η) (hτ : 0 < τ) (hr : 0 ≤ r)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (ν : Measure E) [IsProbabilityMeasure ν]
    (hw : TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance ν
      (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        ((volume : Measure E).tilted (fun x => -U x)) (Real.sqrt η)) ^ 2 ≤ ENNReal.ofReal (r^2)) :
    let d : ℝ := Module.finrank ℝ E
    let A := η+τ
    let a := (α:ℝ)+A⁻¹
    let c := (β:ℝ)+A⁻¹
    let k := c/a
    let M := 4*(β:ℝ)*d+4*(β:ℝ)^2*η*d+2*(β:ℝ)^2*r^2
    let u := fun p : E × E => p.1+Real.sqrt τ • p.2
    let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
    let T := fun p x => x-c⁻¹ • gradient (F p) x
    let N := jointIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
    let out := fun p => (T p)^[N p] p.1
    Measurable N ∧ Measurable out ∧
      (∀ p, ‖gradient (F p) (out p)‖^2 ≤ a*d ∧
        ‖u p-A • gradient U (out p)-out p‖ = A*‖gradient (F p) (out p)‖ ∧
        ‖u p-A • gradient U (out p)-out p‖ ≤ A*Real.sqrt (a*d) ∧
        (∀ j < N p, a*d < ‖gradient (F p) ((T p)^[j] p.1)‖^2) ∧
        (N p:ℝ)+1 ≤ k*Real.log (1+A*‖gradient (F p) p.1‖^2/d)+2) ∧
      Integrable (fun p => (N p:ℝ)+1) (ν.prod (stdGaussian E)) ∧
      (∫ p, (N p:ℝ)+1 ∂ν.prod (stdGaussian E)) ≤
        2+k*Real.log (1+A*(M+τ*d/A^2)/d) := by
  let d : ℝ := Module.finrank ℝ E
  let A := η+τ
  let a := (α:ℝ)+A⁻¹
  let c := (β:ℝ)+A⁻¹
  let k := c/a
  let M := 4*(β:ℝ)*d+4*(β:ℝ)^2*η*d+2*(β:ℝ)^2*r^2
  let u := fun p : E × E => p.1+Real.sqrt τ • p.2
  let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
  let T := fun p x => x-c⁻¹ • gradient (F p) x
  let N := jointIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
  let out := fun p => (T p)^[N p] p.1
  have hA : 0 < A := add_pos_of_nonneg_of_pos hη hτ
  have ha : 0 < a := add_pos_of_nonneg_of_pos α.coe_nonneg (inv_pos.mpr hA)
  have hc : 0 < c := add_pos_of_nonneg_of_pos β.coe_nonneg (inv_pos.mpr hA)
  have hP := actual_joint_program (τ:=τ) hU hH hαβ hA hd rfl
  have hgrad (p : E × E) (x : E) :
      gradient (F p) x=gradient U x+A⁻¹ • (x-u p) :=
    (TerminalReferenceGradientDescent.terminal_reference_gradient_descent
      hU hH hαβ hA hd rfl (u p)).2.2.2.1 x
  have hres (p : E × E) (x : E) :
      ‖u p-A • gradient U x-x‖=A*‖gradient (F p) x‖ := by
    have he : u p-A • gradient U x-x=-(A • gradient (F p) x) := by
      rw [hgrad,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]
  have hMom := ApproximateInitialGradientMoment.approximate_initial_gradient_moment
    hα hαβ hU hH hη hτ hr ν hw
  have hFeq (y z : E) :
      (fun x => U x+‖x-(y+Real.sqrt τ • z)‖^2/(2*(η+τ)))=F (y,z) := by
    funext x
    dsimp [F,u,A]
    simp only [div_eq_mul_inv,mul_inv_rev]
    ring
  have hgi : Integrable (fun p : E × E => ‖gradient (F p) p.1‖^2)
      (ν.prod (stdGaussian E)) := by
    simpa only [hFeq] using hMom.2.2.2.1
  have hM : (∫ p : E × E, ‖gradient (F p) p.1‖^2 ∂ν.prod (stdGaussian E)) ≤
      M+τ*d/A^2 := by
    simpa only [hFeq] using hMom.2.2.2.2.2.1
  have hgm : Measurable (fun p : E × E => ‖gradient (F p) p.1‖^2) := by
    simp_rw [hgrad]
    have hgU := TechnicalLemmas.Analysis.Calculus.Gradient.continuous_gradient_of_contDiff_one
      (hU.of_le (by norm_num))
    exact ((hgU.comp continuous_fst).add
      ((continuous_fst.sub (continuous_fst.add (continuous_snd.const_smul _))).const_smul _)).norm.pow 2 |>.measurable
  have ratio (z : ℝ) : z/(d/A)=A*z/d := by field_simp
  have hE := expected_count (ν.prod (stdGaussian E))
    (fun p => ‖gradient (F p) p.1‖^2) N (k:=k) (s:=d/A)
    (div_pos hc ha) (div_pos hd hA)
    hgm hgi (fun p => sq_nonneg _) hP.1 hM (fun p => by
      simpa only [ratio] using (hP.2.2 p).2.2)
  refine ⟨hP.1,hP.2.1,fun p => ?_,hE.1,?_⟩
  · have hp := hP.2.2 p
    refine ⟨hp.1,hres p _,?_,hp.2.1,hp.2.2⟩
    rw [hres]
    exact mul_le_mul_of_nonneg_left (Real.le_sqrt_of_sq_le hp.1) hA.le
  · simpa only [ratio] using hE.2

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.JointReferenceGradientDescent

Exact module and namespace context