The five local conditions for the density–log-density pairing

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.DirichletPairDomain · structure · Teaching coverage

Statement

For any index type ι, let E be EuclideanSpace ℝ ι with its coordinate measurable structure, let μ and π be arbitrary measures on E, and let L be a real-linear operator on real-valued functions. For the fixed selected RN density ρ and log-ratio r, DirichletPairDomain means exactly that L(ρr), ρLr, and rLρ are π-integrable, the integral of L(ρr) is zero, and the integrals of ρLr and rLρ are equal. Constructing this domain requires five proofs. This is a condition on one ordered pair, not global stationarity or reversibility. Finiteness of ι is required by the later score/gradient bridges, not by this pair-domain structure.

All objects and hypotheses

• ι is an arbitrary index type, and E = EuclideanSpace ℝ ι is used only as a measurable coordinate space in this structure. There is no Fintype or Nonempty ι parameter in its compiler-exported signature.
• μ and π are arbitrary measures on E. No probability, finite-total-mass, or normalization hypothesis is present.
• Use the exact selected functions ρ(x) = (μ.rnDeriv π x).toReal and r(x) = RNLogRatio.logRatio μ π x = MeasureTheory.llr μ π x = Real.log(ρ(x)). They remain fixed by the original ordered pair (μ,π); no gradient is used in this pair-domain definition.
• L is a real-linear map from all functions E → ℝ to all functions E → ℝ. Its linearity alone does not say that it generates a Markov semigroup, preserves a measure, or is a diffusion.
• The definition takes μ, π and L only. Neither absolute continuity, σ-finiteness, score differentiability, score integrability nor the canonical Γ identity is included unless supplied separately.
• Every product of functions is pointwise: (ρr)(x)=ρ(x)r(x). All three integrability claims and both integral identities refer to π.

Construction and meaning

structure DirichletPairDomain
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop where
  generator_product_integrable :
    Integrable
      (generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi)) pi
  density_mul_generator_logRatio_integrable :
    Integrable
      (fun x => RNLogRatio.density mu pi x *
        generator (RNLogRatio.logRatio mu pi) x) pi
  logRatio_mul_generator_density_integrable :
    Integrable
      (fun x => RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x) pi
  stationary_product :
    (∫ x,
      generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi) x ∂pi) = 0
  symmetric_pair :
    (∫ x, RNLogRatio.density mu pi x *
      generator (RNLogRatio.logRatio mu pi) x ∂pi) =
      ∫ x, RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x ∂pi

/-- The concrete carré-du-champ identification required to turn the abstract
Dirichlet form into canonical relative Fisher information.

For overdamped Langevin this is the measure-domain version of
`Gamma(f,g)=inner (grad f) (grad g)` together with the score chain rule for the
canonical density.  It is kept as a separate contract because absolute
continuity alone gives no differentiability of an RN representative. -/

structure DirichletPairDomain
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop where
  generator_product_integrable :
    Integrable
      (generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi)) pi
  density_mul_generator_logRatio_integrable :
    Integrable
      (fun x => RNLogRatio.density mu pi x *
        generator (RNLogRatio.logRatio mu pi) x) pi
  logRatio_mul_generator_density_integrable :
    Integrable
      (fun x => RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x) pi
  stationary_product :
    (∫ x,
      generator
        (RNLogRatio.density mu pi * RNLogRatio.logRatio mu pi) x ∂pi) = 0
  symmetric_pair :
    (∫ x, RNLogRatio.density mu pi x *
      generator (RNLogRatio.logRatio mu pi) x ∂pi) =
      ∫ x, RNLogRatio.logRatio mu pi x *
        generator (RNLogRatio.density mu pi) x ∂pi

/-- The concrete carré-du-champ identification required to turn the abstract
Dirichlet form into canonical relative Fisher information.

For overdamped Langevin this is the measure-domain version of
`Gamma(f,g)=inner (grad f) (grad g)` together with the score chain rule for the
canonical density.  It is kept as a separate contract because absolute
continuity alone gives no differentiability of an RN representative. -/

Scope and omitted-condition boundaries

• These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
• Real.log and ENNReal.toReal are totalized (log 0 = 0 and ∞.toReal = 0). Without the separately stated decomposition/σ-finiteness/absolute-continuity assumptions, this notation alone is not a theorem that ρ represents dμ/dπ with a finite positive value.
• This structure does not assert membership in a separately defined closed Dirichlet-form or Sobolev domain. It does not provide the score-domain witness or the Γ-to-score identity.
• No probability assumption or finite total mass is part of this local domain.
• A focused compiler signature check confirmed that ambient Fintype is not retained for this structure. The finite-dimensional assumptions of the later Fisher bridge must not be copied back into this definition.