Actual ideal RGO identification and normalization

Mathematical statement

exp(-f) is G-integrable with strictly positive real integral; exp(m) is q-integrable with strictly positive real integral; exp(-V) is canonical-volume-integrable with strictly positive real integral. The actual q.tilted(m) equals G.tilted(-f) and also equals volume.withDensity(x → ofReal(exp(-V(x))/integral exp(-V) dvolume)).

theorem ideal_rgo_identification (f : E → ℝ) (hf : Differentiable ℝ f)
    (beta : NNReal) (hlip : LipschitzWith beta (gradient f))
    (eta : ℝ) (heta : 0 < eta) (hstep : (beta : ℝ)*eta < 1) (x0 xp : E) :
    let h := x0-eta • gradient f xp
    let P := (stdGaussian E).map (fun z => Real.sqrt eta • z)
    let nu := (volume.restrict (Set.Ioc (0 : ℝ) 1)).prod P
    let G := (stdGaussian E).map (fun z => x0 + Real.sqrt eta • z)
    let q := (stdGaussian E).map (fun z => h + Real.sqrt eta • z)
    let m := fun x => ∫ s, estimator f h xp x s ∂nu
    let V := fun x => f x + ‖x-x0‖^2/(2*eta)
    Integrable (fun x => Real.exp (-f x)) G ∧
      0 < ∫ x, Real.exp (-f x) ∂G ∧
      Integrable (fun x => Real.exp (m x)) q ∧
      0 < ∫ x, Real.exp (m x) ∂q ∧
      Integrable (fun x => Real.exp (-V x)) volume ∧
      0 < ∫ x, Real.exp (-V x) ∂volume ∧
      q.tilted m = G.tilted (fun x => -f x) ∧
      q.tilted m = (volume : Measure E).withDensity (fun x => ENNReal.ofReal
        (Real.exp (-V x) / ∫ y, Real.exp (-V y) ∂volume))

Proof roadmap

1. 1Obtain the sharp lower Taylor estimate from first derivatives

   For fixed u, consider H(t)=f(x0+t u)-t<grad f(x0),u>+(beta/2)t^2 norm(u)^2 on [0,1]. Differentiate the actual potential along this path. The Lipschitz gradient bound and Cauchy-Schwarz make H prime nonnegative. Monotonicity therefore gives H(1)≥H(0). This retains the precise beta/2 coefficient without a Hessian or convexity assumption.

2. 2Prove a coercive envelope and actual volume integrability

   Set k=1/eta-beta>0. Adding the proximal quadratic to the lower Taylor bound gives a quadratic with coefficient k/2. Young inequality absorbs the linear gradient term, leaving coefficient k/4. Exponentiation bounds the actual weight by an integrable translated Gaussian envelope. Continuity supplies measurability. The actual canonical volume is nonzero, so the integral of this everywhere positive integrable exponential is strictly positive.

3. 3Normalize under the actual Gaussian input

   Reuse the public scaled Gaussian density and prove the translation adapter by pushforward composition and volume translation invariance. Multiplying this density by exp(-f) gives c_eta exp(-V), where c_eta is the strictly positive Gaussian normalization constant. The withDensity integrability equivalence transfers the established volume L1 to the actual Gaussian G. Its probability property and integrability imply a strictly positive real integral. Applying the same density identity to the tilt gives the explicit normalized volume law.

4. 4Use the actual gradient-arc mean with one common constant

   Instantiate the proved GradientArcMean result at h=x0-eta grad f(x_plus). It already establishes the auxiliary integrability needed for its Fubini argument. Expanding the local estimator verifies that it is exactly the same sine/cosine arc and gradient difference. Its potential expectation defines C before x is chosen, and gives the actual mean identity for every x. No affine mean formula is assumed in place of the random estimator.

5. 5Cancel the actual translated Gaussian likelihood

   The public Gaussian likelihood theorem gives q=G.withDensity(L) in the correct direction. Substituting h-x0=-eta g yields log L=-<g,x-x0>-eta norm(g)^2/2. Multiplication by the actual exponential mean leaves A exp(-f), where A is positive and independent of x. This uses the actual proposal measure, not an abstract density selected to satisfy the conclusion.

6. 6Transfer integrability before cancelling normalizers

   The weighted integrability equivalence and the previous product identity prove exp(m) is q-integrable. Integration gives Z_q=A Z_G, hence Z_q>0. Only then expand the definition of exponential tilt and compose the two withDensity operations. The same positive A cancels in numerator and denominator. Combine this law equality with the established normalized volume identity and all three positive integrability statements.