production module

`AutoSamplingTheory.TechnicalLemmas`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas.lean.

Imports

Imported by

AutoSamplingTheory

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.Analysis
import AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexity
import AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularization
import AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrability
import AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMoment
import AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMean
import AutoSamplingTheory.TechnicalLemmas.Analysis.HilbertCorrectorBound
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.TwoPointEntropy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.BernoulliLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactEntropy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianFlipEnergy
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactProductLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianCompactHilbertLogSobolev
import AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GaussianLogSobolev
import AutoSamplingTheory.TechnicalLemmas.Gaussian
import AutoSamplingTheory.TechnicalLemmas.Geometry
import AutoSamplingTheory.TechnicalLemmas.InformationTheory
import AutoSamplingTheory.TechnicalLemmas.InformationTheory.ProductEntropy
import AutoSamplingTheory.TechnicalLemmas.Measure
import AutoSamplingTheory.TechnicalLemmas.Measure.L2PullbackRange
import AutoSamplingTheory.TechnicalLemmas.Measure.L2RealComplexOperator
import AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRoot
import AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareRootUnique
import AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareOrder
import AutoSamplingTheory.TechnicalLemmas.Measure.L2RealSquareCommute
import AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationP2ConstantSpeed
import AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensity
import AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSqrtDensityDomain
import AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCost
import AutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihood
import AutoSamplingTheory.TechnicalLemmas.Measure.GaussianReflectedMean
import AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspective
import AutoSamplingTheory.TechnicalLemmas.Probability
import AutoSamplingTheory.TechnicalLemmas.Probability.BalancedRademacherCLT
import AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions
import AutoSamplingTheory.TechnicalLemmas.Registry
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
import AutoSamplingTheory.TechnicalLemmas.Taylor
import AutoSamplingTheory.TechnicalLemmas.Variational

/-!
# ASTIS reusable technical lemma arsenal

This parent module is the public import surface for ASTIS-owned reusable
SDE/Sampling technical lemmas that are candidates for Mathlib-style cleanup.

It deliberately excludes `AutoSamplingTheory.TechnicalLemmas.SALDExtracted`.
Those declarations compile and are searchable, but they are paper-extracted
bridges that should be generalized before being treated as Mathlib-ready
technical lemmas.
-/