Actual normalized reference and returned sampling precision

Chain rules,actual first-hit parent,positive strong-convex Gibbs normalization,Haar substitution,product maps,and arbitrary-coupling infimum scaling.

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 normalized_reference_call [FiniteDimensional ℝ E]
    [MeasurableSpace E] [BorelSpace E] {U : E → ℝ} {α β : ℝ≥0}
    (hα : 0 < α) (hαβ : α ≤ β) (hU : ContDiff ℝ 2 U)
    (hH : ∀ x v : E, (α:ℝ)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ U) x v v ∧
      fderiv ℝ (fderiv ℝ U) x v v ≤ (β:ℝ)*‖v‖^2)
    {η τ r : ℝ} (hη : 0 ≤ η) (hτ : 0 < τ) (hr : 0 ≤ r)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (ν : Measure E) [IsProbabilityMeasure ν]
    (hw : TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance ν
      (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
        ((volume : Measure E).tilted (fun x => -U x)) (Real.sqrt η)) ^ 2 ≤ ENNReal.ofReal (r^2)) :
    let d : ℝ := Module.finrank ℝ E
    let A := η+τ
    let a := (α:ℝ)+A⁻¹
    let c := (β:ℝ)+A⁻¹
    let k := c/a
    let u := fun p : E × E => p.1+Real.sqrt τ • p.2
    let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
    let T := fun p x => x-c⁻¹ • gradient (F p) x
    let N := actualIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
    let out := fun p => (T p)^[N p] p.1
    let S := fun x : E => Real.sqrt c • x
    let R := fun x : E => (Real.sqrt c)⁻¹ • x
    let G := fun p x => F p (R x)
    let π := fun p => (volume : Measure E).tilted (fun x => -F p x)
    let πbar := fun p => (volume : Measure E).tilted (fun x => -G p x)
    Measurable N ∧ Measurable (fun p => S (out p)) ∧
    (∀ p, ‖gradient (F p) (out p)‖^2 ≤ a*d ∧
      (∀ j < N p, a*d < ‖gradient (F p) ((T p)^[j] p.1)‖^2) ∧
      ‖gradient (G p) (S (out p))‖^2 ≤ d/k ∧
      ContDiff ℝ 2 (G p) ∧
      (∀ x v, (a/c)*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (G p)) x v v ∧
        fderiv ℝ (fderiv ℝ (G p)) x v v ≤ ‖v‖^2) ∧
      Integrable (fun x => Real.exp (-F p x)) (volume : Measure E) ∧
      0 < ∫ x : E, Real.exp (-F p x) ∧ IsProbabilityMeasure (π p) ∧
      Integrable (fun x => Real.exp (-G p x)) (volume : Measure E) ∧
      0 < ∫ x : E, Real.exp (-G p x) ∧ IsProbabilityMeasure (πbar p) ∧
      (π p).map S = πbar p ∧
      (∀ x, gradient (G p) (S x) = (Real.sqrt c)⁻¹ • gradient (F p) x) ∧
      (∀ t : ℝ, 0 ≤ t →
        (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing (πbar p) (Real.sqrt t)).map R =
          TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing (π p) (Real.sqrt (t/c))) ∧
      (∀ (νbar : Measure E) (t B : ℝ), IsProbabilityMeasure νbar → 0 ≤ t → 0 ≤ B →
        TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance νbar
          (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing (πbar p) (Real.sqrt t)) ^ 2 ≤
            ENNReal.ofReal B →
        TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance (νbar.map R)
          (TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing (π p) (Real.sqrt (t/c))) ^ 2 ≤
            ENNReal.ofReal (B/c))) := by
  let d : ℝ := Module.finrank ℝ E
  let A := η+τ
  let a := (α:ℝ)+A⁻¹
  let c := (β:ℝ)+A⁻¹
  let k := c/a
  let u := fun p : E × E => p.1+Real.sqrt τ • p.2
  let F := fun p x => U x+A⁻¹/2*‖x-u p‖^2
  let T := fun p x => x-c⁻¹ • gradient (F p) x
  let N := actualIndex T (fun p x => ‖gradient (F p) x‖^2) (a*d)
  let out := fun p => (T p)^[N p] p.1
  let S := fun x : E => Real.sqrt c • x
  let R := fun x : E => (Real.sqrt c)⁻¹ • x
  let G := fun p x => F p (R x)
  have hA : 0 < A := add_pos_of_nonneg_of_pos hη hτ
  have ha : 0 < a := add_pos_of_nonneg_of_pos α.coe_nonneg (inv_pos.mpr hA)
  have hc : 0 < c := add_pos_of_nonneg_of_pos β.coe_nonneg (inv_pos.mpr hA)
  have hs : 0 < Real.sqrt c := Real.sqrt_pos.mpr hc
  have hi : (Real.sqrt c)⁻¹^2=c⁻¹ := by rw [inv_pow,Real.sq_sqrt hc.le]
  have hP := JointReferenceGradientDescent.joint_reference_gradient_descent
    hα hαβ hU hH hη hτ hr hd ν hw
  have hNm : Measurable N := hP.1
  have hom : Measurable out := hP.2.1
  refine ⟨hNm,(by fun_prop : Measurable S).comp hom,fun p => ?_⟩
  have hreg := regularized_hessian hU A⁻¹ (u p)
  have hFH (x v : E) : a*‖v‖^2 ≤ fderiv ℝ (fderiv ℝ (F p)) x v v ∧
      fderiv ℝ (fderiv ℝ (F p)) x v v ≤ c*‖v‖^2 := by
    rw [hreg.2]
    dsimp [a,c]
    constructor <;> nlinarith [(hH x v).1,(hH x v).2]
  obtain ⟨hG,hGH,hI,hZ,hprob,hIG,hZG,hprobG,hmap,hgrad,hsm,hprec⟩ :=
    normalized_laws ha hc hreg.1 hFH
  have hp : ‖gradient (F p) (out p)‖^2 ≤ a*d := (hP.2.2.1 p).1
  have hearly : ∀ j < N p, a*d < ‖gradient (F p) ((T p)^[j] p.1)‖^2 :=
    (hP.2.2.1 p).2.2.2.1
  refine ⟨hp,hearly,?_,hG,hGH,hI,hZ,hprob,hIG,hZG,hprobG,hmap,hgrad,hsm,
    fun νbar t B _ ht _ hbudget => hprec νbar t B ht hbudget⟩
  rw [hgrad,norm_smul,Real.norm_eq_abs,mul_pow,sq_abs,hi]
  have hb := mul_le_mul_of_nonneg_left hp (inv_pos.mpr hc).le
  calc
    c⁻¹*‖gradient (F p) (out p)‖^2 ≤ c⁻¹*(a*d) := hb
    _ = d/k := by dsimp [k]; field_simp

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.NormalizedReferenceCall

Exact module and namespace context