AutoSamplingTheory.ExampleCases

import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOPositionFisher
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOSqrtDensity
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGORelativeEntropy
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOKLFisher
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StandardizedRGOKLDimension
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FullRangeProximalGaussianOracle
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianBounds
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreVariance
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientVariance
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientEnergy
import AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicEnergy
import AutoSamplingTheory.ExampleCases.ProximalBPS.LiteralReflectedMean
import AutoSamplingTheory.ExampleCases.ProximalBPS.SourceMeanGradientDomain
import AutoSamplingTheory.ExampleCases.ProximalBPS.L2MacroscopicMean
import AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRange
import AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredDefectOperator
import AutoSamplingTheory.ExampleCases.ProximalBPS.DefectComplexLift
import AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRoot
import AutoSamplingTheory.ExampleCases.ProximalBPS.RealDefectRootUnique
import AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicDefectRoot
import AutoSamplingTheory.ExampleCases.ProximalBPS.CenteredRootOrderInverse
import AutoSamplingTheory.ExampleCases.ProximalBPS.PolarIsometry
import AutoSamplingTheory.ExampleCases.ProximalBPS.AmbientAdjointCorrector
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualRootCommutation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionIntertwining
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualProjectedRotation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorChange
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCorrectorPerturbation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHarmonicFlow
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBounceRate
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualHazardClock
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteJumpRecursion
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNonaccumulation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeCover
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhysicalTimeMeasurability
import AutoSamplingTheory.ExampleCases.ProximalBPS.IdealHalfTurnKernel
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualSmallTimeContinuity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedTestContinuity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOuterBoundedL2Continuity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseTransitionKernel
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteFirstEventLaw
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryTailLaw
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitSurvival
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualConditionalNextWaitDensity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteHistoryExtension
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualAbsoluteNextEventTime
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualOrderedPrefix
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualFiniteCountPath
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathDensity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedPathExpansion
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseReversalVolume
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualEndpointTimeReversal
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedGibbsSurvival
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedStateReversal
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedPathReversal
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPrescribedWeightedDensity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualWeightedSector
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPhaseNormalization
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualNormalizedEndpointSector
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualCountableEndpointLaw
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualBoundedGibbsDuality
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2Expectation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualL2FlipDuality
import AutoSamplingTheory.ExampleCases.ProximalBPS.ActualPositionL2Averaging
import AutoSamplingTheory.ExampleCases.ProximalBPS.SharpCorrectorEnergy
import AutoSamplingTheory.ExampleCases.ProximalBPS.RoughMeanGradient
import AutoSamplingTheory.ExampleCases.SampleWiki
import AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflection
import AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentation
import AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentation
import AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScore
import AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRepresentative
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomain
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochner
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradient
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientKernel
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreClosedDomain
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCenteredResolventLimit
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolvent
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalC1Resolvent
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalOrdinaryResolvent
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedResolvent
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalLocalizedSobolev
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactSmoothGraph
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalCompactCoercivity
import AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGlobalCoercivity
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveCondition
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosure
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOCalculus
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVariance
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepth
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepth
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.Truncation
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianMixture
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransport
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKL
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackward
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGO
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveCenterRGO
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLError
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGO
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgram
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepth
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLError
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudget
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOError
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejection
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTail
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianArcLaw
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClipping
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMean
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentification
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponential
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparison
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalSamplerAccuracyCost
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalReferenceGradientDescent
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateInitialGradientMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.JointReferenceGradientDescent
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.NormalizedReferenceCall
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernel
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingCost
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalFORSKernel
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecution
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernel
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedKLOneStep
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKL
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimator
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalEstimatorLipschitz
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateProximalExecution
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalExpectedWork
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardCenterMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PartialMomentumRefresh
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PicardInputLaw
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseKernel
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RealizedProximalWork
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ImplementedPhaseWork
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.CountedPhaseProgram
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SourceQuadratureWork
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalPhaseStability
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseAccuracyWork
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.KineticDissipation
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FirstOrderDifference
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualContraction
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualIncrement
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ActualKernelTransport
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedGibbsPotential
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedScorePosterior
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothedHessianUpper
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseStateMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseMetric
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PhaseReferenceMoment
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialPhaseTransport
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransport
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.InitialGibbsPhaseTransportUnconditional
import AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgram

/-!
# ASTIS example cases

This namespace is the public Lean entry point for externally sourced worked
examples that ASTIS turns into source-pinned theorem targets and then absorbs
into the reusable sampling-theory dependency graph.
-/