Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
Two status layers

Sampling/SDE Implementation Map

The declaration inventory answers “what Lean accepts locally?” The milestone ledger answers “how much of the mathematical textbook route is reproduced?” A compiled helper never promotes an incomplete chapter theorem.

Status vocabulary

CompiledPartialStated/incomplete PlannedBlockedExternal/upstream dependency

Mathematical route and local evidence

MilestoneLocal evidenceRoute statusBoundaryEvidence declarationsBlockers
Log-concavity and normalized Gibbs measuresChapter 1 Compiled Partial The repository has local definitions and reusable leaves for positive log-concavity, Gibbs densities, finite nonzero normalization, and selected convex-potential consequences. 4 2
Langevin generator and finite-dimensional weighted-divergence displayChapter 1 Compiled Partial Coordinate, basis, gradient, Laplacian, and weighted-divergence identities compile locally. They establish the formal differential expression, not the operator domain or invariant law. 3 1
Whole-space weighted integration by parts and Gibbs invarianceChapter 1 Partial Partial Whole-space weighted IBP, an explicit C_c^2 generator-core contract, normalized-Gibbs annihilation on that core, and an abstract semigroup/domain-to-invariance bridge compile locally. The actual Langevin semigroup does not preserve compact support, so the concrete domain extension or a uniqueness route remains open. 9 1
Poincare, log-Sobolev, transport, and dissipationChapter 2 Partial Partial Scalar KL/Fisher/Dirichlet algebra and selected log-Sobolev handoffs compile, while the analytic inequality packages and preservation hierarchy remain incomplete. 1 2
Probability kernels and conditional expectation representativesChapter 3 Compiled Partial ASTIS has exact almost-everywhere bridges between Mathlib conditional distributions, conditional-expectation kernels, mapped kernels, and selected Bochner-integral fields. 2 2
Girsanov, Doob transforms, and path-space change of measureChapter 3 Compiled Partial Finite-dimensional Gaussian cylinder likelihood and measure identities compile and provide a base case. The continuous Brownian path-space theorem has not been packaged. 1 2
Continuous Langevin process to discrete sampling algorithmsChapter 4 Stated/incomplete Planned SDE and sampler contract records exist, but full LMC interpolation, convergence, stability, and error theorems are not local compiled theorem packages. 3 2
Accelerated, high-accuracy, proximal, structured, and generative-model routesChapter 5 Planned Planned Chapters 5-12 are mapped as downstream consumers of shared measure, functional-inequality, stochastic-process, and discretization roots. 0 3
External Lean and textbook dependenciesChapter shared External/upstream dependency Partial Mathlib, cited textbooks, papers, and audited Lean repositories are proof sources and port references. They are never represented as ASTIS-local certificates until an owned declaration compiles. 0 1

Major theorem dependencies

flowchart TD
  LC["LogConcaveOn"]:::compiled
  GibbsDensity["gibbsDensityENNReal"]:::compiled
  Normalize["isProbabilityMeasure_withDensity_normalized_gibbs"]:::compiled
  GibbsLC["logConcaveOn_normalized_gibbsDensity..."]:::compiled
  Generator["finiteEuclidean_langevinGenerator_coordinateDisplay"]:::compiled
  Cutoff["radialSmoothCutoff_tendsto_one"]:::compiled
  FiniteIBP["finite-box divergence + cutoff limits"]:::compiled
  Tails["concrete Gibbs tails / integrability"]:::compiled
  WholeIBP["whole-space weighted integration by parts"]:::compiled
  CoreInvariant["C_c² core annihilation + conditional invariance"]:::compiled
  Semigroup["concrete Langevin semigroup"]:::blocked
  Domains["semigroup-stable domain extension"]:::blocked
  Invariant["Gibbs invariant law"]:::blocked
  PI["Poincare typed interface"]:::compiled
  BE["Bakry--Emery PI criterion"]:::blocked
  Loc["localization theorem"]:::blocked
  Iso["sharp log-concave isoperimetry"]:::blocked
  FI["LSI / transport theorem packages"]:::partial
  Mixing["continuous-time mixing"]:::planned
  LMC["LMC discretization and rate"]:::planned

  GibbsDensity --> Normalize
  LC --> GibbsLC
  GibbsDensity --> GibbsLC
  Generator --> FiniteIBP
  Cutoff --> FiniteIBP
  FiniteIBP --> WholeIBP
  Tails --> WholeIBP
  WholeIBP --> CoreInvariant
  CoreInvariant --> Semigroup
  Semigroup --> Domains
  Domains --> Invariant
  Normalize --> Invariant
  PI --> BE
  PI --> Loc --> Iso
  Semigroup --> BE
  BE --> FI
  Iso --> FI
  Invariant --> Mixing
  FI --> Mixing
  Mixing --> LMC

  classDef compiled fill:#dcecff,stroke:#155eef,color:#172033,stroke-width:2px;
  classDef partial fill:#fff2c7,stroke:#9a6700,color:#172033,stroke-width:1.5px;
  classDef blocked fill:#ffe5e5,stroke:#c92a2a,color:#172033,stroke-width:2px;
  classDef planned fill:#eef3f9,stroke:#627086,color:#172033,stroke-width:1.5px;
A theorem DAG using declarations and open boundaries that exist in the current ASTIS route.

Complete module inventory

ModuleRoleImportsDeclarationsCompiledIncomplete
AutoSamplingTheoryAutoSamplingTheory.lean root aggregator110 00
AutoSamplingTheory.AutomationAutoSamplingTheory/Automation.lean production120 00
AutoSamplingTheory.CoreAutoSamplingTheory/Core.lean production110 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalBochnerAutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalBochner.lean production21 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalGradientAutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalGradient.lean production21 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalResolventAutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalResolvent.lean production21 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreAutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalScore.lean production91 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ConditionalScoreDomainAutoSamplingTheory/ExampleCases/ProximalBPS/ConditionalScoreDomain.lean production81 00
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianAugmentationAutoSamplingTheory/ExampleCases/ProximalBPS/GaussianAugmentation.lean production21 00
AutoSamplingTheory.ExampleCases.ProximalBPS.GaussianReflectionAutoSamplingTheory/ExampleCases/ProximalBPS/GaussianReflection.lean production41 00
AutoSamplingTheory.ExampleCases.ProximalBPS.GibbsAugmentationAutoSamplingTheory/ExampleCases/ProximalBPS/GibbsAugmentation.lean production41 00
AutoSamplingTheory.ExampleCases.ProximalBPS.MacroscopicRepresentativeAutoSamplingTheory/ExampleCases/ProximalBPS/MacroscopicRepresentative.lean production41 00
AutoSamplingTheory.ExampleCases.ProximalBPS.ReflectionL2AutoSamplingTheory/ExampleCases/ProximalBPS/ReflectionL2.lean production61 00
AutoSamplingTheory.ExampleCases.SampleWiki.Cases.IdealProximalChainAutoSamplingTheory/ExampleCases/SampleWiki/Cases/IdealProximalChain.lean production21 00
AutoSamplingTheory.ExampleCases.SampleWikiAutoSamplingTheory/ExampleCases/SampleWiki.lean production16 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveCenterRGOAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/AdaptiveCenterRGO.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.AdaptiveKLErrorAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/AdaptiveKLError.lean production51 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ApproximateInitialGradientMomentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ApproximateInitialGradientMoment.lean production68 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedGradientProgramAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ClippedGradientProgram.lean production314 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedMeanExponentialAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ClippedMeanExponential.lean production610 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ClippedRenyiComparisonAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ClippedRenyiComparison.lean production616 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedFiniteOutputKLAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedFiniteOutputKL.lean production313 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedKLOneStepAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedKLOneStep.lean production68 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.EnhancedTerminalExecutionAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/EnhancedTerminalExecution.lean production413 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOKLErrorAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/FiniteRGOKLError.lean production51 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.FiniteRGOProgramAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/FiniteRGOProgram.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianArcLawAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianArcLaw.lean production28 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianKLAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianKL.lean production41 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianMixtureAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianMixture.lean production31 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianPowerMomentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianPowerMoment.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GaussianRGOErrorBudgetAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GaussianRGOErrorBudget.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GibbsPositionMomentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GibbsPositionMoment.lean production33 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.GradientArcMeanAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/GradientArcMean.lean production510 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.IdealRGOIdentificationAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/IdealRGOIdentification.lean production611 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.JointReferenceGradientDescentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/JointReferenceGradientDescent.lean production36 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.LogarithmicDepthAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/LogarithmicDepth.lean production31 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.NormalizedReferenceCallAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/NormalizedReferenceCall.lean production38 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ObservationConditionalKernelAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ObservationConditionalKernel.lean production45 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonQueryTailAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/PoissonQueryTail.lean production127 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.PoissonRejectionAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/PoissonRejection.lean production736 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalEstimatorLipschitzAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ProximalEstimatorLipschitz.lean production12 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProximalGaussianEstimatorAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ProximalGaussianEstimator.lean production75 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ProxyReverseTransportAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ProxyReverseTransport.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOBackwardAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RGOBackward.lean production31 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOCalculusAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RGOCalculus.lean production31 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RGOClosureAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RGOClosure.lean production71 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveConditionAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveCondition.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveDepthAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveDepth.lean production31 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.RecursiveVarianceAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/RecursiveVariance.lean production41 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingCostAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ReferenceCarryingCost.lean production45 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.ReferenceCarryingKernelAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/ReferenceCarryingKernel.lean production37 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcClippingAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/SmoothGradientArcClipping.lean production27 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.SmoothGradientArcMomentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/SmoothGradientArcMoment.lean production521 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StateDependentRGOAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StateDependentRGO.lean production11 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedGaussianRGOErrorAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StoppedGaussianRGOError.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.StoppedRGODepthAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/StoppedRGODepth.lean production21 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalFORSKernelAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/TerminalFORSKernel.lean production428 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalReferenceGradientDescentAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/TerminalReferenceGradientDescent.lean production78 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TerminalSamplerAccuracyCostAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/TerminalSamplerAccuracyCost.lean production315 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TruncationAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/Truncation.lean production51 00
AutoSamplingTheory.ExampleCases.SmoothedPicardHMC.TwoNoiseRGOAutoSamplingTheory/ExampleCases/SmoothedPicardHMC/TwoNoiseRGO.lean production21 00
AutoSamplingTheory.ExampleCasesAutoSamplingTheory/ExampleCases.lean production570 00
AutoSamplingTheory.LiteratureAutoSamplingTheory/Literature.lean production15 00
AutoSamplingTheory.OpenProblemsAutoSamplingTheory/OpenProblems.lean production13 00
AutoSamplingTheory.ProbabilityAutoSamplingTheory/Probability.lean production1154 00
AutoSamplingTheory.RMFLDAutoSamplingTheory/RMFLD.lean production15 00
AutoSamplingTheory.SALDAutoSamplingTheory/SALD.lean production131575 00
AutoSamplingTheory.SDEAutoSamplingTheory/SDE.lean production14 00
AutoSamplingTheory.TechnicalLemmas.Algebra.LinearGrowthOfStepAutoSamplingTheory/TechnicalLemmas/Algebra/LinearGrowthOfStep.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Algebra.ReciprocalGrowthRateAutoSamplingTheory/TechnicalLemmas/Algebra/ReciprocalGrowthRate.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Analysis.BoundedQuadraticCostIntegrabilityAutoSamplingTheory/TechnicalLemmas/Analysis/BoundedQuadraticCostIntegrability.lean production43 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.CutoffAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Cutoff.lean production325 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.DivergenceAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Divergence.lean production659 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Gradient.lean production410 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.GradientAlgebraAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/GradientAlgebra.lean production58 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LaplacianAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Laplacian.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.LineDerivAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/LineDeriv.lean production49 00
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.TaylorAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus/Taylor.lean production10 00
AutoSamplingTheory.TechnicalLemmas.Analysis.CalculusAutoSamplingTheory/TechnicalLemmas/Analysis/Calculus.lean production70 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexAEDifferentiableAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexAEDifferentiable.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexDomainACAEDifferentiableAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexDomainACAEDifferentiable.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexGradientGapSharpnessAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexGradientGapSharpness.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexLocalSubgradientAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexLocalSubgradient.lean production14 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexOpenAEDifferentiableAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexOpenAEDifferentiable.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSmoothGradientAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSmoothGradient.lean production53 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexSubgradientAutoSamplingTheory/TechnicalLemmas/Analysis/ConvexSubgradient.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC1AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexityC1.lean production73 00
AutoSamplingTheory.TechnicalLemmas.Analysis.ConvexityC2AutoSamplingTheory/TechnicalLemmas/Analysis/ConvexityC2.lean production33 00
AutoSamplingTheory.TechnicalLemmas.Analysis.CycleSuccessorDistinctAutoSamplingTheory/TechnicalLemmas/Analysis/CycleSuccessorDistinct.lean production12 00
AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicCostExpectationAutoSamplingTheory/TechnicalLemmas/Analysis/CyclicCostExpectation.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.CyclicQuadraticCostAutoSamplingTheory/TechnicalLemmas/Analysis/CyclicQuadraticCost.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Analysis.DiagonalProductCostIntegralAutoSamplingTheory/TechnicalLemmas/Analysis/DiagonalProductCostIntegral.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GibbsGradientMomentAutoSamplingTheory/TechnicalLemmas/Analysis/GibbsGradientMoment.lean production65 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentBasicAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentBasic.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentComplexityAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentComplexity.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentContractionAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentContraction.lean production42 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentOptimalStepAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentOptimalStep.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentPLAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentPL.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentRatesAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentRates.lean production12 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentSharpnessAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentSharpness.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentStationarityAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentStationarity.lean production42 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientDescentValueAutoSamplingTheory/TechnicalLemmas/Analysis/GradientDescentValue.lean production52 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowContractionAutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowContraction.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowLastIterateAutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowLastIterate.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowPLAutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowPL.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowStationarityAutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowStationarity.lean production41 00
AutoSamplingTheory.TechnicalLemmas.Analysis.GradientFlowValueAutoSamplingTheory/TechnicalLemmas/Analysis/GradientFlowValue.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.HessianStrongConvexityAutoSamplingTheory/TechnicalLemmas/Analysis/HessianStrongConvexity.lean production61 00
AutoSamplingTheory.TechnicalLemmas.Analysis.IntegrabilityAutoSamplingTheory/TechnicalLemmas/Analysis/Integrability.lean production424 00
AutoSamplingTheory.TechnicalLemmas.Analysis.LeftLebesgueAverageAutoSamplingTheory/TechnicalLemmas/Analysis/LeftLebesgueAverage.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Analysis.MeasurableGradientAutoSamplingTheory/TechnicalLemmas/Analysis/MeasurableGradient.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingClosedChainAutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChain.lean production37 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingClosedChainMonotonicityAutoSamplingTheory/TechnicalLemmas/Analysis/PairingClosedChainMonotonicity.lean production67 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleNeighborhoodAutoSamplingTheory/TechnicalLemmas/Analysis/PairingCycleNeighborhood.lean production53 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCycleQuantitativeNeighborhoodAutoSamplingTheory/TechnicalLemmas/Analysis/PairingCycleQuantitativeNeighborhood.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingCyclicMonotonicityAutoSamplingTheory/TechnicalLemmas/Analysis/PairingCyclicMonotonicity.lean production29 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarConvexDomainAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarConvexDomain.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarPotentialAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarPotential.lean production313 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarRealDomainAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarRealDomain.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarRealSupportAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarRealSupport.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSubgradientAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarSubgradient.lean production29 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PairingRockafellarSupportGradientAutoSamplingTheory/TechnicalLemmas/Analysis/PairingRockafellarSupportGradient.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PermutedProductCostIntegralAutoSamplingTheory/TechnicalLemmas/Analysis/PermutedProductCostIntegral.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PermutedQuadraticCostAutoSamplingTheory/TechnicalLemmas/Analysis/PermutedQuadraticCost.lean production26 00
AutoSamplingTheory.TechnicalLemmas.Analysis.PrefixIntegralAutoSamplingTheory/TechnicalLemmas/Analysis/PrefixIntegral.lean production28 00
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticGradientDescentAutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticGradientDescent.lean production52 00
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationAutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticRegularization.lean production51 00
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationFirstOrderAutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticRegularizationFirstOrder.lean production51 00
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationOracleAutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticRegularizationOracle.lean production12 00
AutoSamplingTheory.TechnicalLemmas.Analysis.QuadraticRegularizationTransferAutoSamplingTheory/TechnicalLemmas/Analysis/QuadraticRegularizationTransfer.lean production61 00
AutoSamplingTheory.TechnicalLemmas.Analysis.RestartLogComplexityAutoSamplingTheory/TechnicalLemmas/Analysis/RestartLogComplexity.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.RestartReductionAutoSamplingTheory/TechnicalLemmas/Analysis/RestartReduction.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.SmoothnessEquivalencesAutoSamplingTheory/TechnicalLemmas/Analysis/SmoothnessEquivalences.lean production12 00
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexFirstOrderAutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexFirstOrder.lean production42 00
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGibbsIntegrabilityAutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexGibbsIntegrability.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexGradientConverseAutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexGradientConverse.lean production71 00
AutoSamplingTheory.TechnicalLemmas.Analysis.StrongConvexPLPullbackAutoSamplingTheory/TechnicalLemmas/Analysis/StrongConvexPLPullback.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Analysis.UniformRegularizationAutoSamplingTheory/TechnicalLemmas/Analysis/UniformRegularization.lean production41 00
AutoSamplingTheory.TechnicalLemmas.AnalysisAutoSamplingTheory/TechnicalLemmas/Analysis.lean production410 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.ClosedGraphResolventAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/ClosedGraphResolvent.lean production31 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.GeneratorAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Generator.lean production17 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.LogSobolevAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/LogSobolev.lean production10 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.PoincareAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/Poincare.lean production29 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.SemigroupDecayAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/SemigroupDecay.lean production217 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedBochnerAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedBochner.lean production31 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedGradient.lean production71 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientDistributionAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedGradientDistribution.lean production22 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedGradientWeakAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedGradientWeak.lean production12 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedLocalL2AutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedLocalL2.lean production41 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalities.WeightedResolventAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities/WeightedResolvent.lean production21 00
AutoSamplingTheory.TechnicalLemmas.FunctionalInequalitiesAutoSamplingTheory/TechnicalLemmas/FunctionalInequalities.lean production110 00
AutoSamplingTheory.TechnicalLemmas.GaussianAutoSamplingTheory/TechnicalLemmas/Gaussian.lean production730 00
AutoSamplingTheory.TechnicalLemmas.Geometry.EuclideanSpaceCoordinatesAutoSamplingTheory/TechnicalLemmas/Geometry/EuclideanSpaceCoordinates.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Geometry.GeodesicConvexityAutoSamplingTheory/TechnicalLemmas/Geometry/GeodesicConvexity.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Geometry.LogConcavityAutoSamplingTheory/TechnicalLemmas/Geometry/LogConcavity.lean production540 00
AutoSamplingTheory.TechnicalLemmas.Geometry.MetricCurveAutoSamplingTheory/TechnicalLemmas/Geometry/MetricCurve.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Geometry.StrongConvexityAutoSamplingTheory/TechnicalLemmas/Geometry/StrongConvexity.lean production24 00
AutoSamplingTheory.TechnicalLemmas.GeometryAutoSamplingTheory/TechnicalLemmas/Geometry.lean production50 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalDirichletFisherAutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalDirichletFisher.lean production36 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalFisherTransportPairingAutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalFisherTransportPairing.lean production53 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalKLDissipationAutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalKLDissipation.lean production35 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.CanonicalRelativeFisherAutoSamplingTheory/TechnicalLemmas/InformationTheory/CanonicalRelativeFisher.lean production310 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.DonskerVaradhanAutoSamplingTheory/TechnicalLemmas/InformationTheory/DonskerVaradhan.lean production10 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.FisherTransportAutoSamplingTheory/TechnicalLemmas/InformationTheory/FisherTransport.lean production13 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.GeodesicFisherTransportAutoSamplingTheory/TechnicalLemmas/InformationTheory/GeodesicFisherTransport.lean production33 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.KLDensityAutoSamplingTheory/TechnicalLemmas/InformationTheory/KLDensity.lean production32 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RNLogRatioAutoSamplingTheory/TechnicalLemmas/InformationTheory/RNLogRatio.lean production411 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RelativeFisherAutoSamplingTheory/TechnicalLemmas/InformationTheory/RelativeFisher.lean production47 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.RenyiAutoSamplingTheory/TechnicalLemmas/InformationTheory/Renyi.lean production38 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceAutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergence.lean production42 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceGradientAutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergenceGradient.lean production32 00
AutoSamplingTheory.TechnicalLemmas.InformationTheory.SimultaneousFDivergenceIntegralAutoSamplingTheory/TechnicalLemmas/InformationTheory/SimultaneousFDivergenceIntegral.lean production32 00
AutoSamplingTheory.TechnicalLemmas.InformationTheoryAutoSamplingTheory/TechnicalLemmas/InformationTheory.lean production130 00
AutoSamplingTheory.TechnicalLemmas.Measure.CanonicalGlobalCompetitorAutoSamplingTheory/TechnicalLemmas/Measure/CanonicalGlobalCompetitor.lean production44 00
AutoSamplingTheory.TechnicalLemmas.Measure.ChewiTheorem1_3_23AutoSamplingTheory/TechnicalLemmas/Measure/ChewiTheorem1_3_23.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassAutoSamplingTheory/TechnicalLemmas/Measure/CommonMass.lean production16 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassNormalizedProductAutoSamplingTheory/TechnicalLemmas/Measure/CommonMassNormalizedProduct.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassProductMapAutoSamplingTheory/TechnicalLemmas/Measure/CommonMassProductMap.lean production12 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceAutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSlice.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonMassSliceFamilyAutoSamplingTheory/TechnicalLemmas/Measure/CommonMassSliceFamily.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonNoiseContractionAutoSamplingTheory/TechnicalLemmas/Measure/CommonNoiseContraction.lean production415 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonRemovableMassAutoSamplingTheory/TechnicalLemmas/Measure/CommonRemovableMass.lean production24 00
AutoSamplingTheory.TechnicalLemmas.Measure.CommonSlicePermutationReplacementAutoSamplingTheory/TechnicalLemmas/Measure/CommonSlicePermutationReplacement.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Measure.ContinuousCostWeakLowerSemicontinuityAutoSamplingTheory/TechnicalLemmas/Measure/ContinuousCostWeakLowerSemicontinuity.lean production49 00
AutoSamplingTheory.TechnicalLemmas.Measure.ConvexInteriorAEAutoSamplingTheory/TechnicalLemmas/Measure/ConvexInteriorAE.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Measure.CouplingAEMarginalsAutoSamplingTheory/TechnicalLemmas/Measure/CouplingAEMarginals.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Measure.CouplingConvexDomainAEAutoSamplingTheory/TechnicalLemmas/Measure/CouplingConvexDomainAE.lean production41 00
AutoSamplingTheory.TechnicalLemmas.Measure.CouplingGraphAutoSamplingTheory/TechnicalLemmas/Measure/CouplingGraph.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.CouplingGraphIdentityAutoSamplingTheory/TechnicalLemmas/Measure/CouplingGraphIdentity.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.CouplingQuadraticIntegrabilityAutoSamplingTheory/TechnicalLemmas/Measure/CouplingQuadraticIntegrability.lean production35 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementChangeOfVariablesAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementChangeOfVariables.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexGradientPositiveAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexGradientPositive.lean production43 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementConvexPotentialSupportAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementConvexPotentialSupport.lean production43 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeDetPosAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeDetPos.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeLogDetAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeLogDet.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementDerivativeMatrixAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementDerivativeMatrix.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementEntropyPushforwardAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementEntropyPushforward.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementGradientDerivativeSymmetryAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementGradientDerivativeSymmetry.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolation.lean production17 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationConstantSpeedAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationConstantSpeed.lean production44 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCostAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCost.lean production45 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationCouplingAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationCoupling.lean production15 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementInterpolationP2ConstantSpeedAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementInterpolationP2ConstantSpeed.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianAffineSpectrumAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianAffineSpectrum.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianEntropyAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianEntropy.lean production514 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementJacobianMatrixLogDetAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementJacobianMatrixLogDet.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapDerivativeAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapDerivative.lean production14 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMapInjectivityAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMapInjectivity.lean production34 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementMonotoneDerivativeAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementMonotoneDerivative.lean production62 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementPositiveOperatorAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPositiveOperator.lean production24 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementPotentialEnergyAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementPotentialEnergy.lean production44 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementRealQuadraticCostAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementRealQuadraticCost.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.DisplacementSupportingPotentialAutoSamplingTheory/TechnicalLemmas/Measure/DisplacementSupportingPotential.lean production13 00
AutoSamplingTheory.TechnicalLemmas.Measure.FiniteRemainderAutoSamplingTheory/TechnicalLemmas/Measure/FiniteRemainder.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Measure.FiniteSumDominationAutoSamplingTheory/TechnicalLemmas/Measure/FiniteSumDomination.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.GaussianLikelihoodAutoSamplingTheory/TechnicalLemmas/Measure/GaussianLikelihood.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.GaussianSmoothingAutoSamplingTheory/TechnicalLemmas/Measure/GaussianSmoothing.lean production27 00
AutoSamplingTheory.TechnicalLemmas.Measure.GibbsAutoSamplingTheory/TechnicalLemmas/Measure/Gibbs.lean production215 00
AutoSamplingTheory.TechnicalLemmas.Measure.GibbsIntegralAutoSamplingTheory/TechnicalLemmas/Measure/GibbsIntegral.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.GibbsLogConcavityAutoSamplingTheory/TechnicalLemmas/Measure/GibbsLogConcavity.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Measure.IsotropicGaussianDensityAutoSamplingTheory/TechnicalLemmas/Measure/IsotropicGaussianDensity.lean production41 00
AutoSamplingTheory.TechnicalLemmas.Measure.KantorovichDualAutoSamplingTheory/TechnicalLemmas/Measure/KantorovichDual.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Measure.L2ExpectationAutoSamplingTheory/TechnicalLemmas/Measure/L2Expectation.lean production35 00
AutoSamplingTheory.TechnicalLemmas.Measure.OptimalContinuousCostAutoSamplingTheory/TechnicalLemmas/Measure/OptimalContinuousCost.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Measure.PermutedMarginalReplacementAutoSamplingTheory/TechnicalLemmas/Measure/PermutedMarginalReplacement.lean production214 00
AutoSamplingTheory.TechnicalLemmas.Measure.PermutedReplacementQuadraticCostAutoSamplingTheory/TechnicalLemmas/Measure/PermutedReplacementQuadraticCost.lean production710 00
AutoSamplingTheory.TechnicalLemmas.Measure.PositiveComponentAEAutoSamplingTheory/TechnicalLemmas/Measure/PositiveComponentAE.lean production14 00
AutoSamplingTheory.TechnicalLemmas.Measure.PowerPerspectiveAutoSamplingTheory/TechnicalLemmas/Measure/PowerPerspective.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Measure.ProbabilityCouplingCompactnessAutoSamplingTheory/TechnicalLemmas/Measure/ProbabilityCouplingCompactness.lean production37 00
AutoSamplingTheory.TechnicalLemmas.Measure.ProductAutoSamplingTheory/TechnicalLemmas/Measure/Product.lean production25 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalBrenierMapAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalBrenierMap.lean production84 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMapAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMap.lean production17 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMapUniquenessAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMapUniqueness.lean production13 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalMidpointAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalMidpoint.lean production35 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalRealMinimalityAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalRealMinimality.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalSupportCyclicAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalSupportCyclic.lean production73 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuadraticOptimalUniquenessAutoSamplingTheory/TechnicalLemmas/Measure/QuadraticOptimalUniqueness.lean production52 00
AutoSamplingTheory.TechnicalLemmas.Measure.QuantitativeSupportLocalBlocksAutoSamplingTheory/TechnicalLemmas/Measure/QuantitativeSupportLocalBlocks.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Measure.RadonNikodymAutoSamplingTheory/TechnicalLemmas/Measure/RadonNikodym.lean production512 00
AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorAutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitor.lean production14 00
AutoSamplingTheory.TechnicalLemmas.Measure.ReplacementCompetitorQuadraticCostAutoSamplingTheory/TechnicalLemmas/Measure/ReplacementCompetitorQuadraticCost.lean production33 00
AutoSamplingTheory.TechnicalLemmas.Measure.StrictCycleCheaperLocalReplacementAutoSamplingTheory/TechnicalLemmas/Measure/StrictCycleCheaperLocalReplacement.lean production111 00
AutoSamplingTheory.TechnicalLemmas.Measure.SupportLocalBlocksAutoSamplingTheory/TechnicalLemmas/Measure/SupportLocalBlocks.lean production34 00
AutoSamplingTheory.TechnicalLemmas.Measure.TransportAutoSamplingTheory/TechnicalLemmas/Measure/Transport.lean production19 00
AutoSamplingTheory.TechnicalLemmas.Measure.TransportGluingAutoSamplingTheory/TechnicalLemmas/Measure/TransportGluing.lean production24 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinFiniteSecondMomentAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinFiniteSecondMoment.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSpaceAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSpace.lean production48 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinSymmetryAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinSymmetry.lean production36 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangle.lean production31 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleCoreAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleCore.lean production211 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleExactAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleExact.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Measure.WassersteinTriangleMarginalsAutoSamplingTheory/TechnicalLemmas/Measure/WassersteinTriangleMarginals.lean production414 00
AutoSamplingTheory.TechnicalLemmas.MeasureAutoSamplingTheory/TechnicalLemmas/Measure.lean production581 00
AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalKernelAutoSamplingTheory/TechnicalLemmas/Probability/ConditionalKernel.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Probability.ConditionalResamplingAutoSamplingTheory/TechnicalLemmas/Probability/ConditionalResampling.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBathAutoSamplingTheory/TechnicalLemmas/Probability/CoordinateHeatBath.lean production24 00
AutoSamplingTheory.TechnicalLemmas.Probability.CoordinateHeatBathConditionalAutoSamplingTheory/TechnicalLemmas/Probability/CoordinateHeatBathConditional.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductPairMarginalAutoSamplingTheory/TechnicalLemmas/Probability/FiniteProductPairMarginal.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Probability.FiniteProductSupportAutoSamplingTheory/TechnicalLemmas/Probability/FiniteProductSupport.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Probability.GaussianConditionalKernelAutoSamplingTheory/TechnicalLemmas/Probability/GaussianConditionalKernel.lean production61 00
AutoSamplingTheory.TechnicalLemmas.Probability.HeatBathAutoSamplingTheory/TechnicalLemmas/Probability/HeatBath.lean production24 00
AutoSamplingTheory.TechnicalLemmas.Probability.KernelInvarianceAutoSamplingTheory/TechnicalLemmas/Probability/KernelInvariance.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Probability.KernelMixtureAutoSamplingTheory/TechnicalLemmas/Probability/KernelMixture.lean production34 00
AutoSamplingTheory.TechnicalLemmas.Probability.KernelReversibilityAutoSamplingTheory/TechnicalLemmas/Probability/KernelReversibility.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Probability.KernelTotalVariationAutoSamplingTheory/TechnicalLemmas/Probability/KernelTotalVariation.lean production21 00
AutoSamplingTheory.TechnicalLemmas.Probability.KernelTransportAutoSamplingTheory/TechnicalLemmas/Probability/KernelTransport.lean production11 00
AutoSamplingTheory.TechnicalLemmas.Probability.LawMapAutoSamplingTheory/TechnicalLemmas/Probability/LawMap.lean production10 00
AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasureAutoSamplingTheory/TechnicalLemmas/Probability/NormalizedFiniteMeasure.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Probability.NormalizedFiniteMeasureIntegralAutoSamplingTheory/TechnicalLemmas/Probability/NormalizedFiniteMeasureIntegral.lean production32 00
AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBathAutoSamplingTheory/TechnicalLemmas/Probability/RandomScanHeatBath.lean production23 00
AutoSamplingTheory.TechnicalLemmas.Probability.RandomScanHeatBathReversibilityAutoSamplingTheory/TechnicalLemmas/Probability/RandomScanHeatBathReversibility.lean production22 00
AutoSamplingTheory.TechnicalLemmas.Probability.UniformExpectationGapAutoSamplingTheory/TechnicalLemmas/Probability/UniformExpectationGap.lean production32 00
AutoSamplingTheory.TechnicalLemmas.ProbabilityAutoSamplingTheory/TechnicalLemmas/Probability.lean production100 00
AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributions.GaussianAutoSamplingTheory/TechnicalLemmas/ProbabilityDistributions/Gaussian.lean production10 00
AutoSamplingTheory.TechnicalLemmas.ProbabilityDistributionsAutoSamplingTheory/TechnicalLemmas/ProbabilityDistributions.lean production10 00
AutoSamplingTheory.TechnicalLemmas.RegistryAutoSamplingTheory/TechnicalLemmas/Registry.lean production3218 00
AutoSamplingTheory.TechnicalLemmas.SALDExtractedAutoSamplingTheory/TechnicalLemmas/SALDExtracted.lean production10 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.AccumulatedEnergyAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/AccumulatedEnergy.lean production16 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianMotion.lean production710 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/BrownianQuadraticVariation.lean production211 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyLocalizerAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyLocalizer.lean production317 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalEnergyStoppingTimeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalEnergyStoppingTime.lean production23 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalLocalizationTheoremAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalLocalizationTheorem.lean production23 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalizationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalization.lean production310 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalRawLocalizationL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalRawLocalizationL2.lean production13 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CanonicalStoppedItoIntegralAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CanonicalStoppedItoIntegral.lean production26 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CarreDuChampAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CarreDuChamp.lean production68 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDefinition1_1_17.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDisplay1_1_18AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiDisplay1_1_18.lean production11 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcessAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcess.lean production39 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiItoProcessProgressiveAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiItoProcessProgressive.lean production31 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiProposition1_1_16AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ChewiProposition1_1_16.lean production13 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CoefficientTruncationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CoefficientTruncation.lean production214 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedEnergyAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CompletedEnergy.lean production111 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.CompletedIntegrandAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/CompletedIntegrand.lean production15 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ContinuousDoobL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ContinuousDoobL2.lean production219 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DiscreteDoobL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DiscreteDoobL2.lean production16 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DiscreteDoobLpPortAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DiscreteDoobLpPort.lean production022 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryRefinementAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryRefinement.lean production244 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicElementaryStoppingAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicElementaryStopping.lean production221 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizonAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGlobalHorizon.lean production213 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGridStoppingItoAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicGridStoppingIto.lean production23 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicHorizonExtensionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicHorizonExtension.lean production517 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicHorizonItoAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/DyadicHorizonIto.lean production16 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoAlgebraAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoAlgebra.lean production115 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoDoobL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoDoobL2.lean production512 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoEmbeddingAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoEmbedding.lean production210 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIntegralAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIntegral.lean production310 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometryAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoIsometry.lean production319 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoL2.lean production313 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoProcessAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryItoProcess.lean production213 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryStoppingTimeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ElementaryStoppingTime.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyPathContinuityAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyPathContinuity.lean production210 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedIntegrandAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyStoppedIntegrand.lean production26 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedItoOverlapAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyStoppedItoOverlap.lean production42 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppedProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyStoppedProgressiveL2.lean production27 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppingBoundaryBridgeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyStoppingBoundaryBridge.lean production22 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EnergyStoppingL2BridgeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EnergyStoppingL2Bridge.lean production54 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.EuclideanBrownianCoordinatesAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/EuclideanBrownianCoordinates.lean production411 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerGeneratorBridgeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerGeneratorBridge.lean production24 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FellerSemigroupAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FellerSemigroup.lean production616 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcessAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcess.lean production17 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalItoProcessProgressiveAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalItoProcessProgressive.lean production33 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteDimensionalNormBridgeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteDimensionalNormBridge.lean production311 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FiniteTimeGridAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FiniteTimeGrid.lean production211 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.FokkerPlanckAlgebraAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/FokkerPlanckAlgebra.lean production12 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GaussianFourthMomentAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GaussianFourthMoment.lean production21 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GeneratorStationarityAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GeneratorStationarity.lean production14 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GirsanovAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Girsanov.lean production15 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalCanonicalLocalizerAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalCanonicalLocalizer.lean production315 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalCanonicalLocalizerLimitAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalCanonicalLocalizerLimit.lean production23 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessGluingAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalItoProcessGluing.lean production218 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalItoProcessProgressiveAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalItoProcessProgressive.lean production11 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalLocalProgressiveL2.lean production14 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedItoMartingaleAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoMartingale.lean production59 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedItoOverlapAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedItoOverlap.lean production59 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedL2OverlapAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedL2Overlap.lean production34 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/GlobalStoppedProgressiveL2.lean production411 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoFormulaAlgebraAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoFormulaAlgebra.lean production412 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoHorizonConsistencyAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoHorizonConsistency.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoHorizonProcessConsistencyAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoHorizonProcessConsistency.lean production24 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcess.lean production778 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessAfterHorizonAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessAfterHorizon.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessCongruenceAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessCongruence.lean production22 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoIntegralProcessGlobalContinuityAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoIntegralProcessGlobalContinuity.lean production11 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ItoTerminalCompletionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ItoTerminalCompletion.lean production241 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.L2GeneratorIdentitiesAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/L2GeneratorIdentities.lean production32 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicApproximationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LaggedDyadicApproximation.lean production319 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicConvergenceAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LaggedDyadicConvergence.lean production610 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Langevin.lean production1032 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCanonicalFisherGammaAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LangevinCanonicalFisherGamma.lean production34 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinCarreDuChampAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LangevinCarreDuChamp.lean production44 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinGeneratorAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LangevinGenerator.lean production35 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LangevinKLDissipationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LangevinKLDissipation.lean production21 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LocalProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/LocalProgressiveL2.lean production28 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LocalizationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Localization.lean production64 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovMeasureEvolutionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovMeasureEvolution.lean production313 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MarkovSemigroupAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/MarkovSemigroup.lean production110 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.MartingaleAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Martingale.lean production12 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGenerator.lean production112 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.OperatorGeneratorDomainAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/OperatorGeneratorDomain.lean production219 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveDriftIntegralAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveDriftIntegral.lean production23 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2.lean production416 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2AlgebraAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Algebra.lean production121 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2DensityAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Density.lean production128 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2HorizonExtensionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2HorizonExtension.lean production19 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2StoppingAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean production17 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2TruncationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Truncation.lean production28 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingBoundaryAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingBoundary.lean production13 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingDyadicApproxAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingDyadicApprox.lean production16 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingGeneralItoAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingGeneralIto.lean production13 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingIntegrandLimitAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingIntegrandLimit.lean production21 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingItoTerminalAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingItoTerminal.lean production22 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2ContractionAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Contraction.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2ConvergenceAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Convergence.lean production24 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProcessApproxAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingProcessApprox.lean production25 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProcessConsistencyAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingProcessConsistency.lean production37 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingProgressiveL2AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingProgressiveL2.lean production27 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ReversibilityAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/Reversibility.lean production22 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ReversibleGeneratorAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ReversibleGenerator.lean production32 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.SampledElementaryApproximationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/SampledElementaryApproximation.lean production210 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StationarityEquivalenceAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StationarityEquivalence.lean production22 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingGraphNullAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingGraphNull.lean production26 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTimeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/StoppingTime.lean production16 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasureAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean production313 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasureRealBridgeAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasureRealBridge.lean production318 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.VectorBrownianFiltrationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/VectorBrownianFiltration.lean production33 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakForwardEquationAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakForwardEquation.lean production17 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.WeakGeneratorAutoSamplingTheory/TechnicalLemmas/StochasticProcesses/WeakGenerator.lean production24 00
AutoSamplingTheory.TechnicalLemmas.StochasticProcessesAutoSamplingTheory/TechnicalLemmas/StochasticProcesses.lean production1010 00
AutoSamplingTheory.TechnicalLemmas.TaylorAutoSamplingTheory/TechnicalLemmas/Taylor.lean production54 00
AutoSamplingTheory.TechnicalLemmas.VariationalAutoSamplingTheory/TechnicalLemmas/Variational.lean production30 00
AutoSamplingTheory.TechnicalLemmasAutoSamplingTheory/TechnicalLemmas.lean production210 00
TestsTests.lean test2020 00
Tests.AccumulatedEnergyTests/AccumulatedEnergy.lean test10 00
Tests.BasicTests/Basic.lean test20 00
Tests.BoundedQuadraticCostIntegrabilityTests/BoundedQuadraticCostIntegrability.lean test10 00
Tests.BrownianMotionTests/BrownianMotion.lean test10 00
Tests.BrownianQuadraticVariationTests/BrownianQuadraticVariation.lean test10 00
Tests.CanonicalDirichletFisherTests/CanonicalDirichletFisher.lean test10 00
Tests.CanonicalEnergyLocalizerTests/CanonicalEnergyLocalizer.lean test10 00
Tests.CanonicalEnergyStoppingTimeTests/CanonicalEnergyStoppingTime.lean test10 00
Tests.CanonicalFisherTransportPairingTests/CanonicalFisherTransportPairing.lean test20 00
Tests.CanonicalGlobalCompetitorTests/CanonicalGlobalCompetitor.lean test10 00
Tests.CanonicalKLDissipationTests/CanonicalKLDissipation.lean test10 00
Tests.CanonicalLocalizationTheoremTests/CanonicalLocalizationTheorem.lean test10 00
Tests.CanonicalRawLocalizationTests/CanonicalRawLocalization.lean test10 00
Tests.CanonicalRawLocalizationL2Tests/CanonicalRawLocalizationL2.lean test10 00
Tests.CanonicalRelativeFisherTests/CanonicalRelativeFisher.lean test10 00
Tests.CanonicalStoppedItoIntegralTests/CanonicalStoppedItoIntegral.lean test10 00
Tests.CarreDuChampTests/CarreDuChamp.lean test11 00
Tests.Chapter1ProgressiveAPITests/Chapter1ProgressiveAPI.lean test30 00
Tests.ChewiDefinition1_1_17Tests/ChewiDefinition1_1_17.lean test10 00
Tests.ChewiItoFormulaTests/ChewiItoFormula.lean test20 00
Tests.ChewiItoProcessTests/ChewiItoProcess.lean test10 00
Tests.ChewiItoProcessProgressiveTests/ChewiItoProcessProgressive.lean test10 00
Tests.ChewiProposition1_1_16Tests/ChewiProposition1_1_16.lean test10 00
Tests.ChewiTheorem1_3_23Tests/ChewiTheorem1_3_23.lean test10 00
Tests.CoefficientTruncationTests/CoefficientTruncation.lean test10 00
Tests.CommonMassTests/CommonMass.lean test10 00
Tests.CommonMassNormalizedProductTests/CommonMassNormalizedProduct.lean test10 00
Tests.CommonMassProductMapTests/CommonMassProductMap.lean test10 00
Tests.CommonMassSliceTests/CommonMassSlice.lean test10 00
Tests.CommonMassSliceFamilyTests/CommonMassSliceFamily.lean test10 00
Tests.CommonNoiseContractionTests/CommonNoiseContraction.lean test10 00
Tests.CommonRemovableMassTests/CommonRemovableMass.lean test10 00
Tests.CommonSlicePermutationReplacementTests/CommonSlicePermutationReplacement.lean test10 00
Tests.CompletedEnergyTests/CompletedEnergy.lean test10 00
Tests.CompletedIntegrandTests/CompletedIntegrand.lean test10 00
Tests.ConditionalResamplingTests/ConditionalResampling.lean test10 00
Tests.ContinuousCostWeakLowerSemicontinuityTests/ContinuousCostWeakLowerSemicontinuity.lean test10 00
Tests.ContinuousDoobL2Tests/ContinuousDoobL2.lean test10 00
Tests.ConvexAEDifferentiableTests/ConvexAEDifferentiable.lean test10 00
Tests.ConvexDomainACAEDifferentiableTests/ConvexDomainACAEDifferentiable.lean test10 00
Tests.ConvexInteriorAETests/ConvexInteriorAE.lean test10 00
Tests.ConvexLocalSubgradientTests/ConvexLocalSubgradient.lean test10 00
Tests.ConvexOpenAEDifferentiableTests/ConvexOpenAEDifferentiable.lean test10 00
Tests.ConvexSubgradientTests/ConvexSubgradient.lean test10 00
Tests.CoordinateHeatBathTests/CoordinateHeatBath.lean test32 00
Tests.CoordinateHeatBathConditionalTests/CoordinateHeatBathConditional.lean test311 00
Tests.CouplingAEMarginalsTests/CouplingAEMarginals.lean test10 00
Tests.CouplingConvexDomainAETests/CouplingConvexDomainAE.lean test10 00
Tests.CouplingGraphTests/CouplingGraph.lean test10 00
Tests.CouplingGraphIdentityTests/CouplingGraphIdentity.lean test10 00
Tests.CouplingQuadraticIntegrabilityTests/CouplingQuadraticIntegrability.lean test10 00
Tests.CycleSuccessorDistinctTests/CycleSuccessorDistinct.lean test10 00
Tests.CyclicCostExpectationTests/CyclicCostExpectation.lean test10 00
Tests.CyclicQuadraticCostTests/CyclicQuadraticCost.lean test10 00
Tests.DiagonalProductCostIntegralTests/DiagonalProductCostIntegral.lean test10 00
Tests.DiscreteDoobL2Tests/DiscreteDoobL2.lean test10 00
Tests.DisplacementChangeOfVariablesTests/DisplacementChangeOfVariables.lean test10 00
Tests.DisplacementConvexGradientPositiveTests/DisplacementConvexGradientPositive.lean test10 00
Tests.DisplacementConvexPotentialSupportTests/DisplacementConvexPotentialSupport.lean test10 00
Tests.DisplacementDerivativeDetPosTests/DisplacementDerivativeDetPos.lean test10 00
Tests.DisplacementDerivativeLogDetTests/DisplacementDerivativeLogDet.lean test10 00
Tests.DisplacementDerivativeMatrixTests/DisplacementDerivativeMatrix.lean test10 00
Tests.DisplacementEntropyPushforwardTests/DisplacementEntropyPushforward.lean test10 00
Tests.DisplacementGradientDerivativeSymmetryTests/DisplacementGradientDerivativeSymmetry.lean test10 00
Tests.DisplacementInterpolationTests/DisplacementInterpolation.lean test10 00
Tests.DisplacementInterpolationConstantSpeedTests/DisplacementInterpolationConstantSpeed.lean test10 00
Tests.DisplacementInterpolationCostTests/DisplacementInterpolationCost.lean test10 00
Tests.DisplacementInterpolationCouplingTests/DisplacementInterpolationCoupling.lean test10 00
Tests.DisplacementJacobianAffineSpectrumTests/DisplacementJacobianAffineSpectrum.lean test10 00
Tests.DisplacementJacobianEntropyTests/DisplacementJacobianEntropy.lean test10 00
Tests.DisplacementJacobianMatrixLogDetTests/DisplacementJacobianMatrixLogDet.lean test10 00
Tests.DisplacementMapDerivativeTests/DisplacementMapDerivative.lean test10 00
Tests.DisplacementMapInjectivityTests/DisplacementMapInjectivity.lean test10 00
Tests.DisplacementMonotoneDerivativeTests/DisplacementMonotoneDerivative.lean test10 00
Tests.DisplacementPositiveOperatorTests/DisplacementPositiveOperator.lean test10 00
Tests.DisplacementPotentialEnergyTests/DisplacementPotentialEnergy.lean test10 00
Tests.DisplacementRealQuadraticCostTests/DisplacementRealQuadraticCost.lean test10 00
Tests.DisplacementSupportingPotentialTests/DisplacementSupportingPotential.lean test10 00
Tests.DyadicElementaryRefinementTests/DyadicElementaryRefinement.lean test10 00
Tests.DyadicElementaryStoppingTests/DyadicElementaryStopping.lean test10 00
Tests.DyadicGlobalHorizonTests/DyadicGlobalHorizon.lean test10 00
Tests.DyadicGridStoppingItoTests/DyadicGridStoppingIto.lean test10 00
Tests.DyadicHorizonExtensionTests/DyadicHorizonExtension.lean test10 00
Tests.DyadicHorizonItoTests/DyadicHorizonIto.lean test10 00
Tests.ElementaryItoAlgebraTests/ElementaryItoAlgebra.lean test10 00
Tests.ElementaryItoDoobL2Tests/ElementaryItoDoobL2.lean test10 00
Tests.ElementaryItoEmbeddingTests/ElementaryItoEmbedding.lean test10 00
Tests.ElementaryItoIntegralTests/ElementaryItoIntegral.lean test10 00
Tests.ElementaryItoIsometryTests/ElementaryItoIsometry.lean test10 00
Tests.ElementaryItoL2Tests/ElementaryItoL2.lean test10 00
Tests.ElementaryItoProcessTests/ElementaryItoProcess.lean test10 00
Tests.ElementaryStoppingTimeTests/ElementaryStoppingTime.lean test10 00
Tests.EnergyPathContinuityTests/EnergyPathContinuity.lean test10 00
Tests.EnergyStoppedIntegrandTests/EnergyStoppedIntegrand.lean test10 00
Tests.EnergyStoppedItoOverlapTests/EnergyStoppedItoOverlap.lean test10 00
Tests.EnergyStoppedProgressiveL2Tests/EnergyStoppedProgressiveL2.lean test10 00
Tests.EnergyStoppingBoundaryBridgeTests/EnergyStoppingBoundaryBridge.lean test10 00
Tests.EnergyStoppingL2BridgeTests/EnergyStoppingL2Bridge.lean test10 00
Tests.EuclideanBrownianCoordinatesTests/EuclideanBrownianCoordinates.lean test10 00
Tests.FellerGeneratorBridgeTests/FellerGeneratorBridge.lean test10 00
Tests.FellerSemigroupTests/FellerSemigroup.lean test11 00
Tests.FiniteDimensionalItoProcessTests/FiniteDimensionalItoProcess.lean test10 00
Tests.FiniteDimensionalItoProcessProgressiveTests/FiniteDimensionalItoProcessProgressive.lean test10 00
Tests.FiniteDimensionalNormBridgeTests/FiniteDimensionalNormBridge.lean test20 00
Tests.FiniteProductPairMarginalTests/FiniteProductPairMarginal.lean test10 00
Tests.FiniteProductSupportTests/FiniteProductSupport.lean test10 00
Tests.FiniteRemainderTests/FiniteRemainder.lean test10 00
Tests.FiniteSumDominationTests/FiniteSumDomination.lean test10 00
Tests.FiniteTimeGridTests/FiniteTimeGrid.lean test10 00
Tests.GaussianConditionalKernelTests/GaussianConditionalKernel.lean test20 00
Tests.GaussianFourthMomentTests/GaussianFourthMoment.lean test10 00
Tests.GaussianSmoothingTests/GaussianSmoothing.lean test10 00
Tests.GeneratorFunctionalInequalitiesTests/GeneratorFunctionalInequalities.lean test10 00
Tests.GeneratorStationarityTests/GeneratorStationarity.lean test10 00
Tests.GeodesicConvexityTests/GeodesicConvexity.lean test10 00
Tests.GeodesicFisherTransportTests/GeodesicFisherTransport.lean test10 00
Tests.GibbsAugmentationTests/GibbsAugmentation.lean test20 00
Tests.GibbsGradientMomentTests/GibbsGradientMoment.lean test10 00
Tests.GlobalCanonicalLocalizerLimitTests/GlobalCanonicalLocalizerLimit.lean test10 00
Tests.GlobalItoProcessGluingTests/GlobalItoProcessGluing.lean test10 00
Tests.GlobalItoProcessProgressiveTests/GlobalItoProcessProgressive.lean test10 00
Tests.GlobalLocalProgressiveL2Tests/GlobalLocalProgressiveL2.lean test10 00
Tests.GlobalStoppedItoMartingaleTests/GlobalStoppedItoMartingale.lean test10 00
Tests.GlobalStoppedItoOverlapTests/GlobalStoppedItoOverlap.lean test10 00
Tests.GlobalStoppedL2OverlapTests/GlobalStoppedL2Overlap.lean test10 00
Tests.GlobalStoppedProgressiveL2Tests/GlobalStoppedProgressiveL2.lean test10 00
Tests.GradientAlgebraTests/GradientAlgebra.lean test10 00
Tests.HeatBathTests/HeatBath.lean test20 00
Tests.HessianStrongConvexityTests/HessianStrongConvexity.lean test30 00
Tests.IsotropicGaussianDensityTests/IsotropicGaussianDensity.lean test13 00
Tests.ItoHorizonConsistencyTests/ItoHorizonConsistency.lean test10 00
Tests.ItoHorizonProcessConsistencyTests/ItoHorizonProcessConsistency.lean test10 00
Tests.ItoIntegralProcessTests/ItoIntegralProcess.lean test13 00
Tests.ItoIntegralProcessAfterHorizonTests/ItoIntegralProcessAfterHorizon.lean test10 00
Tests.ItoIntegralProcessCongruenceTests/ItoIntegralProcessCongruence.lean test10 00
Tests.ItoTerminalCompletionTests/ItoTerminalCompletion.lean test10 00
Tests.KantorovichDualTests/KantorovichDual.lean test10 00
Tests.KernelInvarianceTests/KernelInvariance.lean test10 00
Tests.KernelMixtureTests/KernelMixture.lean test31 00
Tests.KernelTotalVariationTests/KernelTotalVariation.lean test10 00
Tests.KernelTransportTests/KernelTransport.lean test53 00
Tests.L2ExpectationTests/L2Expectation.lean test10 00
Tests.L2GeneratorIdentitiesTests/L2GeneratorIdentities.lean test10 00
Tests.LaggedDyadicApproximationTests/LaggedDyadicApproximation.lean test10 00
Tests.LaggedDyadicConvergenceTests/LaggedDyadicConvergence.lean test10 00
Tests.LangevinCanonicalFisherGammaTests/LangevinCanonicalFisherGamma.lean test10 00
Tests.LangevinCarreDuChampTests/LangevinCarreDuChamp.lean test10 00
Tests.LangevinKLDissipationTests/LangevinKLDissipation.lean test10 00
Tests.LeftLebesgueAverageTests/LeftLebesgueAverage.lean test10 00
Tests.LocalProgressiveL2Tests/LocalProgressiveL2.lean test10 00
Tests.LocalizationTests/Localization.lean test10 00
Tests.MarkovMeasureEvolutionTests/MarkovMeasureEvolution.lean test10 00
Tests.MarkovSemigroupTests/MarkovSemigroup.lean test10 00
Tests.MartingaleTests/Martingale.lean test10 00
Tests.MeasurableGradientTests/MeasurableGradient.lean test10 00
Tests.MetricCurveTests/MetricCurve.lean test10 00
Tests.NormalizedFiniteMeasureTests/NormalizedFiniteMeasure.lean test10 00
Tests.NormalizedFiniteMeasureIntegralTests/NormalizedFiniteMeasureIntegral.lean test10 00
Tests.OperatorGeneratorTests/OperatorGenerator.lean test11 00
Tests.OperatorGeneratorDomainTests/OperatorGeneratorDomain.lean test12 00
Tests.PairingClosedChainTests/PairingClosedChain.lean test10 00
Tests.PairingClosedChainMonotonicityTests/PairingClosedChainMonotonicity.lean test10 00
Tests.PairingCycleNeighborhoodTests/PairingCycleNeighborhood.lean test10 00
Tests.PairingCycleQuantitativeNeighborhoodTests/PairingCycleQuantitativeNeighborhood.lean test10 00
Tests.PairingCyclicMonotonicityTests/PairingCyclicMonotonicity.lean test10 00
Tests.PairingRockafellarConvexDomainTests/PairingRockafellarConvexDomain.lean test10 00
Tests.PairingRockafellarPotentialTests/PairingRockafellarPotential.lean test10 00
Tests.PairingRockafellarRealDomainTests/PairingRockafellarRealDomain.lean test10 00
Tests.PairingRockafellarRealSupportTests/PairingRockafellarRealSupport.lean test10 00
Tests.PairingRockafellarSubgradientTests/PairingRockafellarSubgradient.lean test10 00
Tests.PairingRockafellarSupportGradientTests/PairingRockafellarSupportGradient.lean test10 00
Tests.PermutedMarginalReplacementTests/PermutedMarginalReplacement.lean test10 00
Tests.PermutedProductCostIntegralTests/PermutedProductCostIntegral.lean test10 00
Tests.PermutedQuadraticCostTests/PermutedQuadraticCost.lean test10 00
Tests.PermutedReplacementQuadraticCostTests/PermutedReplacementQuadraticCost.lean test10 00
Tests.PositiveComponentAETests/PositiveComponentAE.lean test10 00
Tests.PrefixIntegralTests/PrefixIntegral.lean test10 00
Tests.ProbabilityCouplingCompactnessTests/ProbabilityCouplingCompactness.lean test10 00
Tests.ProgressiveDriftIntegralTests/ProgressiveDriftIntegral.lean test10 00
Tests.ProgressiveL2Tests/ProgressiveL2.lean test10 00
Tests.ProgressiveL2AlgebraTests/ProgressiveL2Algebra.lean test10 00
Tests.ProgressiveL2DensityTests/ProgressiveL2Density.lean test10 00
Tests.ProgressiveL2HorizonExtensionTests/ProgressiveL2HorizonExtension.lean test10 00
Tests.ProgressiveL2StoppingTests/ProgressiveL2Stopping.lean test10 00
Tests.ProgressiveL2TruncationTests/ProgressiveL2Truncation.lean test10 00
Tests.ProximalBPSConditionalBochnerTests/ProximalBPSConditionalBochner.lean test10 00
Tests.ProximalBPSConditionalGradientTests/ProximalBPSConditionalGradient.lean test10 00
Tests.ProximalBPSConditionalResolventTests/ProximalBPSConditionalResolvent.lean test10 00
Tests.ProximalBPSConditionalScoreTests/ProximalBPSConditionalScore.lean test10 00
Tests.ProximalBPSConditionalScoreDomainTests/ProximalBPSConditionalScoreDomain.lean test10 00
Tests.ProximalBPSGaussianAugmentationTests/ProximalBPSGaussianAugmentation.lean test12 00
Tests.ProximalBPSGaussianReflectionTests/ProximalBPSGaussianReflection.lean test10 00
Tests.ProximalBPSMacroscopicRepresentativeTests/ProximalBPSMacroscopicRepresentative.lean test10 00
Tests.ProximalBPSReflectionL2Tests/ProximalBPSReflectionL2.lean test20 00
Tests.QuadraticOptimalBrenierMapTests/QuadraticOptimalBrenierMap.lean test10 00
Tests.QuadraticOptimalMapTests/QuadraticOptimalMap.lean test10 00
Tests.QuadraticOptimalMapUniquenessTests/QuadraticOptimalMapUniqueness.lean test10 00
Tests.QuadraticOptimalMidpointTests/QuadraticOptimalMidpoint.lean test10 00
Tests.QuadraticOptimalRealMinimalityTests/QuadraticOptimalRealMinimality.lean test10 00
Tests.QuadraticOptimalSupportCyclicTests/QuadraticOptimalSupportCyclic.lean test10 00
Tests.QuadraticOptimalUniquenessTests/QuadraticOptimalUniqueness.lean test10 00
Tests.QuadraticRegularizationTests/QuadraticRegularization.lean test30 00
Tests.QuantitativeSupportLocalBlocksTests/QuantitativeSupportLocalBlocks.lean test10 00
Tests.RNLogRatioTests/RNLogRatio.lean test10 00
Tests.RandomScanHeatBathTests/RandomScanHeatBath.lean test210 00
Tests.RandomScanHeatBathReversibilityTests/RandomScanHeatBathReversibility.lean test213 00
Tests.RandomStoppingBoundaryTests/RandomStoppingBoundary.lean test10 00
Tests.RandomStoppingDyadicApproxTests/RandomStoppingDyadicApprox.lean test10 00
Tests.RandomStoppingGeneralItoTests/RandomStoppingGeneralIto.lean test10 00
Tests.RandomStoppingIntegrandLimitTests/RandomStoppingIntegrandLimit.lean test10 00
Tests.RandomStoppingItoTerminalTests/RandomStoppingItoTerminal.lean test10 00
Tests.RandomStoppingL2ContractionTests/RandomStoppingL2Contraction.lean test10 00
Tests.RandomStoppingL2ConvergenceTests/RandomStoppingL2Convergence.lean test10 00
Tests.RandomStoppingProcessApproxTests/RandomStoppingProcessApprox.lean test10 00
Tests.RandomStoppingProcessConsistencyTests/RandomStoppingProcessConsistency.lean test10 00
Tests.RandomStoppingProgressiveL2Tests/RandomStoppingProgressiveL2.lean test10 00
Tests.RelativeFisherTests/RelativeFisher.lean test10 00
Tests.ReplacementCompetitorTests/ReplacementCompetitor.lean test10 00
Tests.ReplacementCompetitorQuadraticCostTests/ReplacementCompetitorQuadraticCost.lean test10 00
Tests.ReversibilityTests/Reversibility.lean test11 00
Tests.ReversibleGeneratorTests/ReversibleGenerator.lean test10 00
Tests.SampleWikiExampleCasesTests/SampleWikiExampleCases.lean test20 00
Tests.SampledElementaryApproximationTests/SampledElementaryApproximation.lean test10 00
Tests.SemigroupDecayTests/SemigroupDecay.lean test11 00
Tests.Shared.ConvexGradientGapSharpnessTests/Shared/ConvexGradientGapSharpness.lean test20 00
Tests.Shared.ConvexSmoothGradientTests/Shared/ConvexSmoothGradient.lean test20 00
Tests.Shared.ConvexityC1Tests/Shared/ConvexityC1.lean test10 00
Tests.Shared.ConvexityC2Tests/Shared/ConvexityC2.lean test20 00
Tests.Shared.GradientDescentComplexityTests/Shared/GradientDescentComplexity.lean test40 00
Tests.Shared.GradientDescentContractionTests/Shared/GradientDescentContraction.lean test10 00
Tests.Shared.GradientDescentOptimalStepTests/Shared/GradientDescentOptimalStep.lean test20 00
Tests.Shared.GradientDescentPLTests/Shared/GradientDescentPL.lean test30 00
Tests.Shared.GradientDescentRatesTests/Shared/GradientDescentRates.lean test20 00
Tests.Shared.GradientDescentSharpnessTests/Shared/GradientDescentSharpness.lean test10 00
Tests.Shared.GradientDescentStationarityTests/Shared/GradientDescentStationarity.lean test30 00
Tests.Shared.GradientDescentValueTests/Shared/GradientDescentValue.lean test10 00
Tests.Shared.GradientFlowContractionTests/Shared/GradientFlowContraction.lean test20 00
Tests.Shared.GradientFlowLastIterateTests/Shared/GradientFlowLastIterate.lean test20 00
Tests.Shared.GradientFlowPLTests/Shared/GradientFlowPL.lean test20 00
Tests.Shared.GradientFlowStationarityTests/Shared/GradientFlowStationarity.lean test20 00
Tests.Shared.GradientFlowValueTests/Shared/GradientFlowValue.lean test20 00
Tests.Shared.QuadraticGradientDescentTests/Shared/QuadraticGradientDescent.lean test23 00
Tests.Shared.QuadraticRegularizationFirstOrderTests/Shared/QuadraticRegularizationFirstOrder.lean test30 00
Tests.Shared.QuadraticRegularizationOracleTests/Shared/QuadraticRegularizationOracle.lean test30 00
Tests.Shared.QuadraticRegularizationTransferTests/Shared/QuadraticRegularizationTransfer.lean test50 00
Tests.Shared.RestartLogComplexityTests/Shared/RestartLogComplexity.lean test40 00
Tests.Shared.RestartReductionTests/Shared/RestartReduction.lean test40 00
Tests.Shared.SmoothnessEquivalencesTests/Shared/SmoothnessEquivalences.lean test10 00
Tests.Shared.StrongConvexFirstOrderTests/Shared/StrongConvexFirstOrder.lean test10 00
Tests.Shared.StrongConvexGradientConverseTests/Shared/StrongConvexGradientConverse.lean test10 00
Tests.Shared.StrongConvexPLPullbackTests/Shared/StrongConvexPLPullback.lean test31 00
Tests.Shared.UniformRegularizationTests/Shared/UniformRegularization.lean test30 00
Tests.SimultaneousFDivergenceTests/SimultaneousFDivergence.lean test10 00
Tests.SimultaneousFDivergenceGradientTests/SimultaneousFDivergenceGradient.lean test10 00
Tests.SimultaneousFDivergenceIntegralTests/SimultaneousFDivergenceIntegral.lean test10 00
Tests.SmoothedPicardHMCAdaptiveCenterRGOTests/SmoothedPicardHMCAdaptiveCenterRGO.lean test10 00
Tests.SmoothedPicardHMCAdaptiveKLErrorTests/SmoothedPicardHMCAdaptiveKLError.lean test10 00
Tests.SmoothedPicardHMCApproximateInitialGradientMomentTests/SmoothedPicardHMCApproximateInitialGradientMoment.lean test10 00
Tests.SmoothedPicardHMCClippedGradientProgramTests/SmoothedPicardHMCClippedGradientProgram.lean test10 00
Tests.SmoothedPicardHMCClippedMeanExponentialTests/SmoothedPicardHMCClippedMeanExponential.lean test10 00
Tests.SmoothedPicardHMCClippedRenyiComparisonTests/SmoothedPicardHMCClippedRenyiComparison.lean test10 00
Tests.SmoothedPicardHMCEnhancedFiniteOutputKLTests/SmoothedPicardHMCEnhancedFiniteOutputKL.lean test10 00
Tests.SmoothedPicardHMCEnhancedKLOneStepTests/SmoothedPicardHMCEnhancedKLOneStep.lean test10 00
Tests.SmoothedPicardHMCEnhancedTerminalExecutionTests/SmoothedPicardHMCEnhancedTerminalExecution.lean test10 00
Tests.SmoothedPicardHMCFiniteRGOKLErrorTests/SmoothedPicardHMCFiniteRGOKLError.lean test10 00
Tests.SmoothedPicardHMCFiniteRGOProgramTests/SmoothedPicardHMCFiniteRGOProgram.lean test10 00
Tests.SmoothedPicardHMCGaussianArcLawTests/SmoothedPicardHMCGaussianArcLaw.lean test10 00
Tests.SmoothedPicardHMCGaussianKLTests/SmoothedPicardHMCGaussianKL.lean test10 00
Tests.SmoothedPicardHMCGaussianMixtureTests/SmoothedPicardHMCGaussianMixture.lean test10 00
Tests.SmoothedPicardHMCGaussianPowerMomentTests/SmoothedPicardHMCGaussianPowerMoment.lean test10 00
Tests.SmoothedPicardHMCGaussianRGOErrorBudgetTests/SmoothedPicardHMCGaussianRGOErrorBudget.lean test10 00
Tests.SmoothedPicardHMCGibbsPositionMomentTests/SmoothedPicardHMCGibbsPositionMoment.lean test10 00
Tests.SmoothedPicardHMCGradientArcMeanTests/SmoothedPicardHMCGradientArcMean.lean test10 00
Tests.SmoothedPicardHMCIdealRGOIdentificationTests/SmoothedPicardHMCIdealRGOIdentification.lean test10 00
Tests.SmoothedPicardHMCJointReferenceGradientDescentTests/SmoothedPicardHMCJointReferenceGradientDescent.lean test10 00
Tests.SmoothedPicardHMCNormalizedReferenceCallTests/SmoothedPicardHMCNormalizedReferenceCall.lean test10 00
Tests.SmoothedPicardHMCObservationConditionalKernelTests/SmoothedPicardHMCObservationConditionalKernel.lean test10 00
Tests.SmoothedPicardHMCPoissonQueryTailTests/SmoothedPicardHMCPoissonQueryTail.lean test10 00
Tests.SmoothedPicardHMCPoissonRejectionTests/SmoothedPicardHMCPoissonRejection.lean test10 00
Tests.SmoothedPicardHMCProximalEstimatorLipschitzTests/SmoothedPicardHMCProximalEstimatorLipschitz.lean test10 00
Tests.SmoothedPicardHMCProximalGaussianEstimatorTests/SmoothedPicardHMCProximalGaussianEstimator.lean test10 00
Tests.SmoothedPicardHMCProxyReverseTransportTests/SmoothedPicardHMCProxyReverseTransport.lean test10 00
Tests.SmoothedPicardHMCRGOBackwardTests/SmoothedPicardHMCRGOBackward.lean test10 00
Tests.SmoothedPicardHMCReferenceCarryingCostTests/SmoothedPicardHMCReferenceCarryingCost.lean test10 00
Tests.SmoothedPicardHMCReferenceCarryingKernelTests/SmoothedPicardHMCReferenceCarryingKernel.lean test10 00
Tests.SmoothedPicardHMCSmoothGradientArcClippingTests/SmoothedPicardHMCSmoothGradientArcClipping.lean test10 00
Tests.SmoothedPicardHMCSmoothGradientArcMomentTests/SmoothedPicardHMCSmoothGradientArcMoment.lean test10 00
Tests.SmoothedPicardHMCStateDependentRGOTests/SmoothedPicardHMCStateDependentRGO.lean test10 00
Tests.SmoothedPicardHMCStoppedGaussianRGOErrorTests/SmoothedPicardHMCStoppedGaussianRGOError.lean test10 00
Tests.SmoothedPicardHMCStoppedRGODepthTests/SmoothedPicardHMCStoppedRGODepth.lean test10 00
Tests.SmoothedPicardHMCTerminalFORSKernelTests/SmoothedPicardHMCTerminalFORSKernel.lean test10 00
Tests.SmoothedPicardHMCTerminalReferenceGradientDescentTests/SmoothedPicardHMCTerminalReferenceGradientDescent.lean test10 00
Tests.SmoothedPicardHMCTerminalSamplerAccuracyCostTests/SmoothedPicardHMCTerminalSamplerAccuracyCost.lean test10 00
Tests.SmoothedPicardHMCTruncationTests/SmoothedPicardHMCTruncation.lean test10 00
Tests.SmoothedPicardHMCTwoNoiseRGOTests/SmoothedPicardHMCTwoNoiseRGO.lean test10 00
Tests.SmoothedPicardLogarithmicDepthTests/SmoothedPicardLogarithmicDepth.lean test20 00
Tests.SmoothedPicardRGOCalculusTests/SmoothedPicardRGOCalculus.lean test20 00
Tests.SmoothedPicardRGOClosureTests/SmoothedPicardRGOClosure.lean test10 00
Tests.SmoothedPicardRecursiveConditionTests/SmoothedPicardRecursiveCondition.lean test10 00
Tests.SmoothedPicardRecursiveDepthTests/SmoothedPicardRecursiveDepth.lean test25 00
Tests.SmoothedPicardRecursiveVarianceTests/SmoothedPicardRecursiveVariance.lean test20 00
Tests.StationarityEquivalenceTests/StationarityEquivalence.lean test10 00
Tests.StoppingGraphNullTests/StoppingGraphNull.lean test10 00
Tests.StoppingTimeTests/StoppingTime.lean test10 00
Tests.StrictCycleCheaperLocalReplacementTests/StrictCycleCheaperLocalReplacement.lean test10 00
Tests.StrongConvexGibbsIntegrabilityTests/StrongConvexGibbsIntegrability.lean test20 00
Tests.SupportLocalBlocksTests/SupportLocalBlocks.lean test10 00
Tests.TimeMeasureRealBridgeTests/TimeMeasureRealBridge.lean test10 00
Tests.TransportTests/Transport.lean test10 00
Tests.TransportGluingTests/TransportGluing.lean test10 00
Tests.UniformExpectationGapTests/UniformExpectationGap.lean test10 00
Tests.VectorBrownianFiltrationTests/VectorBrownianFiltration.lean test10 00
Tests.WassersteinFiniteSecondMomentTests/WassersteinFiniteSecondMoment.lean test10 00
Tests.WassersteinSpaceTests/WassersteinSpace.lean test10 00
Tests.WassersteinSymmetryTests/WassersteinSymmetry.lean test10 00
Tests.WassersteinTriangleTests/WassersteinTriangle.lean test10 00
Tests.WassersteinTriangleCoreTests/WassersteinTriangleCore.lean test10 00
Tests.WassersteinTriangleExactTests/WassersteinTriangleExact.lean test10 00
Tests.WassersteinTriangleMarginalsTests/WassersteinTriangleMarginals.lean test10 00
Tests.WeakForwardEquationTests/WeakForwardEquation.lean test10 00
Tests.WeightedGradientDistributionTests/WeightedGradientDistribution.lean test10 00
Tests.WeightedGradientWeakTests/WeightedGradientWeak.lean test10 00
Tests.WeightedLocalL2Tests/WeightedLocalL2.lean test20 00
Tests.WeightedResolventTests/WeightedResolvent.lean test10 00