Finite-dimensional coordinates for posterior parameter pairs

Definition

KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Posterior.parameterSpace E is the Euclidean model indexed by the finite rank of $E\times(E\to_L[\mathbb R]E)$ , and parameterChart is a continuous linear equivalence from that parameter pair to its coordinate space. parameterScore is the continuous linear functional $(c,Q)\mapsto\langle c,x\rangle-\frac12\langle Qx,x\rangle$ , parameterFeature is its Riesz representative in the chart coordinates, and parameterRetract is the adjoint of the c-coordinate block. featureLaw pushes a probability measure on E forward through this feature map; the bundle establishes continuity of the score and feature maps but does not define a posterior expectation theorem.

Original module imports

import FunctionalInequalities.Probability.Posterior.Exponent
import FunctionalInequalities.Probability.Posterior.CompactPrior
import FunctionalInequalities.Probability.Posterior.Generator
import FunctionalInequalities.Probability.Posterior.CompactDomain
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.InnerProductSpace.LinearMap
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Normed.Operator.Banach

Original declaration excerpt

Shown in the original module context.

private abbrev parameterSpace := EuclideanSpace ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] E))))

Module navigation

Direct project imports: Probability/Posterior/Exponent, Probability/Posterior/CompactPrior, Probability/Posterior/Generator, Probability/Posterior/CompactDomain.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Posterior.JointRegularity · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Exponent
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactPrior
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Generator
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactDomain
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Adjoint
import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Analysis.InnerProductSpace.LinearMap
import Mathlib.Analysis.Normed.Module.FiniteDimension
import Mathlib.Analysis.Normed.Operator.Banach

noncomputable section
open MeasureTheory ProbabilityTheory FunctionalInequalities
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace Probability
namespace Posterior
section Chart
variable (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
/-- Euclidean model of the parameter space (implementation device). -/
 abbrev parameterSpace := EuclideanSpace ℝ (Fin (Module.finrank ℝ (E × (E →L[ℝ] E))))
/-- Euclidean coordinates of the parameter space `E × (E →L[ℝ] E)`; the operator norm is kept on the
second factor (this is a linear chart, not a whitening). -/
 def parameterChart : (E × (E →L[ℝ] E)) ≃L[ℝ]
    FunctionalInequalities.Probability.Posterior.parameterSpace E :=
  (Module.finBasis ℝ (E × (E →L[ℝ] E))).equivFunL.trans
    (PiLp.continuousLinearEquiv 2 ℝ
      (fun _ : Fin (Module.finrank ℝ (E × (E →L[ℝ] E))) => ℝ)).symm
/-- The exponent of (67) as a continuous linear functional of the parameter pair. -/
 def parameterScore (x : E) : (E × (E →L[ℝ] E)) →L[ℝ] ℝ :=
  (innerSL ℝ x).comp (ContinuousLinearMap.fst ℝ E (E →L[ℝ] E)) -
    (1 / 2 : ℝ) • ((innerSL ℝ x).comp
      ((ContinuousLinearMap.apply ℝ E x).comp (ContinuousLinearMap.snd ℝ E (E →L[ℝ] E))))
omit [FiniteDimensional ℝ E] in
 theorem continuous_parameterScore : Continuous (FunctionalInequalities.Probability.Posterior.parameterScore E) := by
  have hi : Continuous (fun x : E => innerSL ℝ x) := (InnerProductSpace.toDualMap ℝ E).continuous
  have he : Continuous (fun x : E =>
      (ContinuousLinearMap.apply ℝ E x).comp (ContinuousLinearMap.snd ℝ E (E →L[ℝ] E))) :=
    (ContinuousLinearMap.apply ℝ E).continuous.clm_comp_const _
  exact (hi.clm_comp_const _).sub ((hi.clm_comp he).const_smul (1 / 2 : ℝ))
/-- Riesz representative of the score in the chart coordinates. -/
 def parameterFeature (x : E) :
    FunctionalInequalities.Probability.Posterior.parameterSpace E :=
  (InnerProductSpace.toDual ℝ _).symm
    ((FunctionalInequalities.Probability.Posterior.parameterScore E x).comp (FunctionalInequalities.Probability.Posterior.parameterChart E).symm.toContinuousLinearMap)
 theorem continuous_parameterFeature : Continuous (FunctionalInequalities.Probability.Posterior.parameterFeature E) :=
  (InnerProductSpace.toDual ℝ _).symm.continuous.comp
    ((FunctionalInequalities.Probability.Posterior.continuous_parameterScore E).clm_comp_const (FunctionalInequalities.Probability.Posterior.parameterChart E).symm.toContinuousLinearMap)
 def parameterLinearBlock : E →L[ℝ]
    FunctionalInequalities.Probability.Posterior.parameterSpace E :=
  (FunctionalInequalities.Probability.Posterior.parameterChart E).toContinuousLinearMap.comp (ContinuousLinearMap.inl ℝ E (E →L[ℝ] E))
/-- The adjoint of the `c`-block of the chart retracts the feature to the point. -/
 def parameterRetract :
    FunctionalInequalities.Probability.Posterior.parameterSpace E →L[ℝ] E :=
  (FunctionalInequalities.Probability.Posterior.parameterLinearBlock E).adjoint
end Chart
section Expectation
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E]
  [MeasurableSpace E] [BorelSpace E]
/-- The prior pushed forward by the feature map (an internal device, not a new posterior object). -/
 def featureLaw (μ : ProbabilityMeasure E) :
    ProbabilityMeasure (FunctionalInequalities.Probability.Posterior.parameterSpace E) :=
  μ.map (FunctionalInequalities.Probability.Posterior.continuous_parameterFeature E).measurable.aemeasurable
end Expectation
end Posterior
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/JointRegularity.lean#L38-L117 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.JointRegularity`, definition bundle `KLSModular_FunctionalInequalities_Probability_Posterior_JointRegularity`; the repository is private at upload time).

View graph