CanonicalRelativeFisher: 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.

The Euclidean state-space name
Squared score of the selected RN log-ratio
The explicit smooth finite score domain
A guarded finite Fisher value using the shared energy
The guarded value is exactly the shared RelativeFisher energy
The guarded value is the squared-score integral under μ
Move the score integral from μ to the reference measure
Read squared-score integrability from its certificate
The guarded Fisher value is nonnegative
Different proofs of the same domain give the same value

ASTIS mathematical exposition

The Euclidean state-space name

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

Statement

For an index type ι, State is simply the existing Mathlib Euclidean space of real ι-indexed coordinates. The abbreviation itself imposes no finiteness proof; the surrounding Fisher development assumes ι is finite when using the usual Euclidean calculus.

\[E:=\operatorname{EuclideanSpace}(\mathbb R,\iota);\qquad\text{for finite }\iota,\quad \langle x,y\rangle=\sum_{i\in\iota}x_i y_i,\quad\|x\|^2=\sum_{i\in\iota}x_i^2.\]

All objects and hypotheses

ι is an arbitrary index type for the abbreviation itself. In the surrounding section, Fintype ι is available for subsequent finite-dimensional analysis.
No measure, density, gradient, probability assumption, or Nonempty ι proof is needed to name State.

Construction and meaning

1. Reuse the existing space

Give Mathlib's EuclideanSpace ℝ ι the local short name State; no elements, norms, or topology are reconstructed.

\[\mathrm{State}=\operatorname{EuclideanSpace}(\mathbb R,\iota).\]

Corresponding Lean step

EuclideanSpace ℝ ι

Lean statement · State

This line introduces a shorter name for the existing coordinate space. The index type specifies its coordinate labels; it is not a theorem asserting an analytic fact about that space.

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 to supply. The right-hand expression is the underlying Mathlib type, so Lean can unfold the abbreviation whenever a later definition needs Euclidean calculus.

abbrev State := EuclideanSpace ℝ ι

/-- The squared canonical relative score. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The module's later declarations work with finite ι. This abbreviation does not create an independent state-space construction or an infinite-dimensional Fisher theorem.
No positivity-of-dimension or probability-law assumption.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

EuclideanSpace

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Mathlib EuclideanSpace abbreviation — Underlying type reused; finite-coordinate inner-product interpretation is inherited from Mathlib.

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

Squared score of the selected RN log-ratio

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.scoreSq · def · Teaching coverage

Statement

Let μ and π be arbitrary measures on a finite-dimensional real Euclidean space E and let x∈E. Form the specific Mathlib RN log-ratio r(x)=log((dμ/dπ)selected(x).toReal). The canonical squared score at x is the squared Euclidean norm of the totalized classical gradient of this very function r.

\[\rho(x):=(\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal},\qquad r(x):=\log\rho(x),\qquad q(x):=\|\nabla r(x)\|^2.\]

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.
x is any point of E. This definition has no absolute-continuity, differentiability, integrability, σ-finiteness, or Lebesgue-decomposition premise.

Construction and meaning

1. Fix the log-ratio function

Use the canonical RNLogRatio.logRatio attached to the original measures. This is Mathlib's selected log-likelihood ratio; it is not a user-selected smooth density representative.

\[r=\mathrm{llr}(\mu,\pi)=\log\big((\mu.\mathrm{rnDeriv}\,\pi).\mathrm{toReal}\big).\]

Corresponding Lean step

RNLogRatio.logRatio mu pi

2. Take the totalized Euclidean gradient

Mathlib represents a derivative by its Riesz-dual vector when the classical derivative exists, and uses zero when it does not. Thus this operation is globally defined before a regularity domain has been supplied.

\[\nabla r(x)=(\mathrm{toDual}_{\mathbb R,E})^{-1}(\mathrm{fderiv}_{\mathbb R}r(x)).\]

Corresponding Lean step

gradient (RNLogRatio.logRatio mu pi) x

3. Measure its squared length

Take the norm of the gradient vector and square it. This completes a construction, not a proof of differentiability or integrability.

\[q(x)=\|\nabla r(x)\|^2.\]

Corresponding Lean step

‖gradient (RNLogRatio.logRatio mu pi) x‖ ^ 2

Lean statement · scoreSq

The definition takes two measures and one state and returns a real number. No hypothesis accompanies it, so its availability does not certify that the chosen log-ratio is differentiable at that state.

noncomputable def scoreSq
    (mu pi : Measure (State (ι := ι)))
    (x : State (ι := ι)) : ℝ

Exact module and namespace context

Lean construction · scoreSq

The body first obtains the fixed log-ratio function, then its Mathlib gradient at the input point, and finally a squared norm. These are existing operations; the later domain structure is what justifies interpreting the result as a classical finite score energy.

noncomputable def scoreSq
    (mu pi : Measure (State (ι := ι)))
    (x : State (ι := ι)) : ℝ :=
  ‖gradient (RNLogRatio.logRatio mu pi) x‖ ^ 2

/-- Explicit regularity contract for the smooth finite branch of relative
Fisher information.

The future Sobolev/Dirichlet-energy extension should map into this contract on
its smooth finite subdomain; it should not weaken or erase these obligations. -/

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.
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.
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 identification with ∇log of an arbitrary smooth version of a density is supplied.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatio.logRatio

Mathlib API called (external library)

gradient

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
ASTIS selected RN density and log-ratio — Definitions density and logRatio plus pointwise logRatio_apply at line45; representative conventions only.
Mathlib gradient and its nondifferentiable default — Definition gradient; gradient_eq_zero_of_not_differentiableAt is at line118.
Existing selected-score representative boundary in the downstream module card — Context only, not a dependency of either current module. The card explicitly preserves selected-RN versus Sobolev-score limits and records independent source certification withheld for that downstream transport packet. No status is changed here.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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 explicit smooth finite score domain

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain · structure · Teaching coverage

Statement

For arbitrary measures μ and π on finite-dimensional Euclidean space, SmoothFiniteScoreDomain μ π is the conjunction of three actual mathematical requirements: μ is absolutely continuous with respect to π; the selected RN log-ratio r is classically differentiable at μ-almost every point; and its squared totalized gradient q is integrable with respect to μ. A witness must prove all three. This declaration does not prove that any given pair belongs to the domain.

\[\mathcal D(\mu,\pi)\;:\Longleftrightarrow\;\mu\ll\pi\ \land\ [r\text{ is Fréchet differentiable at }x\text{ for }\mu\text{-a.e. }x]\ \land\ q\in L^1(\mu),\qquad q=\|\nabla r\|^2.\]

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.
The structure itself takes only μ and π; its three fields are obligations to prove, not assumptions automatically generated by declaring the structure.
No σ-finiteness or HaveLebesgueDecomposition instance is part of this domain. No probability normalization, strict positivity everywhere, or global smoothness is asserted.

Construction and meaning

1. Supply absolute continuity

Prove that every π-null measurable set is μ-null. This is the first field of a domain witness; it is independent of the later differentiability requirement.

\[\mu\ll\pi.\]

Corresponding Lean step

SmoothFiniteScoreDomain.absolutelyContinuous

2. Supply classical differentiability at almost every μ-point

Prove differentiability of the exact function r on the ambient Euclidean space at all points outside a μ-null exceptional set. The filter is μ, not π or Lebesgue measure.

\[\mu\text{-a.e. }x:\quad r\text{ is differentiable at }x.\]

Corresponding Lean step

SmoothFiniteScoreDomain.differentiable_ae

3. Supply finite score integrability

Prove that q is a.e. strongly measurable and that the integral of its norm is finite. This prevents a real Bochner integral from merely returning its default value for a nonintegrable expression.

\[q\in L^1(\mu),\qquad \int |q|\,d\mu<\infty.\]

Corresponding Lean step

SmoothFiniteScoreDomain.scoreSq_integrable

4. Package the three proofs

Only after all three proofs have been obtained may they be collected into one witness of the proposition. The structure records these facts without deriving one from another.

\[(h_{\mathrm{ac}},h_{\mathrm{diff}},h_{L^1})\;:\;\mathcal D(\mu,\pi).\]

Corresponding Lean step

SmoothFiniteScoreDomain.mk

Lean statement · SmoothFiniteScoreDomain

The result is a proposition with three named proof fields, not descriptive metadata or a string-valued contract. The phrase almost everywhere in the differentiability field refers specifically to μ. Integrable includes both the relevant measurability and finite-norm-integral requirement.

structure SmoothFiniteScoreDomain
    (mu pi : Measure (State (ι := ι))) : Prop where
  absolutelyContinuous : mu ≪ pi
  differentiable_ae :
    ∀ᵐ x ∂mu, DifferentiableAt ℝ (RNLogRatio.logRatio mu pi) x
  scoreSq_integrable : Integrable (scoreSq mu pi) mu

/-- Canonical relative Fisher information on the explicit smooth finite score
domain.

It is exactly the existing `RelativeFisher.information` with base measure `mu`
and density `1`, so no second Fisher hierarchy is introduced. -/

Exact module and namespace context

Lean construction · SmoothFiniteScoreDomain

A structure declaration defines what a certificate must contain; it does not itself construct a certificate. A user must independently prove absolute continuity, differentiability of this selected representative, and squared-score integrability before using the guarded Fisher value.

structure SmoothFiniteScoreDomain
    (mu pi : Measure (State (ι := ι))) : Prop where
  absolutelyContinuous : mu ≪ pi
  differentiable_ae :
    ∀ᵐ x ∂mu, DifferentiableAt ℝ (RNLogRatio.logRatio mu pi) x
  scoreSq_integrable : Integrable (scoreSq mu pi) mu

/-- Canonical relative Fisher information on the explicit smooth finite score
domain.

It is exactly the existing `RelativeFisher.information` with base measure `mu`
and density `1`, so no second Fisher hierarchy is introduced. -/

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.
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.
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.
Differentiable μ-a.e. is not C¹ smoothness, smoothness on the support, differentiability π-a.e., or a weak-derivative assertion.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.Measure.AbsolutelyContinuous
DifferentiableAt
MeasureTheory.Integrable
Filter.Eventually

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Selected log-ratio definition — Identifies the exact function appearing in the differentiability field.
Existing selected-score representative boundary in the downstream module card — Context only, not a dependency of either current module. The card explicitly preserves selected-RN versus Sobolev-score limits and records independent source certification withheld for that downstream transport packet. No status is changed here.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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

A guarded finite Fisher value using the shared energy

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information · def · Teaching coverage

Statement

Given arbitrary measures μ and π on finite-dimensional Euclidean space and a proof h of the smooth finite score domain, define their canonical relative Fisher value by evaluating the existing RelativeFisher energy with base measure μ, constant weight one, and the selected log-ratio r. Thus the guarded value is the finite integral of the squared classical score of that representative.

\[I_h(\mu\Vert\pi):=\operatorname{RelativeFisher}(\mu,1,r)=\int_E 1\cdot\|\nabla r(x)\|^2\,d\mu(x),\qquad h:\mathcal D(\mu,\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.
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).

Construction and meaning

1. Use the explicit domain certificate

The input certificate guarantees a classical score μ-a.e. and integrability of its squared norm. No certificate is inferred from the measures alone.

\[h:\mathcal D(\mu,\pi)\ \Longrightarrow\ q\in L^1(\mu).\]

Corresponding Lean step

_h : SmoothFiniteScoreDomain mu pi

2. Choose the shared energy's three inputs

Set its base measure to μ, its multiplier to the constant function one, and its log-ratio argument to the selected r. Since μ itself is the integration measure, no additional density factor is needed here.

\[(\mathrm{base},\mathrm{weight},\mathrm{logRatio})=(\mu,1,r).\]

Corresponding Lean step

RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

3. Read the constructed value

The shared energy integrates its pointwise weight times squared gradient. The domain's integrability field makes this a genuine finite real integral, not an infinite-energy extension.

\[I_h(\mu\Vert\pi)=\int 1\cdot q\,d\mu=\int q\,d\mu.\]

Corresponding Lean step

RelativeFisher.information; RelativeFisher.densityEnergy

Lean statement · information

The last input is a proof that the pair lies in the stated domain. Although this proof is not used to compute the real-valued expression, requiring it at the interface prevents callers from presenting an unqualified totalized integral as the guarded Fisher value.

noncomputable def information
    (mu pi : Measure (State (ι := ι)))
    (_h : SmoothFiniteScoreDomain mu pi) : ℝ

Exact module and namespace context

Lean construction · information

This is a definition, not a new integral theorem. It calls the already-existing RelativeFisher functional with μ as the base measure and unit weight. The proof certificate controls admissibility; the numerical expression does not depend on how that certificate was established.

noncomputable def information
    (mu pi : Measure (State (ι := ι)))
    (_h : SmoothFiniteScoreDomain mu pi) : ℝ :=
  RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

/-- The canonical guarded definition is definitionally the shared
`RelativeFisher` object. -/

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.
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 second independent Fisher hierarchy is constructed. The codomain is ℝ, and inputs outside the explicit domain have no value through this guarded interface.
The domain certificate contains no probability assumption and no finite-entropy assumption; this definition alone gives neither.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Shared density-energy functional reused by definition — densityEnergy at42 and information at52 define the existing weighted Bochner integral.
Existing selected-score representative boundary in the downstream module card — Context only, not a dependency of either current module. The card explicitly preserves selected-RN versus Sobolev-score limits and records independent source certification withheld for that downstream transport packet. No status is changed here.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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 guarded value is exactly the shared RelativeFisher energy

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_relativeFisher · theorem · Teaching coverage

Statement

For arbitrary μ and π on finite-dimensional Euclidean space, and any witness h that μ≪π, the selected log-ratio r is differentiable μ-a.e., and its squared gradient is μ-integrable, the canonical guarded Fisher value is exactly RelativeFisher.information with base μ, unit weight, and log-ratio r. This equality is built into the definition.

\[I_h(\mu\Vert\pi)=\operatorname{RelativeFisher.information}(\mu,\mathbf 1,r).\]

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

Mathematical proof

1. Unfold the guarded name

Its defining expression already is the shared functional with the specified three inputs.

\[I_h(\mu\Vert\pi)\equiv\operatorname{RelativeFisher.information}(\mu,\mathbf 1,r).\]

Corresponding Lean step

information

2. Recognize identical expressions

Both sides reduce to precisely the same term. No estimate or change of representatives is involved.

\[\operatorname{RelativeFisher.information}(\mu,\mathbf 1,r)=\operatorname{RelativeFisher.information}(\mu,\mathbf 1,r).\]

Corresponding Lean step

rfl

Lean statement · information_eq_relativeFisher

Both sides use the same measures and the same selected log-ratio. The theorem exposes the definition under the older shared energy name; it does not compare two independently defined notions of Fisher information.

theorem information_eq_relativeFisher
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi)

Exact module and namespace context

Lean proof · information_eq_relativeFisher

After Lean unfolds the guarded name, there is nothing to prove beyond equality of an expression with itself. The domain certificate remains a required input even though no analytic field is used in this definitional equality.

theorem information_eq_relativeFisher
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      RelativeFisher.information mu (fun _ => 1) (RNLogRatio.logRatio mu pi) := by
  rfl

/-- On the guarded smooth finite domain, the canonical Fisher information has
the expected measure-level formula

`FI(mu || pi) = integral ||grad log(d mu / d pi)||^2 dmu`. -/

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.
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 wrapper is not an independent analytic identification with a Sobolev, Dirichlet, or source-defined Fisher quantity.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Shared information definition — The exact functional on the right; equality is a reuse identity, not a source equivalence theorem.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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 guarded value is the squared-score integral under μ

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_integral_scoreSq · theorem · Teaching coverage

Statement

For measures μ and π on finite-dimensional Euclidean space and an explicit smooth finite score-domain witness h, the canonical Fisher value equals the μ-integral of the squared gradient of the selected RN log-ratio. The domain witness makes the integrand genuinely integrable; the equality itself follows by removing the unit weight in the reused definition.

\[I_h(\mu\Vert\pi)=\int_E q(x)\,d\mu(x)=\int_E\|\nabla r(x)\|^2\,d\mu(x),\qquad q\in L^1(\mu).\]

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

Mathematical proof

1. Open the shared-energy definition

The guarded value uses μ as the base measure and the constant multiplier one.

\[I_h(\mu\Vert\pi)=\int_E\operatorname{densityEnergy}(\mathbf 1,r)(x)\,d\mu(x).\]

Corresponding Lean step

information; RelativeFisher.information

2. Expand the pointwise energy

The density-energy definition is weight times squared gradient norm.

\[\operatorname{densityEnergy}(\mathbf 1,r)(x)=1\cdot\|\nabla r(x)\|^2.\]

Corresponding Lean step

RelativeFisher.densityEnergy

3. Remove the unit multiplier

Multiplication by one leaves the squared score unchanged, so both integral expressions coincide.

\[1\cdot\|\nabla r(x)\|^2=q(x),\qquad I_h(\mu\Vert\pi)=\int_Eq\,d\mu.\]

Corresponding Lean step

simp [information, RelativeFisher.information, RelativeFisher.densityEnergy, scoreSq]

Lean statement · information_eq_integral_scoreSq

The conclusion is an equality of real numbers. The same selected score appears in the named functional and in the integral, and the domain assumption includes the integrability needed to read that integral as a finite energy.

theorem information_eq_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu

Exact module and namespace context

Lean proof · information_eq_integral_scoreSq

Lean expands the two energy definitions and the squared-score name, then simplifies multiplication by one. It does not establish integrability during this proof: that fact was required in the supplied domain certificate.

theorem information_eq_integral_scoreSq
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h = ∫ x, scoreSq mu pi x ∂mu := by
  simp [information, RelativeFisher.information, RelativeFisher.densityEnergy, scoreSq]

/-- The same canonical Fisher information rewritten against the reference
measure using Mathlib's Radon--Nikodym integral formula:

`FI(mu || pi) = integral density(mu|pi) * scoreSq(mu|pi) dpi`.

Crucially, this changes only the integration measure.  The integrand keeps the
original `mu` parameter; rewriting `mu` itself as a `withDensity` measure would
incorrectly rewrite the score object as well. -/

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.
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 theorem does not require σ-finiteness or a Lebesgue-decomposition instance because it only unfolds the μ-based definition.
No finiteness of KL divergence or entropy is asserted.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

one_mul

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Shared pointwise and integrated energy definitions — Unit-weight specialization only; no RN change of integration measure occurs in this proof.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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

Move the score integral from μ to the reference measure

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_eq_integral_density_mul_scoreSq · theorem · Teaching coverage

Statement

Let μ and π be measures on finite-dimensional Euclidean space. Assume μ is σ-finite, a Lebesgue decomposition of μ with respect to π is available, and h proves μ≪π, differentiability of the selected log-ratio r μ-a.e., and integrability of q=‖∇r‖² under μ. Then the same canonical Fisher value equals the π-integral of the selected real RN density times the same squared score. Only the integration measure changes; both ρ and q retain the original pair (μ,π).

\[I_h(\mu\Vert\pi)=\int_E q_{\mu,\pi}\,d\mu=\int_E\rho_{\mu,\pi}(x)\,q_{\mu,\pi}(x)\,d\pi(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.
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).

Mathematical proof

1. Expose the original μ-integral

Use the already-proved definition-unfolding formula. Keep its integrand fixed as the function q attached to μ and π.

\[I_h(\mu\Vert\pi)=\int_Eq_{\mu,\pi}(x)\,d\mu(x).\]

Corresponding Lean step

information_eq_integral_scoreSq mu pi h

2. Apply the existing RN integral formula

Absolute continuity, the specified Lebesgue decomposition, and σ-finiteness of μ are exactly the assumptions of Mathlib's real-valued RN transport theorem. Applied to f=q, it identifies the weighted π-integral with the μ-integral.

\[\int_E(\mu.\mathrm{rnDeriv}\,\pi\,x).\mathrm{toReal}\,q_{\mu,\pi}(x)\,d\pi(x)=\int_Eq_{\mu,\pi}(x)\,d\mu(x).\]

Corresponding Lean step

MeasureTheory.integral_toReal_rnDeriv_mul (f := scoreSq mu pi) h.absolutelyContinuous

3. Read the selected density and reverse the equality

The real factor is exactly ρ by definition. Reverse the imported equality to obtain the target orientation, without replacing μ inside the score's parameters.

\[I_h(\mu\Vert\pi)=\int_E\rho_{\mu,\pi}(x)q_{\mu,\pi}(x)\,d\pi(x).\]

Corresponding Lean step

simpa [RNLogRatio.density] using (...) .symm

Lean statement · information_eq_integral_density_mul_scoreSq

The two bracketed assumptions provide σ-finiteness of μ and a Lebesgue decomposition of μ relative to π. There is no bracket requiring π to be σ-finite. The domain witness separately supplies absolute continuity and the score's classical and integrability conditions.

theorem information_eq_integral_density_mul_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      ∫ x, RNLogRatio.density mu pi x * scoreSq mu pi x ∂pi

Exact module and namespace context

Lean proof · information_eq_integral_density_mul_scoreSq

The proof first rewrites the guarded value as its μ-integral. It then instantiates Mathlib's RN integral identity with the already-fixed squared-score function and reverses that equality. Expanding only the density name prevents the original μ parameter inside the score from being inadvertently replaced by another representation of the measure.

theorem information_eq_integral_density_mul_scoreSq
    (mu pi : Measure (State (ι := ι)))
    [SigmaFinite mu] [Measure.HaveLebesgueDecomposition mu pi]
    (h : SmoothFiniteScoreDomain mu pi) :
    information mu pi h =
      ∫ x, RNLogRatio.density mu pi x * scoreSq mu pi x ∂pi := by
  rw [information_eq_integral_scoreSq mu pi h]
  simpa [RNLogRatio.density] using
    (MeasureTheory.integral_toReal_rnDeriv_mul
      (f := scoreSq mu pi) h.absolutelyContinuous).symm

/-- The squared score is integrable by the domain contract, rather than by an
implicit convention of the total integral. -/

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.
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.
The RN formula is a reused totalized-integral identity; genuine finite-energy interpretation here is supported by h.scoreSq_integrable. Its companion integrability theorem is contextual, not a direct dependency of the displayed proof.
No σ-finiteness of π, probability normalization, pointwise positivity of ρ, or smooth density version is inferred.
Changing only the integration measure does not justify changing either measure argument inside RNLogRatio or scoreSq.

Source and reuse

ASTIS parents called

Domain assumptions accessed

These are fields of the linked structure, not additional independently authored theorem leaves.

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain.absolutelyContinuous — Access the supplied absolute-continuity proof; this step does not establish absolute continuity from the definition of the score.

Mathlib API called (external library)

MeasureTheory.integral_toReal_rnDeriv_mul

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Exact Mathlib RN integral transport API and ambient hypotheses — Section assumptions include HaveLebesgueDecomposition μ ν and SigmaFinite μ; integral_toReal_rnDeriv_mul is at597.
Companion integrability transport (explanatory, not called by this proof) — integrable_toReal_rnDeriv_mul_iff confirms that the weighted reference-measure integrand is integrable when q is μ-integrable under the same RN hypotheses. It is not an additional theorem proved by this ASTIS wrapper.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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

Read squared-score integrability from its certificate

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.scoreSq_integrable · theorem · Teaching coverage

Statement

If h is a smooth finite score-domain witness for μ and π on finite-dimensional Euclidean space, then the squared gradient q of their selected log-ratio is integrable with respect to μ. This is exactly the integrability field already contained in h, not a consequence newly derived from absolute continuity or differentiability.

\[h:\mathcal D(\mu,\pi)\quad\Longrightarrow\quad q_{\mu,\pi}\in L^1(\mu).\]

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

Mathematical proof

1. Extract the requested field

The domain witness contains three proofs. Return its third proof, whose assertion is precisely the target integrability statement.

\[h=(h_{\mathrm{ac}},h_{\mathrm{diff}},h_{L^1})\quad\Longrightarrow\quad h_{L^1}:q\in L^1(\mu).\]

Corresponding Lean step

h.scoreSq_integrable

Lean statement · scoreSq_integrable

The conclusion repeats one field of the domain certificate. Integrable means a.e. strong measurability together with a finite integral of the norm, not merely that a total real integral expression can be written.

theorem scoreSq_integrable
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    Integrable (scoreSq mu pi) mu

Exact module and namespace context

Lean proof · scoreSq_integrable

The proof retrieves the certificate's stored integrability proof by its field name. No calculation or estimate is performed, and the other two fields do not by themselves imply this one.

theorem scoreSq_integrable
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    Integrable (scoreSq mu pi) mu :=
  h.scoreSq_integrable

/-- Canonical relative Fisher information is nonnegative on its guarded smooth
finite domain. -/

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.
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 is a convenience wrapper for reusing an assumption. It must not be presented as a theorem producing a finite score domain from absolute continuity or differentiability.

Source and reuse

ASTIS parents called

Domain assumptions accessed

These are fields of the linked structure, not additional independently authored theorem leaves.

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.SmoothFiniteScoreDomain.scoreSq_integrable — Return the integrability premise already stored in the supplied domain witness; this is a contract accessor, not a new integrability theorem.

Mathlib API called (external library)

MeasureTheory.Integrable

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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 guarded Fisher value is nonnegative

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_nonneg · theorem · Teaching coverage

Statement

For arbitrary μ and π on finite-dimensional Euclidean space and a supplied smooth finite score-domain witness h, the canonical Fisher value is nonnegative. It is the integral of a pointwise squared Euclidean norm, and therefore cannot be negative.

\[0\le I_h(\mu\Vert\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.
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).

Mathematical proof

1. Use the squared-score representation

Replace the named guarded quantity with the μ-integral of q.

\[I_h(\mu\Vert\pi)=\int_Eq\,d\mu.\]

Corresponding Lean step

information_eq_integral_scoreSq mu pi h

2. Establish pointwise nonnegativity

Every real square is nonnegative, including the square of the gradient's norm at each point. This does not require differentiability at that point because the gradient expression is totalized.

\[\forall x\in E,\quad 0\le\|\nabla r(x)\|^2=q(x).\]

Corresponding Lean step

sq_nonneg ‖gradient (RNLogRatio.logRatio mu pi) x‖

3. Integrate the nonnegative function

The Bochner integral of a pointwise nonnegative real function is nonnegative; in this guarded use q is additionally integrable by hypothesis.

\[0\le\int_Eq\,d\mu=I_h(\mu\Vert\pi).\]

Corresponding Lean step

MeasureTheory.integral_nonneg

Lean statement · information_nonneg

The theorem concludes only a lower bound of zero for the same guarded real-valued Fisher quantity. It has no probability-law assumption and does not state when equality is possible.

theorem information_nonneg
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    0 ≤ information mu pi h

Exact module and namespace context

Lean proof · information_nonneg

The proof rewrites the Fisher value as the score integral, observes that every squared norm is nonnegative, and applies the integral-positivity theorem. It does not need to reprove integrability, since the certificate already supplies it.

theorem information_nonneg
    (mu pi : Measure (State (ι := ι)))
    (h : SmoothFiniteScoreDomain mu pi) :
    0 ≤ information mu pi h := by
  rw [information_eq_integral_scoreSq mu pi h]
  exact integral_nonneg (fun x => sq_nonneg ‖gradient (RNLogRatio.logRatio mu pi) x‖)

/-- The guarded value does not depend on the proof witness used to establish the
same smooth finite score domain. -/

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.
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.
Nonnegativity does not show that zero Fisher implies μ=π, establish strict positivity, or identify the value with a source Sobolev energy.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

MeasureTheory.integral_nonneg
sq_nonneg
gradient

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Mathlib positivity of the integral — The pointwise-nonnegative version used by this proof.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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

Different proofs of the same domain give the same value

AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisher.information_proof_irrel · theorem · Teaching coverage

Statement

Fix the same measures μ and π on finite-dimensional Euclidean space. If h₁ and h₂ are two proofs of exactly the same smooth finite score-domain proposition, the guarded Fisher values obtained from them are equal. The measures and the selected RN/log-gradient representative are unchanged.

\[h_1,h_2:\mathcal D(\mu,\pi)\quad\Longrightarrow\quad I_{h_1}(\mu\Vert\pi)=I_{h_2}(\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.
h₁ and h₂ each prove all three domain fields for the identical ordered measure pair (μ,π): absolute continuity, μ-a.e. classical differentiability of r, and μ-integrability of q.

Mathematical proof

1. Observe that the numerical definition ignores the witness

Both values unfold to the shared energy using the same μ, weight one, and r. The proof argument controls admissibility but is absent from the defining numerical expression.

\[I_{h_1}(\mu\Vert\pi)\equiv\operatorname{RelativeFisher.information}(\mu,1,r)\equiv I_{h_2}(\mu\Vert\pi).\]

Corresponding Lean step

information

2. Close by definitional equality

After unfolding, the two sides are literally the same expression. No comparison of two differentiable versions is needed or provided.

\[\operatorname{RelativeFisher.information}(\mu,1,r)=\operatorname{RelativeFisher.information}(\mu,1,r).\]

Corresponding Lean step

rfl

Lean statement · information_proof_irrel

The subscripts distinguish proofs of admissibility, not two densities or two log-ratios. All mathematical inputs are held fixed, so the conclusion says the choice of proof cannot affect the numerical result.

theorem information_proof_irrel
    (mu pi : Measure (State (ι := ι)))
    (h₁ h₂ : SmoothFiniteScoreDomain mu pi) :
    information mu pi h₁ = information mu pi h₂

Exact module and namespace context

Lean proof · information_proof_irrel

The defining expression never reads the witness. Consequently both sides reduce to the same shared integral and Lean accepts reflexivity. This argument gives no permission to replace the RN representative by another a.e.-equal function.

theorem information_proof_irrel
    (mu pi : Measure (State (ι := ι)))
    (h₁ h₂ : SmoothFiniteScoreDomain mu pi) :
    information mu pi h₁ = information mu pi h₂ := by
  rfl

end

end CanonicalRelativeFisher
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.
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.
Proof-witness irrelevance is not density-version independence, weak/classical score equivalence, or invariance under arbitrary modifications on null sets.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Exact existing ASTIS declaration — Current local declaration and body, read without editing or recompiling.
Separate gradient-congruence theorem, not used here — information_congr_gradient_ae requires actual gradient equality a.e.; it illustrates why witness irrelevance is not representative independence.
Existing declaration-visibility smoke check — This file contains #check only for this declaration; it does not construct domain witnesses or independently establish analytic identities. No test/build was run for this exposition.

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