Actual unclipped gradient-arc mean

Mathematical 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).

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

Proof roadmap

1. 1Use the actual auxiliary input and uniform time

   The noise is the pushforward of the centered identity-covariance Gaussian by sqrt(eta) scaling. Positive eta gives the exact variance identity. Lebesgue measure on (0,1] has total mass one. The choice of one open endpoint changes no probability mass and agrees with the interval-integral convention used below.

2. 2Integrate the actual path derivative

   Extract the public derivative and endpoints from GaussianArcLaw. Its auxiliary scale value 1 is used only to obtain these deterministic facts, never to replace the actual noise law. Apply the true gradient chain rule to r → <grad f(x_plus),gamma_r>-f(gamma_r). The Lipschitz gradient and continuous path imply that its derivative W is continuous, so FTC applies. The path starts at h+z and ends at x.

3. 3Prove potential integrability from quadratic growth

   Along the straight line h+t z, the gradient norm is at most norm(grad f(h))+beta norm(z) for t in [0,1]. The segment derivative bound yields the displayed quadratic growth estimate; no convexity is required. Gaussian second moments persist under actual scalar pushforward, so the constant, linear norm and squared norm terms are integrable. Measurable domination proves f(h+Z) integrable before defining its expectation.

4. 4Bound the same estimator uniformly in time

   Let A=norm(x-h) and D=norm(x_plus-h). Sine and cosine are bounded by one in absolute value, so the speed norm is at most (pi/2)(A+norm(z)) and the arc distance from x_plus is at most D+A+norm(z). Apply the actual gradient Lipschitz inequality and the inner-product norm inequality. This bound holds for every real time; it supplies one majorant for the whole uniform-time integral.

5. 5Establish joint integrability before Fubini

   Expand the majorant as a constant plus a linear norm term plus a squared norm term. The actual mapped Gaussian has finite second moment, making this polynomial integrable. Its lift to the product with the finite uniform-time measure is integrable. Gradient continuity makes the explicit W jointly measurable; domination then proves W integrable under the product. The proof does not infer joint integrability merely from fixed-time sections.

6. 6Identify one finite constant for every x

   Use Fubini only after the preceding joint-integrability result, then replace each time integral by the FTC identity. The actual auxiliary mean is zero, proved by the Gaussian map integral and scalar linearity. The linear, constant and potential terms are individually integrable, so their integrals can be separated. The remaining C depends on f,h,x_plus,eta and is defined before the universal quantifier over x.