True standardized RGO square-root density domains

Reuse the true posterior and the same stationary point; Apply the new density-domain producer to that actual residual; Keep the same law in every derivative and energy conclusion

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 standardized_rgo_sqrt_density_domain
    {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) ∧
      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)
      ∀ s, 0 < Z s ∧ Z s ≤ 1 ∧
        r s = gamma.tilted (fun u => -rho s u) ∧
        r s = gamma.withDensity (fun u => ENNReal.ofReal (q s u)) ∧
        IsProbabilityMeasure (r s) ∧
        (∀ u, 0 < q s u ∧ f s u^2 = q s u) ∧
        (∫ u, q s u ∂gamma) = 1 ∧
        ContDiff ℝ 2 (f s) ∧ MemLp (f s) 2 gamma ∧
        MemLp (gradient (f s)) 2 gamma ∧ MemLp (gradient (rho s)) 2 (r s) ∧
        Integrable (fun u => q s u*Real.log (q s u)) gamma ∧
        (∀ u, gradient (f s) u = -(f s u/2) • gradient (rho s) u) ∧
        (∀ u, gradient (fun z => Real.log (q s z)) u = -gradient (rho s) u) ∧
        (∫ u, ‖gradient (f s) u‖^2 ∂gamma) =
          (1/4 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s) := by
  obtain ⟨p,hpm,heq,hparent⟩ :=
    StandardizedRGOPositionFisher.standardized_rgo_position_and_fisher hκ hV hH heta hy hpos
  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,heq,?_⟩
  change ∀ s, 0 < Z s ∧ Z s ≤ 1 ∧ _
  intro s
  obtain ⟨_hRp,hρ,_hQ,hρgrad,_hQgrad,hρH,_hQH,hlaw,_hrest⟩ := hparent.2 s
  have hρzero : rho s 0 = 0 := by simp [rho]
  let L : ℝ≥0 := ⟨eta s,(hpos s).le⟩
  have hHρ : ∀ u v : E, 0 ≤ fderiv ℝ (fderiv ℝ (rho s)) u v v ∧
      fderiv ℝ (fderiv ℝ (rho s)) u v v ≤ (L : ℝ)*‖v‖^2 := hρH
  have hg := AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSqrtDensityDomain.gaussian_sqrt_density_domain
    hρ hρzero hρgrad hHρ
  obtain ⟨hZ,hZone,hvolume,hdensity,hprob,hfq,hqone,hf,hflp,hfglp,hρlp,he,hdf,hdlog,henergy⟩ := hg
  have htrue : r s=gamma.tilted (fun u => -rho s u) := hlaw.trans hvolume.symm
  have hprob' : IsProbabilityMeasure (r s) := htrue.symm ▸ hprob
  have hρlp' : MemLp (gradient (rho s)) 2 (r s) := htrue.symm ▸ hρlp
  have henergy' : (∫ u, ‖gradient (f s) u‖^2 ∂gamma) =
      (1/4 : ℝ)*(∫ u, ‖gradient (rho s) u‖^2 ∂r s) := htrue.symm ▸ henergy
  exact ⟨hZ,hZone,htrue,htrue.trans hdensity,hprob',hfq,hqone,hf,hflp,hfglp,hρlp',
    he,hdf,hdlog,henergy'⟩

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOSqrtDensity

Exact module and namespace context