production module
`AutoSamplingTheory.TechnicalLemmas.StochasticProcesses`

0 named declarations scanned from AutoSamplingTheory/TechnicalLemmas/StochasticProcesses.lean.
Imports
Imported by
AutoSamplingTheory.TechnicalLemmasAutoSamplingTheory.TechnicalLemmas.Registry
Placeholder scan
0 declaration(s) flagged
Gate status
Partial
Declarations

This aggregator contains no named declarations.
Complete Lean source

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses.lean — full module with imports and context
Download module (.lean)
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariation
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.VectorBrownianFiltration
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EuclideanBrownianCoordinates
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChamp
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BakryEmeryCalculus
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BakryEmeryGradientContraction
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CoefficientTruncation
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryRefinement
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryStopping
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGridStoppingIto
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicHorizonExtension
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicHorizonIto
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DiscreteDoobL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ContinuousDoobL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegral
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoAlgebra
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoEmbedding
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoDoobL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoProcess
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryStoppingTime
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroup
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalNormBridge
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcess
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveDriftIntegral
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessProgressive
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcessProgressive
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcess
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcessProgressive
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDisplay1_1_18
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoFormulaAlgebra
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteTimeGrid
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FokkerPlanckAlgebra
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Girsanov
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoTerminalCompletion
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcess
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessAfterHorizon
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessCongruence
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoHorizonConsistency
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoHorizonProcessConsistency
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Langevin
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCarreDuChamp
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCanonicalFisherGamma
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGenerator
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicApproximation
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicConvergence
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Density
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingDyadicApprox
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingBoundary
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProcessApprox
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingIntegrandLimit
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2Convergence
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingItoTerminal
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2Contraction
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Stopping
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingGraphNull
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingGeneralIto
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BoundedStoppedItoMean
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProcessConsistency
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalCanonicalLocalizer
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalCanonicalLocalizerLimit
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedL2Overlap
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedItoMartingale
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessGluing
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Localization
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroup
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovMeasureEvolution
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGenerator
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomain
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Algebra
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2HorizonExtension
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Reversibility
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.SampledElementaryApproximation
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasureRealBridge
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGenerator
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.AccumulatedEnergy
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LocalProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyPathContinuity
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedEnergy
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyLocalizer
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTime
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalization
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalizationL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrand
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedIntegrand
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppingBoundaryBridge
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedProgressiveL2
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppingL2Bridge
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheorem
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegral
import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedItoOverlap

/-!
# Stochastic-process technical lemma arsenal

Parent import surface for Markov and Feller semigroups, strong-continuity and
operator-generator domains, weak generators, weak Fokker--Planck, and
Euler--Maruyama/SDE reusable leaves.
-/