Actual unclipped gradient-arc mean

AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean.gradient_arc_mean · theorem · Teaching coverage

Statement

The square of sqrt(eta) equals eta, U is a probability measure, and f(h+Z) is integrable under P. Define the finite constant C=integral f(h+z) dP(z)-<grad f(x_plus),h> before choosing x. For every x, W_x is jointly measurable and integrable under U product P, its integral is <grad f(x_plus),x>-f(x)+C, and for every z its time integral from 0 to 1 equals <grad f(x_plus),x-(h+z)>-f(x)+f(h+z).

All objects and hypotheses

• E is a finite-dimensional real inner-product space with its Borel measurable structure; second countability is explicit and automatic for this domain. The real-valued potential f is differentiable everywhere and its actual gradient is globally beta-Lipschitz.
• eta>0, beta>=0 and h,x_plus are arbitrary points. No positive dimension, convexity, center residual or clipping step restriction is assumed.
• P is the pushforward of stdGaussian E by z -> sqrt(eta) z, hence the actual auxiliary N(0,eta I). U is Lebesgue measure restricted to (0,1], which is the same uniform probability law as on [0,1].
• For each x,z and real r, theta=pi*r/2, gamma=h+sin(theta)(x-h)+cos(theta)z, v=(pi/2)(cos(theta)(x-h)-sin(theta)z), and W_x(r,z)=<v,grad f(x_plus)-grad f(gamma)>.

Mathematical proof

theorem gradient_arc_mean (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (h xp : E) :
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    (Real.sqrt eta)^2 = eta ∧ IsProbabilityMeasure U ∧
      Integrable (fun z => f (h+z)) P ∧
      ∀ x : E, Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) ∧
        Integrable (fun q : ℝ × E => estimator f h xp x q.2 q.1) (U.prod P) ∧
        (∀ z : E, (∫ r in (0 : ℝ)..1, estimator f h xp x z r) =
          inner ℝ (gradient f xp) (x-(h+z)) - f x + f (h+z)) ∧
        (∫ q : ℝ × E, estimator f h xp x q.2 q.1 ∂(U.prod P)) =
          inner ℝ (gradient f xp) x - f x + C

theorem gradient_arc_mean (f : E → ℝ) (hf : Differentiable ℝ f)
    (eta beta : ℝ) (heta : 0 < eta) (hbeta : 0 ≤ beta)
    (hlip : LipschitzWith ⟨beta,hbeta⟩ (gradient f)) (h xp : E) :
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let U := volume.restrict (Set.Ioc (0 : ℝ) 1)
    let C := (∫ z, f (h+z) ∂P) - inner ℝ (gradient f xp) h
    (Real.sqrt eta)^2 = eta ∧ IsProbabilityMeasure U ∧
      Integrable (fun z => f (h+z)) P ∧
      ∀ x : E, Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) ∧
        Integrable (fun q : ℝ × E => estimator f h xp x q.2 q.1) (U.prod P) ∧
        (∀ z : E, (∫ r in (0 : ℝ)..1, estimator f h xp x z r) =
          inner ℝ (gradient f xp) (x-(h+z)) - f x + f (h+z)) ∧
        (∫ q : ℝ × E, estimator f h xp x q.2 q.1 ∂(U.prod P)) =
          inner ℝ (gradient f xp) x - f x + C := by
  dsimp only
  refine ⟨Real.sq_sqrt heta.le, ⟨by simp⟩,
    potential_integrable f hf ⟨beta,hbeta⟩ hlip h (Real.sqrt eta), ?_⟩
  intro x
  have hg := hlip.continuous
  have hm : Measurable (fun q : ℝ × E => estimator f h xp x q.2 q.1) := by
    unfold estimator arc velocity
    fun_prop
  exact ⟨hm, estimator_integrable f ⟨beta,hbeta⟩ hlip h xp x (Real.sqrt eta) _,
    fun z => path_integral f hf ⟨beta,hbeta⟩ hlip h xp x z,
    auxiliary_mean f hf ⟨beta,hbeta⟩ hlip h xp x (Real.sqrt eta)⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean

Scope and omitted-condition boundaries

• This proves the actual unclipped estimator mean for each fixed x, including genuine Gaussian/uniform joint integrability. Coordinate-free spaces, zero dimension, beta=0 and arbitrary h are disclosed extensions. It does not assert joint parameter measurability in x,h,x_plus or an additional random-x integral. The source center h=x0-eta grad f(x_plus), completion of the Gaussian square, positive finite target normalization, clipped output law, Renyi comparison, initialization and actual query costs remain separate. L1 integrability of f(h+Z) does not imply exponential Gibbs integrability. Neither full companion paper is complete.