Allpositive-step true standardized RGO position and Fisher

Produce the true proximal point and base law; Differentiate the literal standardized potential; Derive actual curvature and the mode; Produce genuine Q normalization and the position moment; Identify the literal true RGO law; Prove the pointwise gradient comparison; Integrate under the actual standardized posterior

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_position_and_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) ∧
      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 Q := fun s u => ‖u‖^2/2+rho 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))
      IsProbabilityMeasure mu ∧
        ∀ s, IsProbabilityMeasure (R s) ∧
          ContDiff ℝ 2 (rho s) ∧ ContDiff ℝ 2 (Q s) ∧
          gradient (rho s) 0=0 ∧ gradient (Q s) 0=0 ∧
          (∀ u v : E, 0 ≤ fderiv ℝ (fderiv ℝ (rho s)) u v v ∧
            fderiv ℝ (fderiv ℝ (rho s)) u v v ≤ eta s*‖v‖^2) ∧
          (∀ u v : E, ‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (Q s)) u v v ∧
            fderiv ℝ (fderiv ℝ (Q s)) u v v ≤ (1+eta s)*‖v‖^2) ∧
          r s=(volume : Measure E).tilted (fun u => -Q s u) ∧
          IsProbabilityMeasure (r s) ∧ MemLp id 2 (r s) ∧
          Integrable (fun u => ‖u‖^2) (r s) ∧
          (∫ u, ‖u‖^2 ∂r s) ≤ Module.finrank ℝ E ∧
          MemLp (gradient (rho s)) 2 (r s) ∧
          (∫ u, ‖gradient (rho s) u‖^2 ∂r s) ≤
            (eta s)^2*(∫ u, ‖u‖^2 ∂r s) ∧
          (∫ u, ‖gradient (rho s) u‖^2 ∂r s) ≤
            (eta s)^2*Module.finrank ℝ E := by
  have ha : 0<κ⁻¹ := inv_pos.mpr (lt_of_lt_of_le zero_lt_one hκ)
  have hiV := AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability.integrable_exp_neg_of_strongConvexOn
    ha (hV.differentiable (by norm_num))
    (AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity.strongConvexOn_univ_of_fderiv2_lower hV (fun x v => (hH x v).1))
  let mu := (volume : Measure E).tilted (fun x => -V x)
  have hmu : IsProbabilityMeasure mu := isProbabilityMeasure_tilted hiV
  have : IsProbabilityMeasure mu := hmu
  obtain ⟨p,hpm,heq,_hrest⟩ := FullRangeProximalGaussianOracle.full_range_proximal_gaussian_oracle
    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 Q := fun s u => ‖u‖^2/2+rho s u
  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))
  refine ⟨p,hpm,heq,?_⟩
  change IsProbabilityMeasure mu ∧ _
  refine ⟨hmu,?_⟩
  intro s
  have hη : 0<eta s := hpos s
  obtain ⟨hρ,hQ,hρ0,hQ0,hρdd,hQdd⟩ := actual_standardized_calculus hV (p s) (hpos s)
  have hrhoH : ∀ u v : E, 0 ≤ fderiv ℝ (fderiv ℝ (rho s)) u v v ∧
      fderiv ℝ (fderiv ℝ (rho s)) u v v ≤ eta s*‖v‖^2 := by
    intro u v
    rw [hρdd]
    constructor
    · exact mul_nonneg (hpos s).le ((mul_nonneg ha.le (sq_nonneg ‖v‖)).trans (hH _ v).1)
    · exact mul_le_mul_of_nonneg_left (hH _ v).2 (hpos s).le
  have hQH : ∀ u v : E, ‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (Q s)) u v v ∧
      fderiv ℝ (fderiv ℝ (Q s)) u v v ≤ (1+eta s)*‖v‖^2 := by
    intro u v
    rw [hQdd]
    constructor
    · exact le_add_of_nonneg_right (mul_nonneg (hpos s).le ((mul_nonneg ha.le (sq_nonneg ‖v‖)).trans (hH _ v).1))
    · nlinarith [mul_le_mul_of_nonneg_left (hH (p s+Real.sqrt (eta s) • u) v).2 (hpos s).le]
  let beta : ℝ≥0 := ⟨1+eta s,by positivity⟩
  have hβ : (1:ℝ≥0)≤beta := by change 1≤1+eta s; linarith [hpos s]
  have hHQ : ∀ u v : E, ((1:ℝ≥0):ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (Q s)) u v v ∧
      fderiv ℝ (fderiv ℝ (Q s)) u v v ≤ (beta:ℝ)*‖v‖^2 := by
    change ∀ u v : E, 1*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (Q s)) u v v ∧
      fderiv ℝ (fderiv ℝ (Q s)) u v v ≤ (1+eta s)*‖v‖^2
    simpa only [one_mul] using hQH
  obtain ⟨hqp,hiq,_hqpos,hip,_hpair,_heqd,hbd⟩ :=
    GibbsPositionMoment.gibbs_position_moment (by norm_num : (0:ℝ≥0)<1) hβ hQ hHQ (0:E) hQ0
  have hlaw : r s=(volume : Measure E).tilted (fun u => -Q s u) :=
    actual_standardized_law V (hpos s) (p s) (y s) (heq s) hiV hiq hqp
  have hpr : IsProbabilityMeasure (r s) := hlaw.symm ▸ hqp
  have hipos : Integrable (fun u => ‖u‖^2) (r s) := by
    rw [hlaw]
    simpa only [sub_zero] using hip
  have hbound : (∫ u, ‖u‖^2 ∂r s) ≤ Module.finrank ℝ E := by
    rw [hlaw]
    simpa only [sub_zero,NNReal.coe_one,div_one] using hbd
  have hlp : MemLp id 2 (r s) :=
    (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr hipos
  let b : ℝ≥0 := ⟨eta s,(hpos s).le⟩
  have hHρ : ∀ u v : E, ((0:ℝ≥0):ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (rho s)) u v v ∧
      fderiv ℝ (fderiv ℝ (rho s)) u v v ≤ (b:ℝ)*‖v‖^2 := by
    change ∀ u v : E, 0*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (rho s)) u v v ∧
      fderiv ℝ (fderiv ℝ (rho s)) u v v ≤ eta s*‖v‖^2
    simpa only [zero_mul] using hrhoH
  have hlip : LipschitzWith b (gradient (rho s)) := by
    simpa only [NNReal.coe_zero,zero_div,zero_mul,add_zero] using (AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization.strongConvexOn_and_lipschitzWith_gradient_add_quadratic
      (r:=0) hρ hHρ (0:E)).2
  have hpoint (u : E) : ‖gradient (rho s) u‖^2 ≤ (eta s)^2*‖u‖^2 := by
    have h := hlip.norm_sub_le u 0
    rw [hρ0,sub_zero,sub_zero] at h
    have hs := (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (hpos s).le (norm_nonneg u))).mpr h
    simpa only [mul_pow] using hs
  have hgcont : Continuous (gradient (rho s)) := hlip.continuous
  have hif : Integrable (fun u => ‖gradient (rho s) u‖^2) (r s) := by
    apply (hipos.const_mul ((eta s)^2)).mono' (by fun_prop)
    filter_upwards with u
    rw [Real.norm_eq_abs,abs_of_nonneg (sq_nonneg _)]
    exact hpoint u
  have hlf : MemLp (gradient (rho s)) 2 (r s) :=
    (memLp_two_iff_integrable_sq_norm hgcont.aestronglyMeasurable).mpr hif
  have hfp : (∫ u, ‖gradient (rho s) u‖^2 ∂r s) ≤
      (eta s)^2*(∫ u, ‖u‖^2 ∂r s) := by
    rw [← integral_const_mul]
    exact integral_mono hif (hipos.const_mul ((eta s)^2)) hpoint
  have hfd : (∫ u, ‖gradient (rho s) u‖^2 ∂r s) ≤ (eta s)^2*Module.finrank ℝ E :=
    hfp.trans (mul_le_mul_of_nonneg_left hbound (sq_nonneg _))
  have hiR : Integrable (fun x => Real.exp (-‖x-y s‖^2/(2*eta s))) mu := by
    apply (integrable_const (1:ℝ)).mono' (by fun_prop)
    filter_upwards with x
    rw [Real.norm_eq_abs,abs_of_nonneg (Real.exp_pos _).le]
    apply Real.exp_le_one_iff.mpr
    exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) (by positivity)
  have hRp : IsProbabilityMeasure (R s) := isProbabilityMeasure_tilted hiR
  exact ⟨hRp,hρ,hQ,hρ0,hQ0,hrhoH,hQH,hlaw,hpr,hlp,hipos,hbound,hlf,hfp,hfd⟩

end
end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOPositionFisher

Exact module and namespace context