test module
Tests
0 named declarations scanned from Tests.lean.
Declarations
This aggregator contains no named declarations.
Complete Lean source
Tests.lean — full module with imports and context
import Tests.SphereFeatureLawGradient
import Tests.FeatureDifferentiationTransport
import Tests.GaussianFeatureRegularity
import Tests.GaussianPolynomialRidge
import Tests.QuadraticFeatureRisk
import Tests.BoundedPerturbation
import Tests.Shared.SphereRayleigh
import Tests.Shared.SphereGradient
import Tests.Shared.CurveExtension
import Tests.Shared.AffineGradient
import Tests.GaussianLipschitzExponential
import Tests.StandardizedRGOPositionFisher
import Tests.FullRangeProximalGaussianOracle
import Tests.SmoothedHessianBounds
import Tests.CenteredPoincare
import Tests.Shared.UniformRegularization
import Tests.WeightedLocalL2
import Tests.SmoothedPicardHMCApproximateProximalExecution
import Tests.SmoothedPicardHMCProximalExpectedWork
import Tests.SmoothedPicardHMCPicardCenterMoment
import Tests.SmoothedPicardHMCPartialMomentumRefresh
import Tests.SmoothedPicardHMCImplementedPhaseKernel
import Tests.SmoothedPicardHMCRealizedProximalWork
import Tests.SmoothedPicardHMCImplementedPhaseWork
import Tests.SmoothedPicardHMCCountedPhaseProgram
import Tests.SmoothedPicardHMCSourceQuadrature
import Tests.SmoothedPicardHMCPositiveIntegralWeights
import Tests.HessianSecantOperator
import Tests.SmoothedPicardHMCProximalPhaseStability
import Tests.SmoothedPicardHMCPhaseAccuracyWork
import Tests.SmoothedPicardHMCKineticDissipation
import Tests.SmoothedPicardHMCFirstOrderDifference
import Tests.SmoothedPicardHMCActualContraction
import Tests.SmoothedPicardHMCActualIncrement
import Tests.SmoothedPicardHMCActualKernelTransport
import Tests.GaussianConvolutionRegularity
import Tests.GaussianConvolutionDerivatives
import Tests.SmoothedPicardHMCSmoothedGibbsPotential
import Tests.WassersteinLipschitzMoment
import Tests.SmoothedPicardHMCPhaseStateMoment
import Tests.SmoothedPicardHMCPhaseMetric
import Tests.SmoothedPicardHMCPhaseReferenceMoment
import Tests.SmoothedPicardHMCInitialPhaseTransport
import Tests.SmoothedPicardHMCInitialGibbsPhaseTransport
import Tests.SmoothedPicardHMCInitialGibbsPhaseTransportUnconditional
import Tests.Shared.QuadraticRegularizationOracle
import Tests.Shared.QuadraticRegularizationFirstOrder
import Tests.Shared.QuadraticRegularizationTransfer
import Tests.Shared.RestartLogComplexity
import Tests.Shared.RestartReduction
import Tests.Shared.GradientDescentComplexity
import Tests.Shared.GradientDescentRates
import Tests.Shared.GradientFlowLastIterate
import Tests.Shared.GradientFlowStationarity
import Tests.Shared.GradientFlowValue
import Tests.Shared.GradientFlowContraction
import Tests.Shared.GradientFlowPL
import Tests.Shared.StrongConvexPLPullback
import Tests.Shared.ConvexGradientGapSharpness
import Tests.Shared.GradientDescentSharpness
import Tests.Shared.QuadraticGradientDescent
import Tests.Shared.GradientDescentOptimalStep
import Tests.Shared.GradientDescentStationarity
import Tests.Shared.GradientDescentPL
import Tests.Basic
import Tests.HessianStrongConvexity
import Tests.QuadraticRegularization
import Tests.GibbsAugmentation
import Tests.SmoothedPicardRecursiveCondition
import Tests.SmoothedPicardRGOClosure
import Tests.StrongConvexGibbsIntegrability
import Tests.GibbsGradientMoment
import Tests.GibbsGradientMean
import Tests.SmoothedScorePosterior
import Tests.GaussianSqrtDensityDomain
import Tests.StandardizedRGOSqrtDensity
import Tests.StandardizedRGORelativeEntropy
import Tests.StandardizedRGOKLFisher
import Tests.StandardizedRGOKLDimension
import Tests.GibbsCovarianceLower
import Tests.IsotropicGaussianDensity
import Tests.ProximalBPSGaussianAugmentation
import Tests.ProximalBPSGaussianReflection
import Tests.BrownianMotion
import Tests.BrownianQuadraticVariation
import Tests.BrownianQuadraticVariationL2
import Tests.EmpiricalCovariance
import Tests.GaussianFourthMoment
import Tests.VectorBrownianFiltration
import Tests.EuclideanBrownianCoordinates
import Tests.CarreDuChamp
import Tests.CoefficientTruncation
import Tests.ContinuousCostWeakLowerSemicontinuity
import Tests.DisplacementInterpolation
import Tests.DisplacementInterpolationConstantSpeed
import Tests.DisplacementJacobianEntropy
import Tests.DiscreteDoobL2
import Tests.ContinuousDoobL2
import Tests.DyadicElementaryRefinement
import Tests.DyadicElementaryStopping
import Tests.DyadicGridStoppingIto
import Tests.DyadicHorizonExtension
import Tests.DyadicHorizonIto
import Tests.ElementaryItoIntegral
import Tests.ElementaryItoAlgebra
import Tests.ElementaryItoEmbedding
import Tests.ElementaryItoDoobL2
import Tests.ElementaryItoIsometry
import Tests.ElementaryItoL2
import Tests.ElementaryItoProcess
import Tests.ElementaryStoppingTime
import Tests.FellerSemigroup
import Tests.FiniteDimensionalNormBridge
import Tests.FiniteDimensionalItoProcess
import Tests.ProgressiveDriftIntegral
import Tests.ChewiItoProcess
import Tests.ChewiItoFormula
import Tests.FiniteTimeGrid
import Tests.GeneratorFunctionalInequalities
import Tests.GeodesicConvexity
import Tests.Shared.StrongConvexFirstOrder
import Tests.Shared.StrongConvexGradientConverse
import Tests.Shared.ConvexityC1
import Tests.Shared.ConvexityC2
import Tests.Shared.SmoothnessEquivalences
import Tests.Shared.ConvexSmoothGradient
import Tests.Shared.GradientDescentContraction
import Tests.Shared.GradientDescentValue
import Tests.ItoTerminalCompletion
import Tests.ItoHorizonConsistency
import Tests.ItoHorizonProcessConsistency
import Tests.ItoIntegralProcess
import Tests.ItoIntegralProcessAfterHorizon
import Tests.ItoIntegralProcessCongruence
import Tests.KantorovichDual
import Tests.KernelInvariance
import Tests.KernelTotalVariation
import Tests.KernelHybridTelescope
import Tests.LangevinCarreDuChamp
import Tests.LaggedDyadicApproximation
import Tests.LaggedDyadicConvergence
import Tests.LeftLebesgueAverage
import Tests.Localization
import Tests.MarkovSemigroup
import Tests.MarkovMeasureEvolution
import Tests.Martingale
import Tests.MetricCurve
import Tests.OperatorGenerator
import Tests.OperatorGeneratorDomain
import Tests.ProbabilityCouplingCompactness
import Tests.ProgressiveL2
import Tests.ProgressiveL2Density
import Tests.ProgressiveL2Algebra
import Tests.ProgressiveL2HorizonExtension
import Tests.ProgressiveL2Truncation
import Tests.ProgressiveL2Stopping
import Tests.QuadraticOptimalMapUniqueness
import Tests.RelativeFisher
import Tests.StoppingGraphNull
import Tests.GlobalLocalProgressiveL2
import Tests.GlobalCanonicalLocalizerLimit
import Tests.DyadicGlobalHorizon
import Tests.GlobalStoppedProgressiveL2
import Tests.GlobalStoppedL2Overlap
import Tests.GlobalStoppedItoMartingale
import Tests.GlobalItoProcessGluing
import Tests.ChewiProposition1_1_16
import Tests.RandomStoppingDyadicApprox
import Tests.RandomStoppingBoundary
import Tests.BoundedStoppedItoMean
import Tests.RandomStoppingProcessApprox
import Tests.RandomStoppingIntegrandLimit
import Tests.RandomStoppingProgressiveL2
import Tests.RandomStoppingL2Convergence
import Tests.RandomStoppingItoTerminal
import Tests.RandomStoppingL2Contraction
import Tests.RandomStoppingGeneralIto
import Tests.RandomStoppingProcessConsistency
import Tests.Reversibility
import Tests.SampledElementaryApproximation
import Tests.SemigroupDecay
import Tests.BakryEmeryInterpolation
import Tests.BakryEmeryCalculus
import Tests.BakryEmeryGradientContraction
import Tests.StoppingTime
import Tests.TimeMeasureRealBridge
import Tests.Transport
import Tests.WassersteinSpace
import Tests.AccumulatedEnergy
import Tests.LocalProgressiveL2
import Tests.PrefixIntegral
import Tests.EnergyPathContinuity
import Tests.CompletedEnergy
import Tests.CanonicalEnergyLocalizer
import Tests.CanonicalEnergyStoppingTime
import Tests.CanonicalRawLocalization
import Tests.CanonicalRawLocalizationL2
import Tests.CompletedIntegrand
import Tests.EnergyStoppedIntegrand
import Tests.EnergyStoppingBoundaryBridge
import Tests.EnergyStoppedProgressiveL2
import Tests.EnergyStoppingL2Bridge
import Tests.CanonicalLocalizationTheorem
import Tests.CanonicalStoppedItoIntegral
import Tests.EnergyStoppedItoOverlap
import Tests.GaussianConditionalKernel
import Tests.SmoothedPicardRGOCalculus
import Tests.SmoothedPicardRecursiveVariance
import Tests.SmoothedPicardRecursiveDepth
import Tests.SmoothedPicardLogarithmicDepth
import Tests.ProximalBPSReflectionL2
import Tests.ProximalBPSConditionalScore
import Tests.ProximalBPSConditionalGradientVariance
import Tests.ProximalBPSConditionalGradientEnergy
import Tests.ProximalBPSMacroscopicEnergy
import Tests.ProximalBPSGaussianMarginalGradient
import Tests.ProximalBPSGaussianReflectedMean
import Tests.ProximalBPSReflectedMeanRegularity
import Tests.ProximalBPSSourceMeanGradientDomain
import Tests.ProximalBPSL2MacroscopicMean
import Tests.ProximalBPSRoughMeanGradient
import Tests.GaussianMarginalPoincare
import Tests.ProximalBPSMacroscopicRange
import Tests.ProximalBPSCenteredDefect
import Tests.ProximalBPSDefectComplexLift
import Tests.ProximalBPSRealDefectRoot
import Tests.ProximalBPSRealDefectRootUnique
import Tests.ProximalBPSMacroscopicDefectRoot
import Tests.ProximalBPSCenteredRootOrderInverse
import Tests.ProximalBPSPolarIsometry
import Tests.ProximalBPSAmbientAdjointCorrector
import Tests.ProximalBPSActualRootCommutation
import Tests.ProximalBPSSharpCorrectorEnergy
import Tests.ProximalBPSMacroscopicRepresentative
import Tests.ProximalBPSConditionalScoreDomain
import Tests.ProximalBPSConditionalBochner
import Tests.ProximalBPSConditionalGradient
import Tests.WeakGradientZeroKernel
import Tests.WeightedC1GradientDomain
import Tests.ScaledResolventLimit
import Tests.ProximalBPSConditionalResolvent
import Tests.WeightedGradientWeak
import Tests.WeightedGradientDistribution
import Tests.WeightedResolvent
import Tests.CompactC1GradientDomain
import Tests.OrdinaryWeakResolvent
import Tests.LocalizedWeakResolvent
import Tests.CompactWeakPoissonSobolev
import Tests.CompactPoissonSmoothGraph
import Tests.CompactWeightedPoissonCoercivity
import Tests.GlobalWeightedResolventCoercivity
import Tests.SmoothedPicardHMCTruncation
import Tests.SmoothedPicardHMCGaussianPowerMoment
import Tests.SmoothedPicardHMCGaussianMixture
import Tests.SmoothedPicardHMCProxyReverseTransport
import Tests.SmoothedPicardHMCGaussianKL
import Tests.SmoothedPicardHMCRGOBackward
import Tests.SmoothedPicardHMCTwoNoiseRGO
import Tests.SmoothedPicardHMCAdaptiveCenterRGO
import Tests.SmoothedPicardHMCAdaptiveKLError
import Tests.SmoothedPicardHMCStateDependentRGO
import Tests.SmoothedPicardHMCFiniteRGOProgram
import Tests.SmoothedPicardHMCStoppedRGODepth
import Tests.SmoothedPicardHMCFiniteRGOKLError
import Tests.SmoothedPicardHMCGaussianRGOErrorBudget
import Tests.SmoothedPicardHMCStoppedGaussianRGOError
import Tests.SmoothedPicardHMCPoissonRejection
import Tests.SmoothedPicardHMCPoissonQueryTail
import Tests.SmoothedPicardHMCGaussianArcLaw
import Tests.SmoothedPicardHMCSmoothGradientArcMoment
import Tests.SmoothedPicardHMCSmoothGradientArcClipping
import Tests.SmoothedPicardHMCGradientArcMean
import Tests.SmoothedPicardHMCIdealRGOIdentification
import Tests.SmoothedPicardHMCClippedMeanExponential
import Tests.SmoothedPicardHMCClippedRenyiComparison
import Tests.SmoothedPicardHMCTerminalSamplerAccuracyCost
import Tests.SmoothedPicardHMCTerminalReferenceGradientDescent
import Tests.SmoothedPicardHMCApproximateInitialGradientMoment
import Tests.SmoothedPicardHMCJointReferenceGradientDescent
import Tests.SmoothedPicardHMCNormalizedReferenceCall
import Tests.SmoothedPicardHMCReferenceCarryingKernel
import Tests.SmoothedPicardHMCReferenceCarryingCost
import Tests.SmoothedPicardHMCTerminalFORSKernel
import Tests.SmoothedPicardHMCEnhancedTerminalExecution
import Tests.SmoothedPicardHMCObservationConditionalKernel
import Tests.SmoothedPicardHMCEnhancedKLOneStep
import Tests.SmoothedPicardHMCEnhancedFiniteOutputKL
import Tests.SmoothedPicardHMCProximalGaussianEstimator
import Tests.SmoothedPicardHMCGibbsPositionMoment
import Tests.SmoothedPicardHMCProximalEstimatorLipschitz
import Tests.SmoothedPicardHMCClippedGradientProgram
import Tests.TiltedLogRatio
import Tests.TiltedKL
import Tests.QuadraticTiltFisher
import Tests.CanonicalLogSobolev
import Tests.BernoulliLogSobolev
import Tests.BalancedRademacherCLT
import Tests.GaussianCompactEntropy
import Tests.GaussianFlipEnergy
import Tests.GaussianCompactLogSobolev
import Tests.GaussianCompactProductLogSobolev
import Tests.GaussianCompactHilbertLogSobolev
import Tests.GaussianLogSobolev
import Tests.ProductEntropy
import Tests.GradientAECongruence
import Tests.FinitePowerSeries
import Tests.UnitSphere
import Tests.SphereSecondOrder
import Tests.ExponentialKernelInterpolation
import Tests.ProximalBPSActualL2StrongContinuity
import Tests.ProximalBPSActualKernelL2Realization
import Tests.ProximalBPSActualHalfTurnReversibility
import Tests.ProximalBPSActualAugmentedKernelInvariance
import Tests.GaussianComplexityBlockFamily
import Tests.GaussianComplexityDeterminantCancellation
import Tests.GaussianComplexityExpectation
import Tests.GaussianComplexityKernelAxis
import Tests.GaussianComplexityKernelRotation
import Tests.GaussianComplexityLawDensity
import Tests.GaussianComplexityMixtureFubini
import Tests.GaussianComplexityNormalizer
import Tests.GaussianComplexityOrthogonalHaar
import Tests.GaussianComplexityRadialIntegral
import Tests.GaussianComplexitySingleBlock
import Tests.KernelL2
import Tests.KernelRetainedReversibility
import Tests.GaussianComplexityComponents
import Tests.GaussianComplexityMixtureLaws
import Tests.GaussianComplexityMixtureExpectation
import Tests.GaussianComplexityActualTotalVariation
import Tests.GaussianComplexityNumericSeparation
import Tests.GaussianComplexitySelectedTilt
import Tests.GaussianComplexityPoissonNormalization
import Tests.GaussianComplexityColumnTransport
import Tests.GaussianComplexitySurfaceLaw
import Tests.GaussianComplexityPoissonProduct
import Tests.Shared.SubgradientMethod
/-!
Focused Chapter 1.1 stochastic-calculus and Chapter 1.2 Markov/Feller tests are
part of the root target together with the compiled Registry count,
Registry-backed source correspondence, and Samplinglib declaration inventory.
-/