production module

`AutoSamplingTheory.TechnicalLemmas.SALDExtracted`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/SALDExtracted.lean.

Imports

AutoSamplingTheory.SALD

Imported by

AutoSamplingTheory

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

AutoSamplingTheory/TechnicalLemmas/SALDExtracted.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.SALD

/-!
# SALD-extracted technical lemma memory

This module exposes reusable proof blocks that were first formalized inside
the faithful SALD reproduction.  They remain mathematically tied to SALD's
proof route, but agents can now find them under `TechnicalLemmas` instead of
searching the whole SALD file.
-/

namespace AutoSamplingTheory
namespace TechnicalLemmas
namespace SALDExtracted

export SALD (
  gronwallNegIntegralRewriteScalar
  gronwallExpProductRewriteScalar
  gronwallIntervalIntegralAdditivityScalar
  gronwallExpProductRewriteIntervalIntegral
  gronwallExpProductRewriteIntegralCongr
  gronwallIntegratingFactorProductDerivative
  gronwallIntegratingFactorDerivativeInequalityScalar
  gronwallEndpointMultiplyByExpNegScalar
  forwardKlDvPositiveAlphaScalingScalar
  forwardKlDvPositiveAlphaCoefficientScalar
  forwardKlPostDvGronwallCoefficientScalar
  discreteForwardKlAlphaComplexityCollectionScalar
  discreteForwardKlDeltaAccumulationScalar
  discreteForwardKlAccumulatedErrorCollectionScalar
  discreteForwardKlEmInterpolationLeftEndpointVector
  discreteForwardKlEmInterpolationRightEndpointVector
  discreteForwardKlLawEqOfPointwise
  discreteForwardKlEmInterpolationLeftEndpointLawHandoff
  discreteForwardKlEmInterpolationRightEndpointLawHandoff
  discreteForwardKlEmEndpointLawPairHandoff
  selectedWeakTestNormalizedCoordinateLawOfStdGaussianVectorLaw
  selectedWeakTestNormalizedVarianceDefOfGaussianRealUnitLaw
  selectedWeakTestRemainderMeasOfStdGaussianVectorLaw
  selectedWeakTestRemainderBoundOfStdGaussianVectorLaw
  selectedWeakTestRemainderBoundIntegrableOfStdGaussianVectorLaw
  selectedWeakTestNormalizedRemainderBoundIntOfQuadraticBound
  selectedWeakTestQuadraticCoeffDefOfSecondTaylorCoeffDef
  selectedWeakTestVarianceOneOfNormalizedBrownianVarianceDef
  selectedWeakTestQuadraticVariationNormalizationOfCoeffDefAndVarianceOne
  selectedWeakTestHessianOpNormOfSourceHessianField
)

end SALDExtracted
end TechnicalLemmas
end AutoSamplingTheory