ApproximateInitialGradientMoment: mathematical reading route

Actual Gibbs and Gaussian moments, actual smoothing pushforward, finite-cost coupling L1 and strict-budget elimination, true quadratic differentiation, absolutely integrable Gaussian cancellation and explicit arithmetic.

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 approximate_initial_gradient_moment {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)
    (ν : 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 M := 4*(β : ℝ)*d + 4*(β : ℝ)^2*η*d + 2*(β : ℝ)^2*r^2
    let F := fun y z x : E => U x + ‖x-(y+Real.sqrt τ • z)‖^2/(2*(η+τ))
    Integrable (fun y => ‖gradient U y‖^2) ν ∧
      (∫ y, ‖gradient U y‖^2 ∂ν) ≤ M ∧
      (∀ y z, gradient (F y z) y = gradient U y - (Real.sqrt τ/(η+τ)) • z) ∧
      Integrable (fun p : E × E => ‖gradient (F p.1 p.2) p.1‖^2) (ν.prod (stdGaussian E)) ∧
      (∫ p : E × E, ‖gradient (F p.1 p.2) p.1‖^2 ∂ν.prod (stdGaussian E)) =
        (∫ y, ‖gradient U y‖^2 ∂ν) + τ*d/(η+τ)^2 ∧
      (∫ p : E × E, ‖gradient (F p.1 p.2) p.1‖^2 ∂ν.prod (stdGaussian E)) ≤ M + τ*d/(η+τ)^2 ∧
      (β=1 → η≤1/4 → (∫ p : E × E, ‖gradient (F p.1 p.2) p.1‖^2 ∂ν.prod (stdGaussian E)) ≤
        5*(d+r^2+τ*d/(η+τ)^2)) := by
  let d : ℝ := Module.finrank ℝ E
  let μ := (volume : Measure E).tilted (fun x => -U x)
  let ρ := TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing μ (Real.sqrt η)
  let M := 4*(β : ℝ)*d + 4*(β : ℝ)^2*η*d + 2*(β : ℝ)^2*r^2
  let F := fun y z x : E => U x + ‖x-(y+Real.sqrt τ • z)‖^2/(2*(η+τ))
  have hG := TechnicalLemmas.Analysis.GibbsGradientMoment.gibbs_gradient_moment hα hαβ hU hH
  have : IsProbabilityMeasure μ := hG.1
  have hbase := TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
    (r := 0) hU hH (0 : E)
  have hLip : LipschitzWith β (gradient U) := by simpa using hbase.2
  have hSm := smoothing_square hLip hG.2.1 (Real.sqrt η)
  have hW := wasserstein_square hLip hSm.1 hw
  have hbound : (∫ y, ‖gradient U y‖^2 ∂ν) ≤ M := by
    have h1 := hG.2.2.2.2
    have h2 := hSm.2
    have h3 := hW.2
    rw [Real.sq_sqrt hη] at h2
    dsimp [M, d, μ, ρ] at *
    linarith
  have hA : 0 < η+τ := add_pos_of_nonneg_of_pos hη hτ
  have hgrad (y z : E) : gradient (F y z) y =
      gradient U y - (Real.sqrt τ/(η+τ)) • z := by
    rw [regularized_gradient hU hA]
    have he : y-(y+Real.sqrt τ • z) = -(Real.sqrt τ • z) := by abel
    rw [he]
    simp only [smul_neg, smul_smul, sub_eq_add_neg, div_eq_mul_inv, mul_comm]
  have hP := gaussian_perturbation_square hLip.continuous hW.1 (Real.sqrt τ/(η+τ))
  have hnoise : (Real.sqrt τ/(η+τ))^2 * d = τ*d/(η+τ)^2 := by
    rw [div_pow, Real.sq_sqrt hτ.le]
    ring
  have hEq : (∫ p : E × E, ‖gradient (F p.1 p.2) p.1‖^2 ∂ν.prod (stdGaussian E)) =
      (∫ y, ‖gradient U y‖^2 ∂ν) + τ*d/(η+τ)^2 := by
    simp_rw [hgrad]
    exact hP.2.trans (by rw [show (Module.finrank ℝ E : ℝ)=d from rfl, hnoise])
  refine ⟨hW.1, hbound, hgrad, ?_, hEq, ?_, ?_⟩
  · change Integrable (fun p : E × E => ‖gradient (F p.1 p.2) p.1‖^2) (ν.prod (stdGaussian E))
    simpa only [hgrad] using hP.1
  · rw [hEq]
    change (∫ y, ‖gradient U y‖^2 ∂ν) + τ*d/(η+τ)^2 ≤ M + τ*d/(η+τ)^2
    linarith
  · intro hβ hηsmall
    rw [hEq]
    have hd : 0 ≤ d := Nat.cast_nonneg _
    have hn : 0 ≤ τ*d/(η+τ)^2 := div_nonneg (mul_nonneg hτ.le hd) (sq_nonneg _)
    have hηd : 4*η*d ≤ d := by nlinarith [mul_le_mul_of_nonneg_right hηsmall hd]
    simp only [M, hβ, NNReal.coe_one, one_pow, mul_one] at hbound
    nlinarith [sq_nonneg r]


end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateInitialGradientMoment

Exact module and namespace context