Research extensions

Read the textbook background, then follow a research result into its verified mathematical proofs and exact Lean graph locations.

These are Samplinglib extensions, not chapters or numbered results of Chewi’s book. Chapter links are reading context, not certified theorem dependencies. Counts are reviewed declarations, not paper-completion percentages. The same canonical proof is reused, never copied into a second theorem.

Proximal BPS

Research page · Textbook research extension · Ch. 1: The Langevin Diffusion in Continuous Time · Ch. 2: Functional Inequalities · Ch. 8: The Proximal Sampler

125 independently reviewed declarations: statements, proofs and graph locations

Actual centered original-gradient Poincare · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredDomainPoincare
Actual centered Gibbs original-gradient residual limit · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CenteredGibbsResolventLimit
C1 compact functions lie in the same closed gradient graph · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactC1GradientDomain
Actual compact weak Poisson: one smooth function/gradient/Laplacian sequence · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactPoissonSmoothGraph
Actual compact weak Poisson: complex Schwartz, TD and Sobolev · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeakPoissonSobolev
Actual compact weak Poisson: original weighted gradient domain and scalar coercivity · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.CompactWeightedPoissonCoercivity
Actual constants in original closed-gradient domain · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain
Dense closable gradient on the actual Gaussian outer marginal · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalGradient
Poincare for the actual Gaussian Gibbs marginal · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianMarginalPoincare
C1 regularity of the literal reflected Gaussian posterior mean · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.GaussianReflectedMean
The Gaussian posterior is an actual measurable conditional kernel · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernel
From a genuine Hessian bound to the normalized augmented Gibbs law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation
Actual normalized Gibbs C1 variance Poincare · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsC1Poincare
Actual same-original Gibbs zero-gradient kernel equality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernelEquality
Same original Gibbs closed-gradient zero implies AE constant · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsGradientKernel
A Gibbs L2 representative is locally Lebesgue L2 · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2
Actual global weighted resolvent scalar coercivity · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GlobalWeightedResolventCoercivity
Sharp quadratic corrector bound on a real Hilbert space · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound
The explicit density of isotropic Gaussian noise · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity
Positive real L² operators: equality from equal squares · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique
Positive real L² operator: genuine square root and energy · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot
Exact range of real L2 pullback · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange
Positive real L² operator: actual complexification · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator
Actual compact localization of the same weighted weak resolvent · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LocalizedWeakResolvent
Actual ordinary weak zero-gradient is AE constant · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.WeakGradientZero
The actual weighted weak resolvent satisfies an ordinary distribution Laplace equation · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.OrdinaryWeakResolvent
Actual PBPS next absolute-event-time law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime
Actual PBPS: why the reflected augmented transition preserves its target · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAugmentedKernelInvariance
Actual PBPS zero-safe bounce, rate and energy-layer bound · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate
Actual PBPS bounded Gibbs duality and fixed-time invariance · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality
Actual PBPS bounded path functional expansion · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedPathExpansion
Actual PBPS bounded-test integrability and expectation continuity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity
Actual PBPS conditional finite next-wait density · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitDensity
Actual PBPS conditional next-wait survival · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitSurvival
Actual PBPS corrector change under the reflected step · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorChange
Actual PBPS corrector perturbation with the same witnesses · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorPerturbation
Actual normalized PBPS countable endpoint law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw
Actual PBPS finite endpoint and event-time reversal · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal
Actual PBPS event-time nonaccumulation · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation
Actual PBPS finite-count complete-path law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath
Actual PBPS finite first-event density and post-bounce law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteFirstEventLaw
Actual PBPS one-step complete finite-history extension · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryExtension
Actual PBPS finite history and unused-clock tail law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw
Actual PBPS finite stopped postjump recursion · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion
Actual PBPS: detailed balance after independent reference averaging · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHalfTurnReversibility
Actual PBPS harmonic flow and conserved weighted energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow
Actual PBPS integrated hazard and first exponential clock · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock
Actual PBPS: one probability kernel and its real-L2 operator · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualKernelL2Realization
Actual PBPS fixed-time L2 expectation contraction · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation
Actual PBPS full real-L2 momentum-flip adjoint identity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality
Actual PBPS: L2 continuity at time zero, not yet a semigroup · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2StrongContinuity
Actual normalized PBPS endpoint-pair sector reversal · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector
Actual PBPS ordered finite-prefix law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix
Actual PBPS bounded-test outer square-integral continuity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOuterBoundedL2Continuity
Actual PBPS phase Gibbs normalization · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization
Actual PBPS phase-volume preservation and reversal · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume
Actual PBPS finite-time full-phase probability kernel · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel
Actual PBPS finite physical-time interval coverage · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover
Actual PBPS jointly measurable physical-time phase · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeMeasurability
Actual PBPS typed polar isometry and adjoint corrector · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.PolarIsometry
Actual Gaussian momentum averaging and position L2 self-adjoint contraction · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPositionL2Averaging
Actual PBPS finite-path energy and Gibbs/survival balance · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedGibbsSurvival
Actual PBPS prescribed-path hazard and density identity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity
Actual PBPS path reversal and survival-integral substitution · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversal
Actual PBPS finite-state reversal and incoming-rate product · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal
Actual PBPS weighted density under finite path reversal · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedWeightedDensity
Actual PBPS projected reflection rotation and exact pair energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualProjectedRotation
Actual PBPS reflection intertwining on the full conditional-complement space · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining
Same actual PBPS root and centered inverse commutation · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation
Actual PBPS phase-flow defect bound and zero-time stochastic continuity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualSmallTimeContinuity
Actual PBPS weighted finite-sector substitution · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector
Actual PBPS ambient adjoint and globally centered corrector · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector
Exact centered squared-defect coercivity and bounded inverse · Lean graphPaper-specific owning module: Tests.ProximalBPSCenteredDefect
Sharp contraction and defect gap for every centered macro input · Lean graphPaper-specific owning module: Tests.ProximalBPSMacroscopicRange
Actual PBPS centered root order and bounded inverse · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredRootOrderInverse
Actual centered selfadjoint operator and positive squared defect · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredDefectOperator
Closed gradients satisfy weighted compact-test integration by parts · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeak
Weighted Bochner identity from compact-test integration by parts · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochner
Bochner energy under the actual reflected conditional Gibbs kernel · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner
Actual PBPS conditional C1 weak-resolvent tests · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalC1Resolvent
Actual reflected conditional centered residual limit · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCenteredResolventLimit
Actual PBPS reflected resolvent: compact weighted coercivity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactCoercivity
Actual PBPS reflected resolvent: common compact smooth graph · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactSmoothGraph
Actual PBPS reflected global quarter-scale coercivity · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGlobalCoercivity
Sharp outer gradient energy for the actual reflected conditional mean · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientEnergy
Pointwise gradient–variance bound for the actual reflected conditional mean · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientVariance
Actual PBPS conditional closed-gradient zero implies AE constant · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernel
A dense closable gradient for a genuine Gibbs measure · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradient
The actual conditional PBPS gradient is densely defined and closable · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient
Actual PBPS reflected resolvent: one solution before all cutoffs · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent
Actual PBPS reflected resolvent: localized complex Sobolev · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedSobolev
Actual PBPS reflected conditional resolvents have the ordinary weak Laplacian · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalOrdinaryResolvent
A unique weak resolvent from a closed Hilbert graph · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolvent
Solve the weak equation on the actual conditional gradient closure · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent
Actual noncompact conditional scores in original closed gradient · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomain
Actual conditional curvature and the noncompact directional-score domain · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain
Actual reflected conditional Poincare and parameter-score variance · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreVariance
Actual reflected conditional expectation and its score derivative · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore
From the closed Gibbs gradient to ordinary weak derivatives · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistribution
Hilbert corrector perturbation identity · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorPerturbation
Ideal PBPS half-turn returned-position probability kernel · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel
The joint density of a Gaussian augmentation for any input law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation
The actual PBPS conditional mean on all of L2 · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.L2MacroscopicMean
Literal PBPS reflected Gibbs law and C1 compact mean · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.LiteralReflectedMean
Actual PBPS macroscopic range and centering · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange
Actual macroscopic reflection blocks and sharp smooth gradient energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy
The actual macroscopic reflection has a differentiable conditional representative · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRepresentative
Actual PBPS squared defect: positive complex lift · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.DefectComplexLift
Actual PBPS squared defect: positive real root and energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot
Actual reflection and conditional-projection blocks · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2
The closed-gradient resolvent is a genuine weak PDE solution · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolvent
The actual PBPS conditional mean gradient on all of L2 · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.RoughMeanGradient
Actual PBPS sharp first-corrector bound and Lemma B.3 consumer · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.SharpCorrectorEnergy
The actual PBPS source mean belongs to the closed-gradient domain · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.SourceMeanGradientDomain
Actual PBPS: the unique positive macroscopic defect root · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicDefectRoot
Actual PBPS scalar defect: unique positive real root · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRootUnique
Why reflecting the Gaussian auxiliary point preserves its joint law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection
Positive square commutation on arbitrary real L² · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute
Positive square order on arbitrary real L² · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareOrder
Actual scaled closed-graph resolvent norm limit · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ScaledClosedGraphResolvent
From an invariant Markov kernel to its genuine L2 observable operator · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelL2
From conditional detailed balance to a retained-coordinate joint kernel · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelRetainedReversibility
Actual countable unit-exponential product inputs · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.UnitExponentialProduct
Actual weighted C1 pair in original gradient closure · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedC1GradientDomain
The actual weak resolvent admits C1 compact weighted tests · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventC1

Smoothed Picard HMC

Research page · Textbook research extension · Ch. 2: Functional Inequalities · Ch. 5: Faster Low-Accuracy Samplers · Ch. 8: The Proximal Sampler

119 independently reviewed declarations: statements, proofs and graph locations

Actual affine normalized Gibbs transport · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.AffineGibbs
Actual finite-count Rademacher sums converge weakly to the unit Gaussian · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT
True finite Boolean function log-Sobolev inequality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
Bounded binary probability-product entropy, including zero fibers · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.InformationTheory.ProductEntropy
Actual compact Gaussian observer and homogeneous entropy limits · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy
Actual full Boolean flip-energy Gaussian limit · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianFlipEnergy
Compact finite-Hilbert standard Gaussian log-Sobolev inequality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactHilbertLogSobolev
Actual compact scalar Gaussian log-Sobolev inequality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactLogSobolev
Compact finite-product Gaussian log-Sobolev inequality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactProductLogSobolev
Actual posterior score and covariance identities · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity
Actual Gaussian convolution density and C2 normalized potential · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.GaussianConvolutionRegularity
Gaussian Lipschitz first moment and signed exponential domain · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential
Noncompact C2 Gaussian function log-Sobolev inequality · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianLogSobolev
Sharp standard Gaussian concentration for every Lipschitz observable · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.GaussianLipschitzExponential
Actual Gaussian-Gibbs square-root density and energy domains · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSqrtDensityDomain
Actual Gibbs covariance lower · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment
Actual Gibbs gradient has zero mean · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMean
Actual Gibbs linear covariance upper · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GibbsLinearCovarianceUpper
The genuine Hessian integral represents the full gradient difference · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.HessianSecantOperator
From a genuine Hessian lower bound to strong convexity · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity
A common Markov kernel cannot amplify total-variation error · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariation
Quadratic regularization shifts actual curvature and gradient smoothness · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization
Actual source smoothed Gibbs potential and preserved partition · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential
For every actual input pair and every common two-vector noise value, the source exact-gradient numerical phase obeys the \(M_\kappa\) norm contraction with simultaneous explicit universal constant c=1/65536 under \(h\Lambda_J\le c/\kappa\) · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualContraction
For every real kappa and phase point, define the exact source block-matrix quadratic form \(Q_\kappa\) · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric
For every real inner-product E, kappa>=1 and phase point z, the true coordinate energy is bounded by6 times the exact source Q · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric
For every real inner-product E, kappa>=1 and phase point z, the exact source Q is bounded by3/2 times the true coordinate energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric
Actual numerical phase: synchronous increment in the source metric · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualIncrement
Genuine nonlinear common-noise coupling and raw transport cost · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.RandomizedMapTransport
Actual Gaussian numerical kernel: integrated law and source transport contraction · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport
A measurable random-center RGO with actual joint recovery · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveCenterRGO
Actual adaptive backward-kernel KL error propagation · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLError
Actual approximate initialization gradient moments · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateInitialGradientMoment
Measurable stopped proximal execution with certified pointwise work · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution
Chebyshev-Lobatto nodes and integrated coefficient certificate · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoQuadrature
ChebyshevLobattoMomentum actual source component · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoMomentum
Actual clipped-gradient Poisson retry program · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram
Actual clipped-output exponential mean-error bounds · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential
Actual clipped and ideal RGO bidirectional RN moments · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparison
Counted phase program · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram
Counted phase work · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram
Actual finite-output KL with terminal residual discharged · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
Actual Gibbs enhanced-state one-step KL recurrence · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedKLOneStep
Actual enhanced-state termination and terminal FORS execution · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution
Actual finite recursive RGO KL error accumulation · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError
Finite threshold-absorbed RGO execution, terminal marginal and ideal recovery · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram
The actual exact-gradient Picard phase and its first-order difference · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifference
Actual proximal Gaussian oracle with sharp centered concentration · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FullRangeProximalGaussianOracle
Actual Gaussian gradient-arc joint law and calculus · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianArcLaw
Gaussian KL reverse transport from the actual quadratic transport budget · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL
Power perspective from Holder with infinite moments allowed · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspective
Actual Gaussian mixture reverse transport from a bounded coupling · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianMixture
The actual translated Gaussian likelihood and RN derivative · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihood
Exact integrable Gaussian RN power moment and normalized logarithm · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMoment
Actual Gaussian observation and finite recursive A1 budget · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget
Actual Gibbs gradient second moment · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment
Actual Gibbs position moment about a stationary point · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMoment
Actual unclipped gradient-arc mean · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean
Actual ideal RGO identification and normalization · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification
The actual implemented two-layer Picard phase kernel · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel
Both actual Picard query layers under the full phase law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseWork
A positive strongly convex potential attains its minimum · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexMinimizer
The SPHMC q=2 initialization bound with no supplied critical point · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransportUnconditional
Numerical initialization cost for the actual smoothed Gibbs phase law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransport
Couple the initial and reference phase laws with identical momentum · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialPhaseTransport
Actual joint inner reference stopping and expected count · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.JointReferenceGradientDescent
Full-dimensional kinetic drift dissipation in the actual source metric · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.KineticDissipation
Prescribed logarithmic terminal depth with explicit constants · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth
MonotoneProximalMap actual source component · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.MonotoneProximalMap
Actual normalized reference and returned sampling precision · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.NormalizedReferenceCall
Actual observation-conditioned retained-state execution · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernel
The squared norm of a standard Gaussian has mean d · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.StdGaussianMoment
The actual OU half-refresh and its corrected moment budget · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PartialMomentumRefresh
Actual phase accuracy and expected work with identical witnesses · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseAccuracyWork
Gaussian smoothing adds exactly one noise second moment · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment
The actual SPHMC product reference has controlled phase energy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment
Second moments through the two Picard query layers · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardCenterMoment
The actual independent Gaussian inputs for the first Picard layer · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardInputLaw
Actual Poisson rejection query tails with explicit constants · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTail
Actual bounded Poisson rejection output and full-batch cost · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejection
Actual Chebyshev-Lobatto momentum integrals are nonnegative · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.ChebyshevLobattoPositiveWeights
Actual proximal estimator: stability in both inputs · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalEstimatorLipschitz
Successful stopped executions have one output and count · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExecutionIdentity
Expected work of the actual proximal-query program · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExpectedWork
Actual proximal Gaussian estimator and its fiberwise moments · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimator
ProximalPhaseStability actual source component · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStability
A gradient-query interpreter that counts the successful test · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution
One truncation proxy for every Gaussian time and order · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport
Expected work of the same implemented query at its realized center · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RealizedProximalWork
Well-conditioned RGO update: finite variance and contraction · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVariance
Actual reference count under the recursive state law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingCost
Actual reference-carrying recursive Markov transition · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel
One actual RGO backward kernel: precision update, recovery and KL control · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward
RGO calculus: curvature, normalized target and condition-number update · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOCalculus
An RGO of an RGO has an explicit normalized target law · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosure
Actual smooth gradient-arc clipping excess · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClipping
Actual smooth gradient-arc exponential moment · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcMoment
Actual SPHMC smoothed Hessian bounds · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds
Actual source smoothed Hessian upper · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianUpper
True smoothed score and standardized posterior expectation · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedScorePosterior
Actual source quadrature and full phase work · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SourceQuadratureWork
Allpositive-step true standardized RGO position and Fisher · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOPositionFisher
True standardized RGO unique proximal point and finite canonical entropy · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGORelativeEntropy
True standardized RGO square-root density domains · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOSqrtDensity
Joint posterior recovery with measurable state-dependent RGO parameters · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO
Actual stopped Gaussian RGO output correctness under sampler interfaces · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOError
Actual RGO stopping depth and stability beyond the finite cap · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth
Actual terminal reference, FORS kernel and source program · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalFORSKernel
Actual terminal reference by gradient descent · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalReferenceGradientDescent
Actual terminal sampler accuracy and cached gradient costs · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalSamplerAccuracyCost
Evaluate canonical KL with an explicit normalized tilt ratio · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.InformationTheory.TiltedKL
A continuous transport cost attains its infimum · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost
The actual SPHMC truncation proxy from an infimum p-cost budget · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.Truncation
An actual two-noise RGO stage with the added-time KL denominator · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO
Why an ill-conditioned recursive stage makes geometric progress · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition
Numerical canonical KL bound for the actual standardized RGO · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOKLDimension
Canonical KL bound for the actual standardized RGO · Lean graphPaper-specific owning module: AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOKLFisher
Normalize a strongly convex Gibbs target without assuming its minimizer · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability
Signed two-point square entropy upper bound · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy

Gaussian Cloud · Part I

Research page · Textbook research extension · Ch. 5: Faster Low-Accuracy Samplers · Ch. 8: The Proximal Sampler

3 independently reviewed declarations: statements, proofs and graph locations

Average a history-dependent one-call kernel error · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
Later adaptive computation cannot amplify one replaced call · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope
Finite adjacent hybrid errors add · Lean graphCanonical shared module: AutoSamplingTheory.TechnicalLemmas.Probability.KernelHybridTelescope

Midpoint Langevin

Research page · Textbook research extension · Ch. 4: Analysis of Langevin Monte Carlo · Ch. 9: Lower Bounds for Sampling

No independently reviewed declaration is projected here yet. The source route remains open.

Gaussian Sampling Complexity

Research page · Textbook research extension · Ch. 9: Lower Bounds for Sampling

No independently reviewed declaration is projected here yet. The source route remains open.