P5: Doob transform skeleton (API only)

We provide a lightweight Diffusion structure and a Doob transform shell. Heavy analysis (Leibniz, Hessian calculus) is deferred. Key identities are stated as Prop so CI remains light.

structure Frourio.DoobDegradation : Type

Doob transform effect on curvature-dimension parameter. The BE degradation: λ ↦ λ - 2ε(h) where h > 0 is the Doob function. In BE theory, ε(h) measures the curvature degradation:

• ε(h) = sup_φ {∫ Γ₂(log h, φ) dμ / ‖φ‖²}
• ε(h) = 0 iff h is log-harmonic (∇²(log h) = 0) The transformed measure is dμ_h = h²dμ.

• ε : ℝ

  The degradation amount ε(h) from the Doob function h

• ε_nonneg : 0 ≤ self.ε

  Non-negativity (always true in BE theory)

• degraded_lambda : ℝ → ℝ

  The degraded parameter after Doob transform

structure Frourio.Diffusion (X : Type u_1) : Type u_1

• E : (X → ℝ) → ℝ
• L : (X → ℝ) → X → ℝ
• Gamma : (X → ℝ) → X → ℝ
• Gamma2 : (X → ℝ) → X → ℝ

def Frourio.HasCD {X : Type u_1} (D : Diffusion X) (lam : ℝ) : Prop

Curvature-dimension predicate (pointwise Γ₂ bound). HasCD D λ encodes a Bakry–Émery type lower bound in the CD(λ, ∞) form: for all test functions f and points x, one has Γ₂(f)(x) ≥ λ · Γ(f)(x). This concrete predicate keeps the API light while allowing downstream theorems to reference an actual inequality.

Equations

• Frourio.HasCD D lam = ∀ (f : X → ℝ) (x : X), D.Gamma2 f x ≥ lam * D.Gamma f x

noncomputable def Frourio.gammaPair {X : Type u_1} (D : Diffusion X) (f g : X → ℝ) : X → ℝ

Symmetric bilinear form associated to Gamma by polarization. This provides a concrete Γ(f,g) using the unary Γ available in Diffusion.

Equations

• Frourio.gammaPair D f g x = (D.Gamma (fun (y : X) => f y + g y) x - D.Gamma f x - D.Gamma g x) / 2

def Frourio.HasLeibnizL {X : Type u_1} (D : Diffusion X) : Prop

Minimal Leibniz rule for the generator L using gammaPair for the cross term. This is a concrete predicate, not a placeholder.

Equations

• Frourio.HasLeibnizL D = ∀ (f g : X → ℝ), (D.L fun (x : X) => f x * g x) = fun (x : X) => f x * D.L g x + g x * D.L f x - 2 * Frourio.gammaPair D f g x

def Frourio.HasLeibnizGamma {X : Type u_1} (D : Diffusion X) : Prop

Product rule for Γ in a minimal concrete form via gammaPair.

Equations

• Frourio.HasLeibnizGamma D = ∀ (f g : X → ℝ), (D.Gamma fun (x : X) => f x * g x) = fun (x : X) => f x ^ 2 * D.Gamma g x + g x ^ 2 * D.Gamma f x + 2 * f x * g x * Frourio.gammaPair D f g x

noncomputable def Frourio.doobL {X : Type u_1} (D : Diffusion X) (h : X → ℝ) : (X → ℝ) → X → ℝ

Equations

• Frourio.doobL D h f x = if h x = 0 then 0 else 1 / h x * D.L (fun (y : X) => h y * f y) x

noncomputable def Frourio.Doob {X : Type u_1} (h : X → ℝ) (D : Diffusion X) : Diffusion X

Equations

• Frourio.Doob h D = { E := D.E, L := Frourio.doobL D h, Gamma := D.Gamma, Gamma2 := D.Gamma2 }

structure Frourio.DoobAssumptions {X : Type u_1} (h : X → ℝ) (D : Diffusion X) : Type

• h_pos (x : X) : 0 < h x

  Strict positivity of h ensuring the Doob transform is well-defined.

• leibniz_L : HasLeibnizL D

  Concrete Leibniz rule for the generator.

• leibniz_Gamma : HasLeibnizGamma D

  Concrete product rule for Γ.

• gamma_eq : (Doob h D).Gamma = D.Gamma
• gamma2_eq (f : X → ℝ) : (Doob h D).Gamma2 f = D.Gamma2 f
• cd_shift (lam : ℝ) : HasCD D lam → ∃ (lam' : ℝ), HasCD (Doob h D) lam' ∧ lam' ≤ lam

  Curvature-dimension shift: for any CD parameter lam of D, there exists a possibly degraded parameter lam' for Doob h D with lam' ≤ lam. Later phases will refine this to an explicit formula using ∇² log h.

• BE_degradation : ℝ

  BE degradation for meta-variational principle: λ_eff ≥ λ - 2ε(h). This field provides the degradation amount ε(h) ≥ 0 from the Hessian of log h.

• BE_degradation_nonneg : 0 ≤ self.BE_degradation

  Non-negativity of degradation

• cd_shift_explicit (lam : ℝ) : HasCD D lam → HasCD (Doob h D) (lam - 2 * self.BE_degradation)

  The cd_shift explicitly uses BE_degradation: Doob h D satisfies CD(λ - 2*BE_degradation)

def Frourio.BochnerMinimal {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (eps : ℝ) : Prop

Minimal Bochner-style correction statement needed to realize the explicit CD parameter shift under a Doob transform. Parameterized by eps from the Hessian bound on log h.

Equations

• Frourio.BochnerMinimal h D eps = ∀ (lam : ℝ), Frourio.HasCD D lam → Frourio.HasCD (Frourio.Doob h D) (lam - 2 * eps)

theorem Frourio.doob_gamma_eq {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) : (Doob h D).Gamma = D.Gamma

Γ identity under Doob transform (theoremized via assumptions).

theorem Frourio.doob_gamma2_eq {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (f : X → ℝ) (H : DoobAssumptions h D) : (Doob h D).Gamma2 f = D.Gamma2 f

Γ₂ identity under Doob transform (theoremized via assumptions). Later phases will relax the equality to the corrected identity under minimal Bochner assumptions.

theorem Frourio.doob_gamma2_eq_all {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (f : X → ℝ) : (Doob h D).Gamma2 f = D.Gamma2 f

Γ₂ identity for all test functions (quantified version).

theorem Frourio.doobL_pointwise {X : Type u_1} (D : Diffusion X) (h : X → ℝ) (H : DoobAssumptions h D) (f : X → ℝ) (x : X) : doobL D h f x = 1 / h x * D.L (fun (y : X) => h y * f y) x

Under strict positivity of h, the Doob generator evaluates without the if guard. This provides a convenient pointwise formula.

theorem Frourio.gammaPair_doob_eq {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (f g : X → ℝ) : gammaPair (Doob h D) f g = gammaPair D f g

Pairwise carré-du-champ agrees under the Doob transform when Γ agrees.

theorem Frourio.hasLeibnizGamma_doob_of_base {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (HG : HasLeibnizGamma D) : HasLeibnizGamma (Doob h D)

If Γ satisfies the product rule for D, then it also does for Doob h D when the Γ fields agree (operator-level compatibility).

theorem Frourio.cd_parameter_shift {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) {lam : ℝ} (hCD : HasCD D lam) : ∃ (lam' : ℝ), HasCD (Doob h D) lam' ∧ lam' ≤ lam

def Frourio.lambdaBE (lam eps : ℝ) : ℝ

Equations

• Frourio.lambdaBE lam eps = lam - 2 * eps

theorem Frourio.lambdaBE_le_base {lam eps : ℝ} (hε : 0 ≤ eps) : lambdaBE lam eps ≤ lam

theorem Frourio.hasCD_doob_of_bochnerMinimal {X : Type u_1} (h : X → ℝ) (D : Diffusion X) {eps lam : ℝ} (HB : BochnerMinimal h D eps) (hCD : HasCD D lam) : HasCD (Doob h D) (lambdaBE lam eps)

theorem Frourio.lambdaBE_from_doobAssumptions {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (_H : DoobAssumptions h D) (lam eps : ℝ) (hCD : HasCD D lam) (hBochner : BochnerMinimal h D eps) : HasCD (Doob h D) (lambdaBE lam eps)

API: Extract the effective curvature parameter λ_BE from DoobAssumptions when we know the Hessian bound parameter ε.

theorem Frourio.lambdaBE_bound_from_doobAssumptions {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (_H : DoobAssumptions h D) (lam eps : ℝ) (heps : 0 ≤ eps) : lambdaBE lam eps ≤ lam

API: The Doob-shifted parameter λ_BE satisfies the expected inequality λ_BE = λ - 2ε ≤ λ when ε ≥ 0.

theorem Frourio.doob_cd_with_lambdaBE {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (lam eps : ℝ) (heps : 0 ≤ eps) (hCD : HasCD D lam) (hBochner : BochnerMinimal h D eps) : HasCD (Doob h D) (lambdaBE lam eps) ∧ lambdaBE lam eps ≤ lam

Combined API: Given DoobAssumptions and BochnerMinimal, we get both the CD property with λ_BE and the bound λ_BE ≤ λ.

structure Frourio.DoobQuantitative {X : Type u_1} (h : X → ℝ) (D : Diffusion X) : Type

Quantitative Doob transform pack: stores an ε ≥ 0 for which the minimal Bochner correction holds. This yields an explicit CD parameter shift λ' = λ − 2ε together with λ' ≤ λ.

• eps : ℝ
• eps_nonneg : 0 ≤ self.eps
• bochner : BochnerMinimal h D self.eps

theorem Frourio.cd_parameter_shift_explicit {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (HQ : DoobQuantitative h D) {lam : ℝ} (hCD : HasCD D lam) : ∃ (lam' : ℝ), lam' = lambdaBE lam HQ.eps ∧ HasCD (Doob h D) lam' ∧ lam' ≤ lam

Explicit CD-parameter shift under the quantitative Doob pack.

theorem Frourio.cd_parameter_shift_explicit_value {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (HQ : DoobQuantitative h D) {lam : ℝ} (hCD : HasCD D lam) : HasCD (Doob h D) (lambdaBE lam HQ.eps) ∧ lambdaBE lam HQ.eps ≤ lam

Pointwise form: from DoobQuantitative, directly obtain the transformed CD bound at the explicit value λ_BE = λ − 2ε along with the monotonicity ≤.

structure Frourio.DoobLamBound : Type

• lamBase : ℝ
• eps : ℝ
• lamEff : ℝ
• h_lamEff : self.lamEff = lambdaBE self.lamBase self.eps

def Frourio.DoobLamBound.mk' (lamBase eps : ℝ) : DoobLamBound

Equations

• Frourio.DoobLamBound.mk' lamBase eps = { lamBase := lamBase, eps := eps, lamEff := Frourio.lambdaBE lamBase eps, h_lamEff := ⋯ }

theorem Frourio.DoobLamBound.le_base {B : DoobLamBound} (hε : 0 ≤ B.eps) : B.lamEff ≤ B.lamBase

theorem Frourio.doob_lambda_eff_formula {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (lam : ℝ) (hCD : HasCD D lam) : ∃ (lam_eff : ℝ), lam_eff = lam - 2 * H.BE_degradation ∧ HasCD (Doob h D) lam_eff ∧ lam_eff ≤ lam

Extended API for meta-variational principle: Connect BE_degradation field to the explicit λ_eff formula.

def Frourio.doob_lambda_eff {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (lam : ℝ) : ℝ

Convenience: extract effective λ for meta-variational principle

Equations

• Frourio.doob_lambda_eff h D H lam = lam - 2 * H.BE_degradation

theorem Frourio.doob_lambda_eff_le {X : Type u_1} (h : X → ℝ) (D : Diffusion X) (H : DoobAssumptions h D) (lam : ℝ) : doob_lambda_eff h D H lam ≤ lam

The effective λ satisfies the expected bound