ReferenceCarryingCost: mathematical reading route

Genuine current Hessian, original-coordinate W2 input, existing actual first-hit count, source/completed-square index identity, measurable zero-cost branch and actual kernel integral calculus.

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 reference_carrying_cost [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
    {V : E → ℝ} {α β : ℝ≥0} (hα : 0 < α) (hαβ : α ≤ β)
    (hV : ContDiff ℝ 2 V)
    (hH : ∀ x w : E, (α:ℝ)*‖w‖^2 ≤ fderiv ℝ (fderiv ℝ V) x w w ∧
      fderiv ℝ (fderiv ℝ V) x w w ≤ (β:ℝ)*‖w‖^2)
    (hd : 0 < (Module.finrank ℝ E : ℝ))
    (η τ ε : RefState E → ℝ) (hη : Measurable η) (hτ : Measurable τ)
    (hη0 : ∀ s, 0 < η s) (hτ0 : ∀ s, 0 < τ s)
    (M : Kernel (RefState E) E) [IsMarkovKernel M] (threshold : ℝ≥0)
    (hw : ∀ s : RefState E, s.1 < threshold →
      AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpace.wassersteinDistance (M s)
        (AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothing.gaussianSmoothing
          ((volume : Measure E).tilted (fun x => -(V x+(s.1:ℝ)/2*‖x-s.2.1‖^2)))
          (Real.sqrt (η s/((β:ℝ)+s.1)))) ^ 2 ≤
        ENNReal.ofReal ((((β:ℝ)+s.1)/((α:ℝ)+s.1))*(ε s)^2/((β:ℝ)+s.1))) :
    let d : ℝ := Module.finrank ℝ E
    let bs := fun s : RefState E => (β:ℝ)+s.1
    let a := fun s : RefState E => (α:ℝ)+s.1
    let v := fun s => (η s+τ s)/bs s
    let bp := fun s : RefState E => s.1+Real.toNNReal (v s)⁻¹
    let obs := fun p : RefState E × (E × E) => p.2.1+Real.sqrt (τ p.1/bs p.1) • p.2.2
    let center := fun p : RefState E × (E × E) => (bp p.1:ℝ)⁻¹ •
      ((p.1.1:ℝ) • p.1.2.1+(v p.1)⁻¹ • obs p)
    let F := fun p x => V x+(bp p.1:ℝ)/2*‖x-center p‖^2
    let T := fun p x => x-((β:ℝ)+bp p.1)⁻¹ • gradient (F p) x
    let q := fun n p => ‖gradient (F p) ((T p)^[n] p.2.1)‖^2
    let N := firstIndex q (fun p => ((α:ℝ)+bp p.1)*d)
    let C := fun p : RefState E × (E × E) => if threshold ≤ p.1.1 then 0 else (N p:ℝ)+1
    let B := fun s : RefState E => if threshold ≤ s.1 then 0 else
      2+(((β:ℝ)+bp s)/((α:ℝ)+bp s))*Real.log
        (1+4*(η s+τ s)*(1+η s)+2*(η s+τ s)*(bs s/a s)*(ε s)^2/d+τ s/(η s+τ s))
    let K := M ×ₖ Kernel.const (RefState E) (stdGaussian E)
    Measurable C ∧ (Measurable ε → Measurable B) ∧ (∀ p, 0 ≤ C p) ∧
      (∀ s, Integrable (fun z => C (s,z)) (K s) ∧ (∫ z, C (s,z) ∂K s) ≤ B s) ∧
      (∀ (μ : Measure (RefState E)) [SFinite μ],
        (∫⁻ p, ENNReal.ofReal (C p) ∂μ.compProd K) ≤ ∫⁻ s, ENNReal.ofReal (B s) ∂μ ∧
          (Integrable B μ → Integrable C (μ.compProd K) ∧
            (∫ p, C p ∂μ.compProd K) ≤ ∫ s, B s ∂μ)) := by
  classical
  intro d bs a v bp obs center F T q N C B K
  have R := AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel.reference_carrying_kernel
    hα hαβ hV hH hd η τ hη hτ hη0 hτ0 M threshold
  have hbp (s : RefState E) : (bp s:ℝ)=(s.1:ℝ)+(v s)⁻¹ := (R.1 s).2
  have hNm : Measurable N := R.2.1
  have hCm : Measurable C := by
    apply Measurable.ite (measurableSet_le measurable_const (by fun_prop)) measurable_const
    exact (measurable_from_nat.comp hNm).add measurable_const
  have hC0 (p : RefState E × (E × E)) : 0 ≤ C p := by dsimp [C]; split_ifs <;> positivity
  have hBm (hε : Measurable ε) : Measurable B := by
    dsimp [B,bp,v,bs,a]
    apply Measurable.ite (measurableSet_le measurable_const (by fun_prop)) measurable_const
    fun_prop
  have hK : IsMarkovKernel K := by dsimp [K]; infer_instance
  have hKs (s : RefState E) : K s=(M s).prod (stdGaussian E) := by
    simp only [K,Kernel.prod_apply,Kernel.const_apply]
  have hp (s : RefState E) : Integrable (fun z => C (s,z)) (K s) ∧
      (∫ z, C (s,z) ∂K s) ≤ B s := by
    by_cases hs : threshold ≤ s.1
    · simp only [C,B,if_pos hs,integrable_const,integral_const,smul_zero,le_refl,and_self]
    · have Hs := statewise_cost hα hαβ hV hH hd s.1 s.2.1 (η s) (τ s) (ε s)
        (hη0 s) (hτ0 s) (M s) (hw s (lt_of_not_ge hs))
      let W := fun z : E × E => fun x => V x+(s.1:ℝ)/2*‖x-s.2.1‖^2+
        (v s)⁻¹/2*‖x-(z.1+Real.sqrt (τ s/bs s) • z.2)‖^2
      let Ts := fun z x => x-(bs s+(v s)⁻¹)⁻¹ • gradient (W z) x
      let qs := fun n z => ‖gradient (W z) ((Ts z)^[n] z.1)‖^2
      let Ns := firstIndex qs (fun _ => (a s+(v s)⁻¹)*d)
      have hc : bs s+(v s)⁻¹=(β:ℝ)+bp s := by rw [hbp]; dsimp [bs]; ring
      have ha : a s+(v s)⁻¹=(α:ℝ)+bp s := by rw [hbp]; dsimp [a]; ring
      have hq (n : ℕ) (z : E × E) : qs n z=q n (s,z) := by
        have hz := R.2.2.2.2.1 (s,z)
        have ht := hz.2.2.2.2.2.1 n
        have hg := hz.2.2.2.2.1
        change (fun x => x-((β:ℝ)+bp s)⁻¹ • gradient (W z) x)^[n] z.1 =
          (T (s,z))^[n] z.1 at ht
        dsimp only [qs,Ts]
        rw [hc,ht]
        exact congrArg (fun w : E => ‖w‖^2) (hg _)
      have hN (z : E × E) : Ns z=N (s,z) := by
        dsimp only [Ns,N,firstIndex]
        simp only [hq,ha]
      change Integrable (fun z => (Ns z:ℝ)+1) ((M s).prod (stdGaussian E)) ∧
        (∫ z, (Ns z:ℝ)+1 ∂(M s).prod (stdGaussian E)) ≤
          2+((bs s+(v s)⁻¹)/(a s+(v s)⁻¹))*Real.log _ at Hs
      simp_rw [hN] at Hs
      simpa only [C,B,if_neg hs,hKs,hc,ha] using Hs
  exact ⟨hCm,hBm,hC0,hp,fun μ => integrate_actual_cost K C B hCm hC0
    (fun s => (hp s).1) (fun s => (hp s).2) μ⟩

end AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingCost

Exact module and namespace context