standardized_rgo_unique_prox_and_kl_le_fisher

Plain-English statement

Actual same-prox canonical finite KL<=half smooth rho Fisher. Internally reconcile actual32/33 proximal witnesses by uniqueness, transport all rho/Z/q/f/r, use actual42 noncompact GaussianLSI2 and actual32 quarter energy/mass1. True posterior probability/AC/finiteKL/scoreL2 outputs; no supplied law/coherence/domain/inequality certificate or pointwise canonicalRN derivative. Actual eta2/unboundedfamily/rank0 Tests. GaussianT2/FIRST/main/work/cost separate. Independently verified 19b569ae0fe37c97da0f98b4d1f4933ebabc7052.

Lean statement

theorem standardized_rgo_unique_prox_and_kl_le_fisher
    {E S : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    [MeasurableSpace S] {V : E → ℝ} {κ : ℝ}
    (hκ : 1 ≤ κ) (hV : ContDiff ℝ 2 V)
    (hH : ∀ x v : E, κ⁻¹*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ V) x v v ∧
      fderiv ℝ (fderiv ℝ V) x v v ≤ ‖v‖^2)
    {eta : S → ℝ} {y : S → E} (heta : Measurable eta) (hy : Measurable y)
    (hpos : ∀ s, 0 < eta s) :
    ∃ p : S → E, Measurable p ∧
      (∀ s, p s+eta s • gradient V (p s)=y s) ∧
      (∀ s z, z+eta s • gradient V z=y s → z=p s) ∧
      let rho := fun s u => V (p s+Real.sqrt (eta s) • u)-V (p s)-
        Real.sqrt (eta s)*inner ℝ (gradient V (p s)) u
      let mu := (volume : Measure E).tilted (fun x => -V x)
      let R := fun s => mu.tilted (fun x => -‖x-y s‖^2/(2*eta s))
      let r := fun s => (R s).map (fun x => (Real.sqrt (eta s))⁻¹ • (x-p s))
      let gamma := stdGaussian E
      ∀ s, IsProbabilityMeasure (r s) ∧ r s ≪ gamma ∧
        _root_.InformationTheory.klDiv (r s) gamma ≠ ⊤ ∧
        MemLp (gradient (rho s)) 2 (r s) ∧
        (_root_.InformationTheory.klDiv (r s) gamma).toReal ≤
          (1/2 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s) := by
  obtain ⟨p, hpm, hstat, huniq, hk⟩ :=
    StandardizedRGORelativeEntropy.standardized_rgo_unique_prox_and_finite_entropy
      hκ hV hH heta hy hpos
  obtain ⟨p', hpm', hstat', hd⟩ :=
    StandardizedRGOSqrtDensity.standardized_rgo_sqrt_density_domain
      hκ hV hH heta hy hpos
  have hp : p'=p := funext (fun s => huniq s (p' s) (hstat' s))
  rw [hp] at hd
  let rho := fun s u => V (p s+Real.sqrt (eta s) • u)-V (p s)-
    Real.sqrt (eta s)*inner ℝ (gradient V (p s)) u
  let mu := (volume : Measure E).tilted (fun x => -V x)
  let R := fun s => mu.tilted (fun x => -‖x-y s‖^2/(2*eta s))
  let r := fun s => (R s).map (fun x => (Real.sqrt (eta s))⁻¹ • (x-p s))
  let gamma := stdGaussian E
  let Z := fun s => ∫ u, Real.exp (-rho s u) ∂gamma
  let q := fun s u => Real.exp (-rho s u)/Z s
  let f := fun s u => Real.exp (-rho s u/2)/Real.sqrt (Z s)
  refine ⟨p, hpm, hstat, huniq, ?_⟩
  change ∀ s, IsProbabilityMeasure (r s) ∧ r s ≪ gamma ∧
    _root_.InformationTheory.klDiv (r s) gamma ≠ ⊤ ∧
    MemLp (gradient (rho s)) 2 (r s) ∧
    (_root_.InformationTheory.klDiv (r s) gamma).toReal ≤
      (1/2 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s)
  intro s
  obtain ⟨hZpos, hZle, hrtilt, hrden, hprob, hq, hmass, hfC, hf2,
    hg2, hrho2, hqint, hgf, hglog, he⟩ := hd s
  obtain ⟨hac, hfin, hllr, hlog, hrhoint, hKLq, hKLrho⟩ := hk s
  change (∫ u, q s u ∂gamma)=1 at hmass
  change (∫ u, ‖gradient (f s) u‖^2 ∂gamma) =
    (1/4 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s) at he
  change (_root_.InformationTheory.klDiv (r s) gamma).toReal =
    (∫ u, q s u*Real.log (q s u) ∂gamma) at hKLq
  have hsq : ∀ u, (f s u)^2=q s u := fun u => (hq u).2
  have hphi : Integrable (fun u => (f s u)^2*Real.log ((f s u)^2)) gamma := by
    simpa only [hsq] using hqint
  have hLSI := AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianLogSobolev.gaussian_logSobolev_of_contDiff
    (f s) hfC hf2 hg2 hphi
  change (∫ u, (f s u)^2*Real.log ((f s u)^2) ∂gamma) -
    (∫ u, (f s u)^2 ∂gamma)*Real.log (∫ u, (f s u)^2 ∂gamma) ≤
    2 * ∫ u, ‖gradient (f s) u‖^2 ∂gamma at hLSI
  refine ⟨hprob, hac, hfin, hrho2, ?_⟩
  calc
    _ = ∫ u, q s u*Real.log (q s u) ∂gamma := hKLq
    _ ≤ 2 * ∫ u, ‖gradient (f s) u‖^2 ∂gamma := by
      simpa only [hsq, hmass, Real.log_one, mul_zero, sub_zero] using hLSI
    _ = (1/2 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s) := by
      rw [he]
      ring

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOKLFisher

Open AutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StandardizedRGOKLFisher.lean:19published source at ed709a7f320d

Proof architecture

SPHMC actual standardized posterior; no SALD admission

Lean proof walkthrough

• Read the quantified variables and typeclass brackets as part of the mathematical statement; inferred arguments are not missing assumptions.
• `intro` introduces quantified hypotheses into the local proof context.
• `have` creates a named intermediate mathematical fact.
• `calc` records an equality or inequality chain matching a paper calculation.
• `rw` rewrites by an established identity.
• `refine` instantiates a reusable theorem while leaving explicit subgoals.
• `simpa` closes the goal after a controlled simplification of a typed result.

Why the statement has this shape

The declaration is kept at the reusable level recorded by its Registry tags and direct consumers. Explicit measures, spaces, wrappers, and regularity hypotheses expose interfaces that paper notation often infers. A theorem card explains those interfaces but never widens the compiled statement.

Hidden assumptions and non-claims

• Measurability is represented explicitly or must be supplied by a dependency.
• Integrability is an input or proved output; a displayed integral alone does not supply it.
• Totalized `fderiv` values must not be read as a differentiability theorem.
• Almost-everywhere hypotheses depend on the stated measure and representative.
• Density statements retain normalization and absolute-continuity prerequisites.