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