Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412

CanonicalDirichletFisher: mathematical reading route

Read the statements and derivations in source order. Every result has its own optional Lean statement and proof. Source assumptions, library reuse and unproved boundaries are kept explicit.

  1. The Euclidean space used by the Dirichlet bridge
  2. The five local conditions for the density–log-density pairing
  3. The separate carré-du-champ identification needed for Fisher energy
  4. Identify the density–log-density Dirichlet pairing with guarded Fisher
  5. The same Dirichlet bridge written as an integral under μ
  6. Rewrite a supplied negative-Dirichlet derivative as negative Fisher
ASTIS mathematical exposition

The Euclidean space used by the Dirichlet bridge

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.State · abbrev · Teaching coverage

Statement

For an index type ι, the local name State denotes Mathlib's EuclideanSpace ℝ ι. It is definitionally the same underlying Euclidean type used in the canonical relative-Fisher module; the two namespace-local abbreviations do not create different mathematical spaces. Subsequent analysis in this module is carried out for finite ι.

\[E:=\operatorname{EuclideanSpace}(\mathbb R,\iota),\qquad\mathrm{CanonicalDirichletFisher.State}=\mathrm{CanonicalRelativeFisher.State}=E.\]

All objects and hypotheses

  • ι is any index type for the abbreviation itself; the surrounding section supplies Fintype ι to subsequent finite-dimensional analytic declarations.
  • No measure or generator is an input to this abbreviation. No Nonempty ι hypothesis is present.

Construction and meaning

1. Reuse the Mathlib coordinate space

The local type name unfolds directly to the existing real Euclidean space. Equality of the two local names is definitional, not a constructed transport map between spaces.

\[\mathrm{State}\equiv\operatorname{EuclideanSpace}(\mathbb R,\iota).\]
Corresponding Lean step

EuclideanSpace ℝ ι

Lean statement · State

This declaration is a short name for the coordinate type used by every later density, gradient, and generator in this module. It does not attach a particular measure or choose a dynamics.

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.

abbrev State

Exact module and namespace context

Lean construction · State

There is no proof body: the abbreviation simply expands to Mathlib's type. The inherited finite-dimensional structure is available later because the module works under the finite-index assumption.

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.

abbrev State := EuclideanSpace ℝ ι

/-- The canonical density/log-ratio pair is in the generator integration-by-
parts domain needed to invoke Chewi Theorem 1.2.14.

The fields are exactly the three integrability terms, stationarity of the
product observable, and generator symmetry for this pair.  This is a local
pair contract, not a global reversibility claim. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • This is a namespace-local alias, not a new geometric construction or theorem about changing spaces.
  • No probability normalization, measure invariance, or generator property.

Source and reuse

ASTIS parents called

    Mathlib API called (external library)

    • EuclideanSpace

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    ASTIS mathematical exposition

    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.

    \[\begin{aligned}\mathcal P(\mu,\pi,L)\ :\Longleftrightarrow\;&L(\rho r),\ \rho Lr,\ rL\rho\in L^1(\pi),\\&\int_E L(\rho r)\,d\pi=0,\\&\int_E\rho Lr\,d\pi=\int_ErL\rho\,d\pi.\end{aligned}\]

    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

    1. Check the generator applied to the product

    Supply integrability of the single function L(ρr). This term will be the first summand in the carré-du-champ expansion.

    \[L(\rho r)\in L^1(\pi).\]
    Corresponding Lean step

    DirichletPairDomain.generator_product_integrable

    2. Check the two generator pairings

    Supply integrability of both cross terms separately. One finite integral does not automatically establish the other.

    \[\rho Lr\in L^1(\pi),\qquad rL\rho\in L^1(\pi).\]
    Corresponding Lean step

    DirichletPairDomain.density_mul_generator_logRatio_integrable; DirichletPairDomain.logRatio_mul_generator_density_integrable

    3. Check stationarity only for the product observable

    Supply the identity that the π-integral of L(ρr) vanishes. The definition does not quantify over every observable.

    \[\int_E L(\rho r)\,d\pi=0.\]
    Corresponding Lean step

    DirichletPairDomain.stationary_product

    4. Check symmetry only for this pairing

    Supply equality of the two cross integrals. This is precisely the pair-level equality used in the integral algebra.

    \[\int_E\rho Lr\,d\pi=\int_ErL\rho\,d\pi.\]
    Corresponding Lean step

    DirichletPairDomain.symmetric_pair

    5. Collect the five proofs

    These obligations together form the local domain witness consumed by the later integration-by-parts bridge; none of them is proved by naming the structure.

    \[(h_1,h_2,h_3,h_{\mathrm{stat}},h_{\mathrm{sym}}):\mathcal P(\mu,\pi,L).\]
    Corresponding Lean step

    DirichletPairDomain.mk

    Lean statement · DirichletPairDomain

    This is a proposition with five mathematical fields. The first three prevent invalid subtraction of nonintegrable Bochner integrals. The last two apply only to the selected density and log-ratio, even though their names recall stationarity and symmetry.

    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.

    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. -/

    Exact module and namespace context

    Lean construction · DirichletPairDomain

    A domain witness is built by providing the five required proofs. Declaring L as a linear map does not supply any of them. Once supplied, they match the five hypotheses of the existing integration-by-parts helper exactly.

    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.

    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. -/

    Exact module and namespace context

    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.

    Source and reuse

    ASTIS parents called

    Mathlib API called (external library)

    • LinearMap
    • MeasureTheory.Integrable
    • MeasureTheory.integral

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    ASTIS mathematical exposition

    The separate carré-du-champ identification needed for Fisher energy

    AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.HasCanonicalFisherGamma · def · Teaching coverage

    Statement

    For arbitrary μ and π on finite-dimensional Euclidean space and a real-linear operator L on functions, HasCanonicalFisherGamma is the assertion that, π-almost everywhere, the algebraic carré du champ of the selected density ρ and log-ratio r equals ρ times the squared totalized gradient of r. This equality is a separate input to the bridge, not a chain rule derived by the definition.

    \[\begin{aligned}\Gamma_L(f,g)&:=\tfrac12\big[L(fg)-fLg-gLf\big],\\\operatorname{HasCanonicalFisherGamma}(\mu,\pi,L)&:\Longleftrightarrow\Gamma_L(\rho,r)=\rho\,\|\nabla r\|^2\quad\pi\text{-a.e.}\end{aligned}\]

    All objects and hypotheses

    • ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
    • μ 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)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
    • 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.
    • This proposition is defined without assuming any domain witness, absolute continuity, integrability, σ-finiteness, or differentiability. To use it as a hypothesis, a caller must actually prove its π-a.e. equality.

    Construction and meaning

    1. Evaluate the existing algebraic Γ expression

    Substitute the fixed functions ρ and r into the imported carré-du-champ definition. The factor one-half fixes the normalization.

    \[\Gamma_L(\rho,r)(x)=\tfrac12\big(L(\rho r)(x)-\rho(x)Lr(x)-r(x)L\rho(x)\big).\]
    Corresponding Lean step

    StochasticProcesses.CarreDuChamp.carreDuChamp generator (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)

    2. Form the intended score-energy density

    Multiply the same selected ρ by the squared gradient of the same selected r. No derivative of ρ or chain rule is assumed merely by writing this expression.

    \[\rho(x)q(x)=\rho(x)\|\nabla r(x)\|^2.\]
    Corresponding Lean step

    RNLogRatio.density mu pi x * CanonicalRelativeFisher.scoreSq mu pi x

    3. Require equality outside a π-null set

    Define the proposition by the a.e. comparison of these expressions. A concrete diffusion must supply its proof; a pointwise identity everywhere is not required.

    \[\Gamma_L(\rho,r)=\rho q\quad\pi\text{-a.e.}.\]
    Corresponding Lean step

    ∀ᵐ x ∂pi, ...

    Lean statement · HasCanonicalFisherGamma

    The result is a proposition saying that two functions agree almost everywhere for π, the reference measure. It differs from the score-domain differentiability condition, whose exceptional set is measured by μ. The statement itself includes no integrability or regularity proof.

    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.

    def HasCanonicalFisherGamma
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop

    Exact module and namespace context

    Lean construction · HasCanonicalFisherGamma

    The body spells out the desired a.e. equality using the already-defined algebraic Γ, selected RN functions, and squared score. It does not establish the equality. In an eventual concrete model, the appropriate diffusion formula and representative-valid chain rule must justify it.

    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.

    def HasCanonicalFisherGamma
    (mu pi : Measure (State (ι := ι)))
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ)) : Prop :=
  ∀ᵐ x ∂pi,
    StochasticProcesses.CarreDuChamp.carreDuChamp generator
      (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) x =
      RNLogRatio.density mu pi x *
        CanonicalRelativeFisher.scoreSq mu pi x

/-- Chewi Theorem 1.2.14 plus the concrete Gamma/score identification gives
exactly the canonical relative Fisher information:

`E_pi(dmu/dpi, log(dmu/dpi)) = FI(mu || pi)`.

This is the reusable Dirichlet--Fisher edge consumed by KL dissipation and by
the generator form of log-Sobolev inequalities. -/

    Exact module and namespace context

    Scope and omitted-condition boundaries

    • This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
    • These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
    • No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
    • A μ-a.e. identity alone would not be the same stated hypothesis; the integral comparison later uses this π-a.e. identity.
    • This does not follow from absolute continuity alone and does not construct a valid canonical-density chain rule.

    Source and reuse

    ASTIS parents called

    Mathlib API called (external library)

    • LinearMap
    • Filter.Eventually

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    ASTIS mathematical exposition

    Identify the density–log-density Dirichlet pairing with guarded Fisher

    AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_information · theorem · Teaching coverage

    Statement

    Let μ and π be measures on finite-dimensional Euclidean space, with μ σ-finite and a Lebesgue decomposition of μ relative to π. Let L be a real-linear operator on real-valued functions. Suppose the selected RN log-ratio has a smooth finite score-domain witness hscore; the three terms L(ρr), ρLr, rLρ are π-integrable; the integral of L(ρr) is zero; the two cross integrals are equal; and Γ_L(ρ,r)=ρ‖∇r‖² π-a.e. Then the generator Dirichlet pairing of the selected density and log-ratio equals their guarded canonical Fisher value.

    \[\mathcal E_\pi^L(\rho,r):=-\int_E\rho\,Lr\,d\pi\ =\ \int_E\Gamma_L(\rho,r)\,d\pi\ =\ \int_E\rho\,\|\nabla r\|^2\,d\pi\ =\ I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]

    All objects and hypotheses

    • ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
    • μ 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)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
    • μ is σ-finite, and the typeclass HaveLebesgueDecomposition μ π is supplied. π need not be assumed σ-finite. These are in addition to μ ≪ π in the score-domain witness.
    • 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 supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).
    • The supplied witness hpair proves, for the fixed functions ρ and r, that L(ρr), x ↦ ρ(x)Lr(x), and x ↦ r(x)Lρ(x) are π-integrable, that ∫ L(ρr) dπ = 0, and that ∫ ρ Lr dπ = ∫ r Lρ dπ.
    • The supplied hgamma asserts Γ_L(ρ,r)(x) = ρ(x)q(x) for π-almost every x, where Γ_L(f,g) = ½[L(fg) − f Lg − g Lf]. It is not required pointwise everywhere.

    Mathematical proof

    1. Apply the existing integration-by-parts theorem to the selected pair

    Pass all five fields of hpair to the existing helper with base measure π, f=ρ, and g=r. The relevant second conclusion identifies the Dirichlet pairing with the integrated Γ.

    \[\mathcal E_\pi^L(\rho,r)=\int_E\Gamma_L(\rho,r)\,d\pi.\]
    Corresponding Lean step

    StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts ...; hibp.2

    2. Understand why that reused identity is valid

    Inside the helper, the three integrability assumptions permit subtracting integrals term by term in the Γ definition. This is explanatory expansion of the reused proof, not a newly proved helper.

    \[\int_E\Gamma_L(\rho,r)\,d\pi=\tfrac12\left[\int_EL(\rho r)\,d\pi-\int_E\rho Lr\,d\pi-\int_ErL\rho\,d\pi\right].\]
    Corresponding Lean step

    fundamental_integration_by_parts: hLfg.sub hfLg; integral_const_mul; integral_sub

    3. Use only the supplied local stationarity and symmetry

    The first integral is zero and the two cross integrals coincide, so the half-sum is exactly minus either cross integral, with the same sign as the Dirichlet-form definition.

    \[\tfrac12(0-A-A)=-A=\mathcal E_\pi^L(\rho,r),\qquad A:=\int_E\rho Lr\,d\pi.\]
    Corresponding Lean step

    fundamental_integration_by_parts: hstationary; hsymmetric; Generator.dirichletForm

    4. Put the Fisher value over the same measure

    Use the already-established RN change-of-measure formula for the fixed original score, under μ's σ-finiteness, the decomposition instance, and the absolute continuity in hscore.

    \[I_{h_{\mathrm{score}}}(\mu\Vert\pi)=\int_E\rho(x)q(x)\,d\pi(x).\]
    Corresponding Lean step

    CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq mu pi hscore

    5. Compare the integrands almost everywhere

    Now both sides are π-integrals. Apply integral congruence to hgamma; its exceptional π-null set is harmless and no pointwise-everywhere identity is needed.

    \[\Gamma_L(\rho,r)=\rho q\quad\pi\text{-a.e.}\quad\Longrightarrow\quad\int_E\Gamma_L(\rho,r)\,d\pi=\int_E\rho q\,d\pi.\]
    Corresponding Lean step

    MeasureTheory.integral_congr_ae hgamma

    Lean statement · dirichletForm_density_logRatio_eq_information

    The three named witnesses carry different obligations: the score witness controls μ-a.e. classical differentiability and μ-integrability, the pair witness supplies five π-integral conditions, and the Γ witness supplies a π-a.e. equality. The bracketed RN assumptions are additional. None of these witnesses is constructed by this theorem.

    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 dirichletForm_density_logRatio_eq_information
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      CanonicalRelativeFisher.information mu pi hscore

    Exact module and namespace context

    Lean proof · dirichletForm_density_logRatio_eq_information

    Lean first obtains the two-part integration-by-parts result and uses its second component. It next rewrites the Fisher side as a weighted π-integral. The remaining goal is equality of two π-integrals, which follows directly from the supplied a.e. Γ identity. The integral algebra behind the imported helper explains the factor one-half and the negative-generator sign.

    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 dirichletForm_density_logRatio_eq_information
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      CanonicalRelativeFisher.information mu pi hscore := by
  have hibp :=
    StochasticProcesses.CarreDuChamp.fundamental_integration_by_parts
      pi generator (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)
      hpair.generator_product_integrable
      hpair.density_mul_generator_logRatio_integrable
      hpair.logRatio_mul_generator_density_integrable
      hpair.stationary_product hpair.symmetric_pair
  rw [hibp.2]
  rw [CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq
    mu pi hscore]
  exact integral_congr_ae hgamma

/-- Equivalent source-facing integral form of the same bridge. -/

    Exact module and namespace context

    Scope and omitted-condition boundaries

    • This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
    • These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
    • No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
    • This bridge preserves the selected representative, generator normalization, and all three witnesses. It does not produce a concrete Γ formula or show that any diffusion satisfies the hypotheses.
    • The source card belongs to the reused integration-by-parts helper. This combined canonical Fisher edge is not assigned a new numbered source theorem or a source-equivalence certification.
    • No probability normalization, entropy identity, or law-evolution statement is required or concluded.

    Source and reuse

    ASTIS parents called

    Mathlib API called (external library)

    • MeasureTheory.integral_congr_ae

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    ASTIS mathematical exposition

    The same Dirichlet bridge written as an integral under μ

    AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.dirichletForm_density_logRatio_eq_integral_scoreSq · theorem · Teaching coverage

    Statement

    Under exactly the same hypotheses as the Dirichlet–Fisher bridge—μ σ-finite, a Lebesgue decomposition relative to π, a real-linear L, the smooth finite selected-score domain, the five local π-pair conditions, and Γ_L(ρ,r)=ρ‖∇r‖² π-a.e.—the Dirichlet pairing equals the μ-integral of the squared selected score. This is a reformulation of the preceding bridge using the integral definition of guarded Fisher information.

    \[\mathcal E_\pi^L(\rho,r)=-\int_E\rho Lr\,d\pi=\int_E\|\nabla r(x)\|^2\,d\mu(x).\]

    All objects and hypotheses

    • ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
    • μ 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)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
    • μ is σ-finite, and the typeclass HaveLebesgueDecomposition μ π is supplied. π need not be assumed σ-finite. These are in addition to μ ≪ π in the score-domain witness.
    • 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 supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).
    • The supplied witness hpair proves, for the fixed functions ρ and r, that L(ρr), x ↦ ρ(x)Lr(x), and x ↦ r(x)Lρ(x) are π-integrable, that ∫ L(ρr) dπ = 0, and that ∫ ρ Lr dπ = ∫ r Lρ dπ.
    • The supplied hgamma asserts Γ_L(ρ,r)(x) = ρ(x)q(x) for π-almost every x, where Γ_L(f,g) = ½[L(fg) − f Lg − g Lf]. It is not required pointwise everywhere.

    Mathematical proof

    1. Reuse the guarded Dirichlet–Fisher identification

    Apply the preceding theorem with the same μ, π, L and three witnesses. No new integration-by-parts argument is needed.

    \[\mathcal E_\pi^L(\rho,r)=I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]
    Corresponding Lean step

    dirichletForm_density_logRatio_eq_information mu pi generator hscore hpair hgamma

    2. Open the already-proved μ-integral formula

    The canonical relative-Fisher formula identifies that same guarded value with the μ-integral of q. Combine the two equalities.

    \[I_{h_{\mathrm{score}}}(\mu\Vert\pi)=\int_Eq(x)\,d\mu(x)=\int_E\|\nabla r(x)\|^2\,d\mu(x).\]
    Corresponding Lean step

    CanonicalRelativeFisher.information_eq_integral_scoreSq mu pi hscore

    Lean statement · dirichletForm_density_logRatio_eq_integral_scoreSq

    The right side now displays the squared-score integral explicitly instead of naming the guarded value. The hypotheses have not been weakened: the same score certificate, pair certificate, Γ equality, σ-finiteness, and decomposition instance remain inputs.

    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 dirichletForm_density_logRatio_eq_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      ∫ x, CanonicalRelativeFisher.scoreSq mu pi x ∂mu

    Exact module and namespace context

    Lean proof · dirichletForm_density_logRatio_eq_integral_scoreSq

    Lean chains two existing equalities. First it replaces the Dirichlet pairing with the guarded Fisher value; then it replaces that value with its μ-integral formula. This declaration is a reusable presentation wrapper, not a second proof of the analytic bridge.

    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 dirichletForm_density_logRatio_eq_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator) :
    FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi) =
      ∫ x, CanonicalRelativeFisher.scoreSq mu pi x ∂mu := by
  rw [dirichletForm_density_logRatio_eq_information
    mu pi generator hscore hpair hgamma]
  exact CanonicalRelativeFisher.information_eq_integral_scoreSq mu pi hscore

/-- A supplied KL derivative written as minus the canonical density/log-ratio
Dirichlet form immediately becomes the standard dissipation rate `-FI`.

This theorem intentionally starts *after* the analytic law-evolution /
differentiation-under-the-integral step.  The next topology node must prove that
step for the Langevin measure flow rather than hiding it inside this algebraic
handoff. -/

    Exact module and namespace context

    Scope and omitted-condition boundaries

    • This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
    • These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
    • No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
    • This source-facing notation does not make the selected score automatically equal to a source's Sobolev or square-root-density Fisher functional.
    • No new diffusion-domain existence, integrability producer, source theorem, or entropy dissipation result.

    Source and reuse

    ASTIS parents called

    Mathlib API called (external library)

    No direct Mathlib call recorded; see the ASTIS parents.

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.

    ASTIS mathematical exposition

    Rewrite a supplied negative-Dirichlet derivative as negative Fisher

    AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisher.hasDerivAt_eq_neg_information_of_eq_neg_dirichlet · theorem · Teaching coverage

    Statement

    Let μ and π, L, and the three domain/Γ witnesses satisfy all hypotheses of the Dirichlet–Fisher bridge, including μ σ-finiteness and a Lebesgue-decomposition instance. Let K:ℝ→ℝ be any real function and t∈ℝ. If K has a two-sided derivative at t with value −Eπ^L(ρ,r), then K has a derivative there with value −I_hscore(μ∥π). The derivative assumption is supplied; K is not required by the formal statement to be a KL-divergence path.

    \[\left[K'(t)=-\mathcal E_\pi^L(\rho,r)\ \text{in the sense of HasDerivAt}\right]\quad\Longrightarrow\quad K'(t)=-I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]

    All objects and hypotheses

    • ι is a finite index type (Fintype ι), and E = EuclideanSpace ℝ ι has its standard real inner product, norm, topology and Borel measurable structure. Empty ι is allowed; no Nonempty ι assumption is made.
    • μ 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)); put q(x) = ‖gradient r x‖². These are fixed by the original ordered pair (μ,π), not arbitrary versions.
    • μ is σ-finite, and the typeclass HaveLebesgueDecomposition μ π is supplied. π need not be assumed σ-finite. These are in addition to μ ≪ π in the score-domain witness.
    • 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 supplied witness h (or hscore) proves all three conditions: μ ≪ π; r is classically Fréchet differentiable over ℝ at μ-almost every x; and q is μ-integrable (including its a.e. strong measurability and finite integral of its norm).
    • The supplied witness hpair proves, for the fixed functions ρ and r, that L(ρr), x ↦ ρ(x)Lr(x), and x ↦ r(x)Lρ(x) are π-integrable, that ∫ L(ρr) dπ = 0, and that ∫ ρ Lr dπ = ∫ r Lρ dπ.
    • The supplied hgamma asserts Γ_L(ρ,r)(x) = ρ(x)q(x) for π-almost every x, where Γ_L(f,g) = ½[L(fg) − f Lg − g Lf]. It is not required pointwise everywhere.
    • K is an arbitrary function ℝ → ℝ and t is an arbitrary real time. hK is the full HasDerivAt assertion for K at t with derivative −Eπ^L(ρ,r), using the ordinary two-sided neighborhood filter, not a one-sided derivative on t≥0.
    • The measures μ and π are fixed parameters in this declaration. No time-dependent law μ_t or equation relating K to entropy is assumed.

    Mathematical proof

    1. Identify the rate already present in the derivative hypothesis

    The existing conditional bridge gives equality of the Dirichlet pairing and guarded Fisher value for these fixed measures and generator.

    \[\mathcal E_\pi^L(\rho,r)=I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]
    Corresponding Lean step

    dirichletForm_density_logRatio_eq_information mu pi generator hscore hpair hgamma

    2. Negate equal quantities

    The negative rate in hK can therefore be written as negative Fisher without changing its numerical value.

    \[-\mathcal E_\pi^L(\rho,r)=-I_{h_{\mathrm{score}}}(\mu\Vert\pi).\]
    Corresponding Lean step

    Rewriting under the unary minus in HasDerivAt

    3. Reuse the already-supplied derivative proof

    Substitute that equal real number into the derivative assertion. The differentiability and limiting argument are wholly contained in hK, not produced here.

    \[\operatorname{HasDerivAt}(K,-\mathcal E_\pi^L(\rho,r),t)\Longrightarrow\operatorname{HasDerivAt}(K,-I_{h_{\mathrm{score}}}(\mu\Vert\pi),t).\]
    Corresponding Lean step

    simpa [dirichletForm_density_logRatio_eq_information ...] using hK

    Lean statement · hasDerivAt_eq_neg_information_of_eq_neg_dirichlet

    K is a general real-valued function and hK already proves its derivative at t. The conclusion changes only the displayed derivative value. Since the type is the ordinary HasDerivAt, an endpoint right derivative by itself is not the input required here.

    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 hasDerivAt_eq_neg_information_of_eq_neg_dirichlet
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator)
    {K : ℝ → ℝ} {t : ℝ}
    (hK : HasDerivAt K
      (-FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)) t) :
    HasDerivAt K (-CanonicalRelativeFisher.information mu pi hscore) t

    Exact module and namespace context

    Lean proof · hasDerivAt_eq_neg_information_of_eq_neg_dirichlet

    The proof uses the Dirichlet–Fisher equality to rewrite the real number inside hK, preserving its minus sign. It then reuses hK unchanged in substance. There is no proof of a measure-flow equation, no entropy identification, and no exchange of differentiation with integration.

    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 hasDerivAt_eq_neg_information_of_eq_neg_dirichlet
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (generator :
      (State (ι := ι) → ℝ) →ₗ[ℝ] (State (ι := ι) → ℝ))
    (hscore : CanonicalRelativeFisher.SmoothFiniteScoreDomain mu pi)
    (hpair : DirichletPairDomain mu pi generator)
    (hgamma : HasCanonicalFisherGamma mu pi generator)
    {K : ℝ → ℝ} {t : ℝ}
    (hK : HasDerivAt K
      (-FunctionalInequalities.Generator.dirichletForm pi generator
        (RNLogRatio.density mu pi) (RNLogRatio.logRatio mu pi)) t) :
    HasDerivAt K (-CanonicalRelativeFisher.information mu pi hscore) t := by
  simpa [dirichletForm_density_logRatio_eq_information
    mu pi generator hscore hpair hgamma] using hK

end

end CanonicalDirichletFisher
end InformationTheory
end TechnicalLemmas
end AutoSamplingTheory

    Exact module and namespace context

    Scope and omitted-condition boundaries

    • This is the selected RN/log-ratio and its totalized classical gradient, not a representative-free Sobolev score. Equality of log-ratios merely a.e. does not by itself identify their gradients. Mathlib sets gradient to zero at nondifferentiable points; the score-domain witness excludes those points only μ-a.e.
    • These are only local pair conditions. No global stationarity, reversibility, generator-domain closure, concrete Langevin generator, or diffusion chain rule is derived.
    • No existence of the smooth score domain is proved. No weak derivative, Sobolev-domain membership, lower-semicontinuous or extended-valued Fisher extension, or square-root-density identity 4∫‖∇√ρ‖² dπ is established.
    • No KL identity, entropy finiteness, evolving family of measures, PDE/semigroup equation, or differentiation under the integral is proved. The function K and its derivative are supplied as inputs.
    • A finite-entropy neighborhood, differentiability of an actual KL path, source-law normalization, and an endpoint one-sided-to-two-sided adapter are not supplied.
    • This is an algebraic handoff after a derivative proof; it is not a new entropy-dissipation theorem.

    Source and reuse

    ASTIS parents called

    Mathlib API called (external library)

    • HasDerivAt

    Mathematical sources

    ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.