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.

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