Restricted-Gaussian fiber log ratio and exact relative score

The proof combines the three canonical Mathlib llr identities pointwise on a full-measure set and uses absolute continuity to change the a.e. measure.

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 llr_tilted_tilted_ae
    (mu : Measure X) [SigmaFinite mu] (f g : X → ℝ)
    (hf : Measurable f)
    (hfi : Integrable (fun x => Real.exp (f x)) mu)
    (hgi : Integrable (fun x => Real.exp (g x)) mu) :
    MeasureTheory.llr (mu.tilted f) (mu.tilted g) =ᵐ[mu.tilted f]
      fun x => f x - Real.log (∫ z, Real.exp (f z) ∂mu) - g x +
        Real.log (∫ z, Real.exp (g z) ∂mu) := by
  have hbase :
      MeasureTheory.llr (mu.tilted f) (mu.tilted g) =ᵐ[mu]
        representative mu f g := by
    filter_upwards [
      MeasureTheory.llr_tilted_left
        (μ := mu) (ν := mu.tilted g) (f := f)
        (absolutelyContinuous_tilted hgi) hfi hf.aemeasurable,
      MeasureTheory.llr_tilted_right
        (μ := mu) (ν := mu) (f := g)
        Measure.AbsolutelyContinuous.rfl hgi,
      MeasureTheory.llr_self mu] with x hleft hright hself
    rw [hleft, hright, hself]
    simp [representative]
    ring
  exact (tilted_absolutelyContinuous mu f).ae_eq hbase

section Quadratic

variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E]

Exact module and namespace context

A private helper derives the genuine gradient of each quadratic from the norm-square derivative and the Hilbert duality map. The public proof removes constant normalizers and performs the linear cancellation.

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 gradient_quadratic_representative
    (mu : Measure E) {eta : ℝ} (heta : eta ≠ 0) (y y' x : E) :
    gradient
        (fun t =>
          -(‖t - y‖ ^ 2 / (2 * eta)) -
            Real.log (∫ z, Real.exp (-(‖z - y‖ ^ 2 / (2 * eta))) ∂mu) -
          (-(‖t - y'‖ ^ 2 / (2 * eta))) +
            Real.log (∫ z, Real.exp (-(‖z - y'‖ ^ 2 / (2 * eta))) ∂mu)) x =
      eta⁻¹ • (y - y') := by
  have hy := hasGradientAt_quadraticExponent heta y x
  have hy' := hasGradientAt_quadraticExponent heta y' x
  apply HasGradientAt.gradient
  rw [hasGradientAt_iff_hasFDerivAt]
  change HasFDerivAt
    (fun t => quadraticExponent eta y t -
      Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu) -
      quadraticExponent eta y' t +
      Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu))
    (InnerProductSpace.toDual ℝ E (eta⁻¹ • (y - y'))) x
  let c := Real.log (∫ z, Real.exp (quadraticExponent eta y z) ∂mu)
  let c' := Real.log (∫ z, Real.exp (quadraticExponent eta y' z) ∂mu)
  have hderiv : HasFDerivAt
      (fun t => quadraticExponent eta y t - c - quadraticExponent eta y' t + c')
      ((InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y))) -
        InnerProductSpace.toDual ℝ E (-eta⁻¹ • (x - y'))) x :=
    ((hy.hasFDerivAt.sub_const c).sub hy'.hasFDerivAt).add_const c'
  have hvec :
      (-eta⁻¹ • (x - y)) - (-eta⁻¹ • (x - y')) =
        eta⁻¹ • (y - y') := by
    module
  rw [← hvec, map_sub]
  simpa only [c, c'] using hderiv

end Quadratic

end

end TiltedLogRatio
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context