Mathesis
Dhruv GuptaDhruv GuptaZetetic-Dhruvperson2026-09-24T00:00:00Z
ClaimMTH.C-2026-6022ArgumentMTH.R-2026-6022

Closed form of the multivariate Gaussian KL divergence (M3b). For positive-definite covariances S₁, S₂, KL(N(m₁,S₁) ‖ N(m₂,S₂)) = ½ ( log(det S₂ / det S₁) + tr(S₂⁻¹ S₁) + ⟪m₁-m₂, S₂⁻¹(m₁-m₂)⟫ - d ).

The whitening reduction (klDivReal_multivariateGaussian_whiten) sends the pair to a KL against the standard Gaussian (klDivReal_multivariateGaussian_stdGaussian); the three scalar invariants of the whitened covariance (det_whitened, trace_whitened, normSq_cfcSqrt_inv_apply) then identify the arguments.

DeclProbabilityTheory.klDivReal_multivariateGaussian
∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m₁ m₂ : EuclideanSpace ℝ ι) {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef →
    S₂.PosDef →
      InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian m₁ S₁)
          (ProbabilityTheory.multivariateGaussian m₂ S₂) =
        1 / 2 *
          (Real.log (S₂.det / S₁.det) + (S₂⁻¹ * S₁).trace + (m₁ - m₂).ofLp ⬝ᵥ S₂⁻¹.mulVec (m₁.ofLp - m₂.ofLp) -
            ↑(Fintype.card ι))
TopicInformation theory
Layout
ThesisStepHypothesisDefinition
klDivReal_multivariateGau…theoremS₁.PosDefhS₁S₂.PosDefhS₂trace_whitenedtheoremposDef_whitenedtheoremnormSq_cfcSqrt_inv_applytheoremconjTranspose_cfcSqrt_invtheoremconjTranspose_cfcSqrttheoremcfcSqrt_inv_mul_selftheoremklDivReal_multivariateGau…theoremmultivariateGaussian_eq_m…theoremgaussianAffineEquiv_applytheoremgaussianAffineEquiv_symm_…theoremklDivReal_multivariateGau…theoremnormSq_toEuclideanCLM_of_…theoremmap_multivariateGaussian_…theoremklDivReal_multivariateGau…theoremmultivariateGaussian_diag…theoremmap_stdGaussian_affinetheoreminner_adjoint_toEuclidean…theoremadjoint_toEuclideanCLMtheoremklDiv_gaussianReal_ne_toptheoremklDivReal_pi'theoremklDiv_pi'theoremklDiv_pitheoremklDiv_prodtheoremklDiv_prod_same_lefttheoremklDiv_map_equivtheoremllr_map_equivtheoremklDivReal_eq_toReal_klDivtheoremintegrand_eq_llrtheoremklDivReal_gaussianRealtheoremrnDeriv_gaussianReal_ratiotheoremlog_gaussianPDFRealtheoremintegral_sq_sub_consttheoremintegral_sub_mean_selftheoremintegral_sq_sub_mean_selftheoremklDivReal_map_measurableE…theoremdet_whitenedtheoremisUnit_det_cfcSqrttheoremklDivRealdefgaussianAffineEquivdeftoEuclideanCLEdeftoLpMeasurableEquivdef
  1. DeclProbabilityTheory.klDivReal_multivariateGaussianDeclaration kindtheorem
    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m₁ m₂ : EuclideanSpace ℝ ι) {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef →
    S₂.PosDef →
      InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian m₁ S₁)
          (ProbabilityTheory.multivariateGaussian m₂ S₂) =
        1 / 2 *
          (Real.log (S₂.det / S₁.det) + (S₂⁻¹ * S₁).trace + (m₁ - m₂).ofLp ⬝ᵥ S₂⁻¹.mulVec (m₁.ofLp - m₂.ofLp) -
            ↑(Fintype.card ι))
    InformationTheory.klDivReal
    Uses
  2. DeclProbabilityTheory.trace_whitenedDeclaration kindtheorem

    tr C(S₁,S₂) = tr(S₂⁻¹ S₁).

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef →
    S₂.PosDef →
      ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁ * ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁).conjTranspose).trace = (S₂⁻¹ * S₁).trace
    Uses
    Used by
  3. DeclProbabilityTheory.posDef_whitenedDeclaration kindtheorem

    The whitened covariance (√S₂⁻¹ √S₁)(√S₂⁻¹ √S₁)ᴴ is positive-definite (its factor is invertible).

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef → S₂.PosDef → ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁ * ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁).conjTranspose).PosDef
    Uses
    Used by
  4. DeclProbabilityTheory.normSq_cfcSqrt_inv_applyDeclaration kindtheorem

    The whitening map preserves the quadratic form: ‖√S₂⁻¹ v‖² = ⟪v, S₂⁻¹ v⟫.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {S₂ : Matrix ι ι ℝ},
  S₂.PosDef → ∀ (v : EuclideanSpace ℝ ι), ‖(Matrix.toEuclideanCLM (CFC.sqrt S₂)⁻¹) v‖ ^ 2 = v.ofLp ⬝ᵥ S₂⁻¹.mulVec v.ofLp
    Uses
    Used by
  5. DeclProbabilityTheory.conjTranspose_cfcSqrt_invDeclaration kindtheorem

    The inverse of a functional-calculus square root is self-adjoint.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (S : Matrix ι ι ℝ),
  (CFC.sqrt S)⁻¹.conjTranspose = (CFC.sqrt S)⁻¹
    Uses
    Used by
  6. DeclProbabilityTheory.conjTranspose_cfcSqrtDeclaration kindtheorem

    The functional-calculus square root of a matrix is self-adjoint.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (S : Matrix ι ι ℝ), (CFC.sqrt S).conjTranspose = CFC.sqrt S
    Used by
  7. DeclProbabilityTheory.cfcSqrt_inv_mul_selfDeclaration kindtheorem

    (√S)⁻¹ (√S)⁻¹ = S⁻¹ for positive-definite S.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {S : Matrix ι ι ℝ},
  S.PosDef → (CFC.sqrt S)⁻¹ * (CFC.sqrt S)⁻¹ = S⁻¹
    Used by
  8. DeclProbabilityTheory.klDivReal_multivariateGaussian_whitenDeclaration kindtheorem

    Whitening reduction of the multivariate Gaussian KL. For positive-definite S₂, pushing both measures through the whitening equivalence (gaussianAffineEquiv m₂ hS₂).symm reduces the KL divergence of two multivariate Gaussians to a KL against the standard Gaussian, with whitened mean √S₂⁻¹ (m₁ − m₂) and covariance (√S₂⁻¹ √S₁)(√S₂⁻¹ √S₁)ᴴ.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m₁ m₂ : EuclideanSpace ℝ ι) (S₁ S₂ : Matrix ι ι ℝ),
  S₂.PosDef →
    InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian m₁ S₁)
        (ProbabilityTheory.multivariateGaussian m₂ S₂) =
      InformationTheory.klDivReal
        (ProbabilityTheory.multivariateGaussian ((Matrix.toEuclideanCLM (CFC.sqrt S₂)⁻¹) (m₁ - m₂))
          ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁ * ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁).conjTranspose))
        (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι))
    InformationTheory.klDivRealProbabilityTheory.gaussianAffineEquiv
    Uses
    Used by
  9. DeclProbabilityTheory.multivariateGaussian_eq_map_gaussianAffineEquivDeclaration kindtheorem

    multivariateGaussian m S is the pushforward of the standard Gaussian by the affine equivalence gaussianAffineEquiv m hS.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ}
  (hS : S.PosDef),
  ProbabilityTheory.multivariateGaussian m S =
    MeasureTheory.Measure.map (⇑(ProbabilityTheory.gaussianAffineEquiv m hS))
      (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι))
    ProbabilityTheory.gaussianAffineEquiv
    Uses
    Used by
  10. DeclProbabilityTheory.gaussianAffineEquiv_applyDeclaration kindtheorem

    gaussianAffineEquiv m hS is the affine map z ↦ m + √S z.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosDef)
  (z : EuclideanSpace ℝ ι), (ProbabilityTheory.gaussianAffineEquiv m hS) z = m + (Matrix.toEuclideanCLM (CFC.sqrt S)) z
    ProbabilityTheory.gaussianAffineEquivProbabilityTheory.toEuclideanCLE
    Uses
    Used by
  11. DeclProbabilityTheory.gaussianAffineEquiv_symm_applyDeclaration kindtheorem

    The whitening map: the inverse of gaussianAffineEquiv m hS is z ↦ √S⁻¹ (z - m).

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (m : EuclideanSpace ℝ ι) {S : Matrix ι ι ℝ} (hS : S.PosDef)
  (z : EuclideanSpace ℝ ι),
  (ProbabilityTheory.gaussianAffineEquiv m hS).symm z = (Matrix.toEuclideanCLM (CFC.sqrt S)⁻¹) (z - m)
    ProbabilityTheory.gaussianAffineEquivProbabilityTheory.toEuclideanCLE
    Uses
    Used by
  12. DeclProbabilityTheory.klDivReal_multivariateGaussian_stdGaussianDeclaration kindtheorem

    Closed form of the multivariate Gaussian KL against the standard Gaussian. For a positive-definite covariance C, klDivReal (N(w, C)) (stdGaussian) = ½ ( -log det C + tr C + ‖w‖² - d ).

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (w : EuclideanSpace ℝ ι) {C : Matrix ι ι ℝ},
  C.PosDef →
    InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian w C)
        (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) =
      1 / 2 * (-Real.log C.det + C.trace + ‖w‖ ^ 2 - ↑(Fintype.card ι))
    InformationTheory.klDivRealProbabilityTheory.toEuclideanCLE
    Uses
    Used by
  13. DeclProbabilityTheory.normSq_toEuclideanCLM_of_isometryDeclaration kindtheorem

    An orthogonal change of variables preserves the Euclidean norm: if Mᴴ M = 1 then ‖toEuclideanCLM M w‖² = ‖w‖².

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {M : Matrix ι ι ℝ},
  M.conjTranspose * M = 1 → ∀ (w : EuclideanSpace ℝ ι), ‖(Matrix.toEuclideanCLM M) w‖ ^ 2 = ‖w‖ ^ 2
    Uses
    Used by
  14. DeclProbabilityTheory.map_multivariateGaussian_affineDeclaration kindtheorem

    General affine image of a multivariate Gaussian. For positive-semidefinite covariance S, the affine pushforward x ↦ a + B x of multivariateGaussian μ S is the multivariate Gaussian with transported mean a + B μ and congruent covariance B * S * Bᴴ. This is the covariance- transport engine of the diagonalization step: an orthogonal B = Uᵀ sends the whitened covariance to its eigenvalue diagonal Uᵀ S U. Proved by composing the two affine maps and reducing to the standard-Gaussian image map_stdGaussian_affine, using √S · √Sᴴ = √S · √S = S.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (a μ : EuclideanSpace ℝ ι) (B S : Matrix ι ι ℝ),
  S.PosSemidef →
    MeasureTheory.Measure.map (fun x => a + (Matrix.toEuclideanCLM B) x) (ProbabilityTheory.multivariateGaussian μ S) =
      ProbabilityTheory.multivariateGaussian (a + (Matrix.toEuclideanCLM B) μ) (B * S * B.conjTranspose)
    Uses
    Used by
  15. DeclProbabilityTheory.klDivReal_multivariateGaussian_diagonal_stdGaussianDeclaration kindtheorem

    KL of a diagonal multivariate Gaussian against the standard Gaussian, tensorized. For strictly positive diagonal covariance d > 0, klDivReal (mvG μ (diagonal d)) stdGaussian = ∑ᵢ ½(-log dᵢ + dᵢ + μᵢ² - 1), the coordinatewise sum of the scalar Gaussian-Gaussian KL closed forms. This is the diagonalized-and-tensorized leg of the multivariate Gaussian KL closed form.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (μ : EuclideanSpace ℝ ι) (d : ι → ℝ),
  (∀ (i : ι), 0 < d i) →
    InformationTheory.klDivReal (ProbabilityTheory.multivariateGaussian μ (Matrix.diagonal d))
        (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) =
      ∑ i, 1 / 2 * (-Real.log (d i) + d i + μ.ofLp i ^ 2 - 1)
    InformationTheory.klDivRealProbabilityTheory.toLpMeasurableEquiv
    Uses
    Used by
  16. DeclProbabilityTheory.multivariateGaussian_diagonal_eq_map_piDeclaration kindtheorem

    A diagonal multivariate Gaussian is a pushed-forward product of scalar Gaussians. For d ≥ 0, multivariateGaussian μ (diagonal d) is the image under toLp 2 of the product measure ∏ᵢ gaussianReal μᵢ dᵢ.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (μ : EuclideanSpace ℝ ι) (d : ι → ℝ),
  (∀ (i : ι), 0 ≤ d i) →
    ProbabilityTheory.multivariateGaussian μ (Matrix.diagonal d) =
      MeasureTheory.Measure.map (WithLp.toLp 2)
        (MeasureTheory.Measure.pi fun i => ProbabilityTheory.gaussianReal (μ.ofLp i) (d i).toNNReal)
    Uses
    Used by
  17. DeclProbabilityTheory.map_stdGaussian_affineDeclaration kindtheorem

    The affine image z ↦ a + B z of the standard Gaussian on EuclideanSpace ℝ ι is the multivariate Gaussian with mean a and covariance B * Bᴴ.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (a : EuclideanSpace ℝ ι) (B : Matrix ι ι ℝ),
  MeasureTheory.Measure.map (fun z => a + (Matrix.toEuclideanCLM B) z)
      (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ ι)) =
    ProbabilityTheory.multivariateGaussian a (B * B.conjTranspose)
    Uses
    Used by
  18. DeclProbabilityTheory.inner_adjoint_toEuclideanCLMDeclaration kindtheorem

    The real inner product of the two adjoint images (toEuclideanCLM B)ᴴ x and (toEuclideanCLM B)ᴴ y equals the quadratic form x ⬝ᵥ (B * Bᴴ) *ᵥ y.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (B : Matrix ι ι ℝ) (x y : EuclideanSpace ℝ ι),
  inner ℝ ((ContinuousLinearMap.adjoint (Matrix.toEuclideanCLM B)) x)
      ((ContinuousLinearMap.adjoint (Matrix.toEuclideanCLM B)) y) =
    x.ofLp ⬝ᵥ (B * B.conjTranspose).mulVec y.ofLp
    Uses
    Used by
  19. DeclProbabilityTheory.adjoint_toEuclideanCLMDeclaration kindtheorem

    The adjoint of toEuclideanCLM B is toEuclideanCLM Bᴴ: toEuclideanCLM is a star algebra equivalence, so it carries the matrix conjugate transpose to the operator adjoint.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (B : Matrix ι ι ℝ),
  ContinuousLinearMap.adjoint (Matrix.toEuclideanCLM B) = Matrix.toEuclideanCLM B.conjTranspose
    Used by
  20. DeclInformationTheory.klDiv_gaussianReal_ne_topDeclaration kindtheorem

    Finiteness of the one-dimensional Gaussian-Gaussian KL divergence. For variance parameters v₁ ≠ 0, v₂ ≠ 0, the ℝ≥0∞-valued klDiv (N(m₁, v₁)) (N(m₂, v₂)) is finite. This is the integrability side-condition that klDivReal_pi requires per coordinate: the log-likelihood ratio is P-a.e. an explicit quadratic, whose square-integrability against P = N(m₁, v₁) is the finiteness of the second moment.

    ∀ {m₁ m₂ : ℝ} {v₁ v₂ : NNReal},
  v₁ ≠ 0 →
    v₂ ≠ 0 → InformationTheory.klDiv (ProbabilityTheory.gaussianReal m₁ v₁) (ProbabilityTheory.gaussianReal m₂ v₂) ≠ ⊤
    Uses
    Used by
  21. DeclInformationTheory.klDivReal_pi'Declaration kindtheorem

    KL tensorization for klDivReal over an arbitrary finite product (general Fintype index): the real-valued analogue of klDiv_pi'.

    ∀ {ι : Type u_3} [inst : Fintype ι] {X : ι → Type u_4} {mX : (i : ι) → MeasurableSpace (X i)}
  (P Q : (i : ι) → MeasureTheory.Measure (X i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (Q i)],
  (∀ (i : ι), (P i).AbsolutelyContinuous (Q i)) →
    (∀ (i : ι), InformationTheory.klDiv (P i) (Q i) ≠ ⊤) →
      InformationTheory.klDivReal (MeasureTheory.Measure.pi P) (MeasureTheory.Measure.pi Q) =
        ∑ i, InformationTheory.klDivReal (P i) (Q i)
    InformationTheory.klDivReal
    Uses
    Used by
  22. DeclInformationTheory.klDiv_pi'Declaration kindtheorem

    KL tensorization over an arbitrary finite product (general Fintype index). Reduces to the Fin-indexed klDiv_pi by reindexing through ι ≃ Fin (card ι).

    ∀ {ι : Type u_3} [inst : Fintype ι] {X : ι → Type u_4} {mX : (i : ι) → MeasurableSpace (X i)}
  (P Q : (i : ι) → MeasureTheory.Measure (X i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)]
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (Q i)],
  InformationTheory.klDiv (MeasureTheory.Measure.pi P) (MeasureTheory.Measure.pi Q) =
    ∑ i, InformationTheory.klDiv (P i) (Q i)
    Uses
    Used by
  23. DeclInformationTheory.klDiv_piDeclaration kindtheorem

    KL tensorization over a finite product, indexed by Fin (n+1): klDiv (Measure.pi P) (Measure.pi Q) = ∑ i, klDiv (P i) (Q i).

    ∀ {n : ℕ} {X : Fin n → Type u_3} {mX : (i : Fin n) → MeasurableSpace (X i)}
  (P Q : (i : Fin n) → MeasureTheory.Measure (X i)) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (P i)]
  [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (Q i)],
  InformationTheory.klDiv (MeasureTheory.Measure.pi P) (MeasureTheory.Measure.pi Q) =
    ∑ i, InformationTheory.klDiv (P i) (Q i)
    Uses
    Used by
  24. DeclInformationTheory.klDiv_prodDeclaration kindtheorem

    Binary KL tensorization. For probability measures, klDiv (μ.prod ν) (μ'.prod ν') = klDiv μ μ' + klDiv ν ν'.

    ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ μ' : MeasureTheory.Measure α)
  (ν ν' : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsProbabilityMeasure μ']
  [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure ν'],
  InformationTheory.klDiv (μ.prod ν) (μ'.prod ν') = InformationTheory.klDiv μ μ' + InformationTheory.klDiv ν ν'
    Uses
    Used by
  25. DeclInformationTheory.klDiv_prod_same_leftDeclaration kindtheorem

    Two products sharing the same first marginal reduce to the second-coordinate KL: klDiv (μ.prod ν) (μ.prod ν') = klDiv ν ν'.

    ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  (ν ν' : MeasureTheory.Measure β) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ν'], InformationTheory.klDiv (μ.prod ν) (μ.prod ν') = InformationTheory.klDiv ν ν'
    Uses
    Used by
  26. DeclInformationTheory.klDiv_map_equivDeclaration kindtheorem

    KL invariance under a measurable equivalence (ℝ≥0∞-valued). For finite measures μ, ν and a measurable equivalence e : α ≃ᵐ β, klDiv (μ.map e) (ν.map e) = klDiv μ ν.

    ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β)
  (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν],
  InformationTheory.klDiv (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) =
    InformationTheory.klDiv μ ν
    Uses
    Used by
  27. DeclInformationTheory.llr_map_equivDeclaration kindtheorem

    The log-likelihood ratio is invariant (a.e.) under pushforward by a measurable equivalence: llr (μ.map e) (ν.map e) (e x) =ᵐ[ν] llr μ ν x.

    ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β)
  (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν],
  (fun x => MeasureTheory.llr (MeasureTheory.Measure.map (⇑e) μ) (MeasureTheory.Measure.map (⇑e) ν) (e x)) =ᵐ[ν]
    MeasureTheory.llr μ ν
    Used by
  28. DeclInformationTheory.klDivReal_eq_toReal_klDivDeclaration kindtheorem

    For probability measures with P ≪ Q, the ℝ-valued KL equals (Mathlib.klDiv P Q).toReal. Both measures have total mass 1, so the Mathlib correction term vanishes.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P]
  [MeasureTheory.IsProbabilityMeasure Q],
  P.AbsolutelyContinuous Q → InformationTheory.klDivReal P Q = (InformationTheory.klDiv P Q).toReal
    InformationTheory.klDivReal
    Uses
    Used by
  29. DeclInformationTheory.integrand_eq_llrDeclaration kindtheorem

    The integrand log ((P.rnDeriv Q x).toReal) is definitionally Mathlib's log-likelihood ratio llr P Q x.

    ∀ {α : Type u_1} [inst : MeasurableSpace α] (P Q : MeasureTheory.Measure α),
  (fun x => Real.log (P.rnDeriv Q x).toReal) = MeasureTheory.llr P Q
    Used by
  30. DeclInformationTheory.klDivReal_gaussianRealDeclaration kindtheorem

    Closed form of the 1-D Gaussian-Gaussian KL divergence. For variance parameters v₁ ≠ 0, v₂ ≠ 0, KL( N(m₁, v₁) ‖ N(m₂, v₂) ) = ½ ( log(v₂/v₁) + (v₁ + (m₁-m₂)²)/v₂ - 1 ).

    ∀ {m₁ m₂ : ℝ} {v₁ v₂ : NNReal},
  v₁ ≠ 0 →
    v₂ ≠ 0 →
      InformationTheory.klDivReal (ProbabilityTheory.gaussianReal m₁ v₁) (ProbabilityTheory.gaussianReal m₂ v₂) =
        1 / 2 * (Real.log (↑v₂ / ↑v₁) + (↑v₁ + (m₁ - m₂) ^ 2) / ↑v₂ - 1)
    InformationTheory.klDivReal
    Uses
    Used by
  31. DeclInformationTheory.rnDeriv_gaussianReal_ratioDeclaration kindtheorem

    The Radon-Nikodym derivative of one real Gaussian w.r.t. another is, volume-a.e., the ratio of their densities.

    ∀ {m₁ m₂ : ℝ} {v₁ v₂ : NNReal},
  v₁ ≠ 0 →
    v₂ ≠ 0 →
      (ProbabilityTheory.gaussianReal m₁ v₁).rnDeriv (ProbabilityTheory.gaussianReal m₂ v₂) =ᵐ[MeasureTheory.volume]
        fun x => ProbabilityTheory.gaussianPDF m₁ v₁ x / ProbabilityTheory.gaussianPDF m₂ v₂ x
    Used by
  32. DeclInformationTheory.log_gaussianPDFRealDeclaration kindtheorem

    log (gaussianPDFReal m v x) = -½ log(2πv) - (x - m)²/(2v) for v ≠ 0.

    ∀ {m₁ : ℝ} {v₁ : NNReal},
  v₁ ≠ 0 →
    ∀ (x : ℝ),
      Real.log (ProbabilityTheory.gaussianPDFReal m₁ v₁ x) =
        -(1 / 2) * Real.log (2 * Real.pi * ↑v₁) - (x - m₁) ^ 2 / (2 * ↑v₁)
    Used by
  33. DeclInformationTheory.integral_sq_sub_constDeclaration kindtheorem

    ∫ (x - m₂)² ∂gaussianReal m₁ v₁ = v₁ + (m₁ - m₂)² (bias-variance split).

    ∀ {m₁ m₂ : ℝ} {v₁ : NNReal}, ∫ (x : ℝ), (x - m₂) ^ 2 ∂ProbabilityTheory.gaussianReal m₁ v₁ = ↑v₁ + (m₁ - m₂) ^ 2
    Uses
    Used by
  34. DeclInformationTheory.integral_sub_mean_selfDeclaration kindtheorem

    ∫ (x - m₁) ∂gaussianReal m₁ v₁ = 0.

    ∀ {m₁ : ℝ} {v₁ : NNReal}, ∫ (x : ℝ), x - m₁ ∂ProbabilityTheory.gaussianReal m₁ v₁ = 0
    Used by
  35. DeclInformationTheory.integral_sq_sub_mean_selfDeclaration kindtheorem

    ∫ (x - m₁)² ∂gaussianReal m₁ v₁ = v₁.

    ∀ {m₁ : ℝ} {v₁ : NNReal}, ∫ (x : ℝ), (x - m₁) ^ 2 ∂ProbabilityTheory.gaussianReal m₁ v₁ = ↑v₁
    Used by
  36. DeclInformationTheory.klDivReal_map_measurableEquivDeclaration kindtheorem

    KL invariance under a measurable equivalence. For σ-finite measures P, Q on α and a measurable equivalence e : α ≃ᵐ β, klDivReal (P.map e) (Q.map e) = klDivReal P Q.

    ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β)
  (P Q : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite P] [MeasureTheory.SigmaFinite Q],
  InformationTheory.klDivReal (MeasureTheory.Measure.map (⇑e) P) (MeasureTheory.Measure.map (⇑e) Q) =
    InformationTheory.klDivReal P Q
    InformationTheory.klDivReal
    Used by
  37. DeclProbabilityTheory.det_whitenedDeclaration kindtheorem

    det C(S₁,S₂) = det S₁ / det S₂.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] {S₁ S₂ : Matrix ι ι ℝ},
  S₁.PosDef →
    S₂.PosDef → ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁ * ((CFC.sqrt S₂)⁻¹ * CFC.sqrt S₁).conjTranspose).det = S₁.det / S₂.det
    Uses
    Used by
  38. DeclProbabilityTheory.isUnit_det_cfcSqrtDeclaration kindtheorem

    For a positive-definite matrix S, the functional-calculus square root has invertible determinant: (CFC.sqrt S).det ^ 2 = S.det > 0, so the sqrt is itself invertible.

    ∀ {ι : Type u_1} [inst : Fintype ι] [inst_1 : DecidableEq ι] (S : Matrix ι ι ℝ), S.PosDef → IsUnit (CFC.sqrt S).det
    Used by
  39. HypothesishS₁
    S₁.PosDef
  40. HypothesishS₂
    S₂.PosDef
  41. DefinitionInformationTheory.klDivRealdef

    ℝ-valued KL divergence. Returns 0 when P is not absolutely continuous with respect to Q (by convention; the ℝ≥0∞-valued klDiv returns ⊤ in that case).

    {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → MeasureTheory.Measure α → ℝ
  42. DefinitionProbabilityTheory.gaussianAffineEquivdef

    The defining affine map z ↦ m + √S z of multivariateGaussian m S, as a measurable equivalence for positive-definite S (whose functional-calculus square root is invertible).

    {ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] → EuclideanSpace ℝ ι → {S : Matrix ι ι ℝ} → S.PosDef → EuclideanSpace ℝ ι ≃ᵐ EuclideanSpace ℝ ι
  43. DefinitionProbabilityTheory.toEuclideanCLEdef

    An invertible matrix as a continuous linear equivalence on EuclideanSpace ℝ ι.

    {ι : Type u_1} →
  [inst : Fintype ι] →
    [inst_1 : DecidableEq ι] → (M : Matrix ι ι ℝ) → IsUnit M.det → EuclideanSpace ℝ ι ≃L[ℝ] EuclideanSpace ℝ ι
  44. DefinitionProbabilityTheory.toLpMeasurableEquivdef

    The Euclidean identification toLp 2 : (ι → ℝ) → EuclideanSpace ℝ ι as a measurable equivalence, used to transport the tensorization of Measure.pi onto EuclideanSpace.

    {ι : Type u_1} → [Fintype ι] → (ι → ℝ) ≃ᵐ EuclideanSpace ℝ ι
DOIMTH.R-2026-6022
Cite

Verification

Replay
accepted
Axioms
Classical.choiceQuot.soundpropext
Statement identity
not-applicable
Substrate
Lean 4 kernel v4.31.0
Dictionary pin
design-lab@5802df4 · initial
Frozen export
40c078c5fc77
Verified
2026-09-24T00:00:00Z