`OAI/Probability/SpanningForest/`

2103 declarations, 0 contain sorry, 0 declared as axioms; 231 files

Files

AlgebraicCycleSpace.lean 28 declarations
AllPairAllocation.lean 21 declarations
AllPairFactorAssembly.lean 1 declarations
AllPairIID.lean 16 declarations
AllPairIntrinsicBridge.lean 4 declarations
AllPairObservation.lean 15 declarations
AllPairPicardDecoder.lean 8 declarations
AllPairPosteriorDrift.lean 3 declarations
AllPairWiener.lean 21 declarations
AnalyticSupport.lean 17 imports, no declarations
BinaryGaussianPosterior.lean 7 declarations
BinaryLawUnique.lean 4 declarations
BinaryWeakConvergence.lean 4 declarations
BitRecovery.lean 12 declarations
BorelExhaustion.lean 21 declarations
BorelFUSFKernel.lean 6 declarations
BorelFiniteChoice.lean 5 declarations
BrownianBridge.lean 11 declarations
BrownianCanonicalPosterior.lean 6 declarations
BrownianFamilyIdentification.lean 4 declarations
BrownianFamilyNoise.lean 1 declarations
BrownianFamilyPast.lean 7 declarations
BrownianFinitePosterior.lean 2 declarations
BrownianPosteriorReduction.lean 3 declarations
BrownianReference.lean 11 declarations
BrownianSublinear.lean 3 declarations
CanonicalBrownianReference.lean 25 declarations
CanonicalBrownianSampler.lean 9 declarations
CanonicalDecoder.lean 9 declarations
CanonicalDrift.lean 7 declarations
CanonicalFUSFLaw.lean 9 declarations
CanonicalIID.lean 6 declarations
CanonicalPosteriorIdentification.lean 5 declarations
CanonicalPosteriorMartingale.lean 3 declarations
CauchyBinet.lean 16 declarations
CharacteristicRemainder.lean 5 declarations
CharacteristicTaylor.lean 2 declarations
CodeLaplacian.lean 7 declarations
CodeTransferKernel.lean 7 declarations
CodedIncidenceMinors.lean 12 declarations
CodedInclusion.lean 6 declarations
CodedMarginal.lean 6 declarations
CodedMatrixTree.lean 6 declarations
CodedTransferBridge.lean 6 declarations
CodedTransferProjection.lean 5 declarations
ConditionalInnovation.lean 6 declarations
ContinuousPathLaw.lean 13 declarations
ContinuousPathLimit.lean 11 declarations
ContinuousPathSampler.lean 2 declarations
CoordinateTruncation.lean 18 declarations
CountableBrownian.lean 12 declarations
CountableProjective.lean 13 declarations
CylinderKernel.lean 11 declarations
CylinderLimitMeasure.lean 5 declarations
DecoderBundle.lean 5 imports, no declarations
DecoderPathSpace.lean 3 declarations
DecoderRestriction.lean 4 declarations
Definitions.lean 29 declarations
DenseBrownian.lean 17 declarations
DenseGaussian.lean 6 declarations
DenseGaussianModification.lean 2 declarations
DeterminantalResponse.lean 10 declarations
DisconnectedIncidence.lean 10 declarations
DyadicGaussianBound.lean 9 declarations
DyadicInterpolation.lean 21 declarations
DyadicPathLimit.lean 12 declarations
DyadicTimes.lean 18 declarations
EdgeAction.lean 16 declarations
EdgeAllocation.lean 13 declarations
EdgeAllocationMeasurable.lean 7 declarations
EdgeBallExhaustion.lean 19 declarations
EdgeIID.lean 24 declarations
EdgeUniformRule.lean 16 declarations
EquivariantFUSFKernel.lean 2 declarations
Exhaustion.lean 11 declarations
ExhaustionExistence.lean 11 declarations
ExponentialFamily.lean 15 declarations
FUSFExistenceReduction.lean 2 declarations
FUSFLawSupport.lean 9 declarations
FUSFLawUnique.lean 5 declarations
FUSFPosteriorResponse.lean 2 declarations
FUSFRelabelMeasure.lean 6 declarations
Factor.lean 2 declarations
FactorAssembly.lean 16 declarations
FactorLawTransport.lean 4 declarations
FactorReadout.lean 2 declarations
FactorSampler.lean 4 declarations
FinalFactor.lean 7 declarations
FiniteCycleIncidence.lean 17 declarations
FiniteGaussianPosterior.lean 6 declarations
FiniteGradientResponse.lean 5 declarations
FiniteIncidenceBridge.lean 19 declarations
FiniteKernelBridge.lean 5 declarations
FiniteKernelEmbedding.lean 6 declarations
FiniteKernelSupport.lean 4 declarations
FiniteObservationReduction.lean 9 declarations
FinitePosterior.lean 13 declarations
FinitePosteriorTilt.lean 2 declarations
FiniteProductDensity.lean 5 declarations
FiniteResponse.lean 9 declarations
FiniteResponseBundle.lean 1 import, no declarations
FiniteTiltLimit.lean 12 declarations
FiniteTiltMeasure.lean 9 declarations
FiniteUSTIntegrals.lean 11 declarations
FiniteUSTLimit.lean 6 declarations
FiniteUSTMeasure.lean 11 declarations
FiniteUSTProbability.lean 2 declarations
FiniteUSTRelabel.lean 25 declarations
FullObservationPosterior.lean 1 declarations
GaussianBoundedCorrection.lean 14 declarations
GaussianLikelihood.lean 8 declarations
GaussianMomentScaling.lean 10 declarations
GaussianObservationDensity.lean 4 declarations
GaussianObservationKernel.lean 11 declarations
GaussianPosteriorAllTime.lean 6 declarations
GaussianSum.lean 2 declarations
GeneratorExhaustion.lean 6 declarations
GibbsField.lean 21 declarations
GibbsResponse.lean 5 declarations
GlobalWiener.lean 9 declarations
GramDeterminantUpdate.lean 3 declarations
GraphBalls.lean 32 declarations
GraphBorel.lean 17 declarations
GraphCoordinateTruncation.lean 7 declarations
GraphDomain.lean 12 declarations
GraphEncoding.lean 27 declarations
GraphFUSFLaw.lean 3 declarations
GraphFreeKernel.lean 21 declarations
GraphLaw.lean 3 declarations
GraphTreePosterior.lean 27 declarations
GraphTreePosteriorEquiv.lean 8 declarations
GraphTreeResponse.lean 4 declarations
HilbertBundle.lean 7 imports, no declarations
IIDBlocks.lean 2 declarations
IncidenceCirculation.lean 16 declarations
IncidenceMinorClassification.lean 7 declarations
IncidenceResponse.lean 2 declarations
IncidenceUnimodular.lean 10 declarations
InclusionPolynomial.lean 8 declarations
IncreasingProjections.lean 4 declarations
IndependentProcessVectors.lean 3 declarations
InducedCode.lean 11 declarations
InnovationAdapted.lean 5 declarations
InnovationErrorRate.lean 4 declarations
InnovationFiniteGaussian.lean 5 declarations
InnovationGaussianLaw.lean 1 declarations
InnovationGaussianObservation.lean 2 declarations
InnovationGaussianProcess.lean 2 declarations
InnovationIdentification.lean 9 declarations
InnovationLawIdentification.lean 4 declarations
InnovationMartingale.lean 20 declarations
InnovationMean.lean 7 declarations
InnovationMoments.lean 7 declarations
InnovationPhaseRecurrence.lean 18 declarations
InnovationProcessLaw.lean 3 declarations
InnovationProjection.lean 4 declarations
InnovationStep.lean 2 declarations
InnovationSubdivision.lean 6 declarations
InnovationTaylor.lean 5 declarations
IntrinsicBridge.lean 9 declarations
IntrinsicExhaustion.lean 36 declarations
IntrinsicHalfResponse.lean 4 declarations
IntrinsicPosteriorDrift.lean 2 declarations
IntrinsicPosteriorIdentification.lean 4 declarations
IntrinsicRelabel.lean 5 declarations
IntrinsicTotalExhaustion.lean 1 import, no declarations
IntrinsicTreeDrift.lean 15 declarations
JointInnovationLaw.lean 1 declarations
JointProcessLaw.lean 2 declarations
LabelNoCollision.lean 11 declarations
LawLimits.lean 5 imports, no declarations
LawPosteriorBundle.lean 3 imports, no declarations
Main.lean 230 imports, no declarations
MarkedGram.lean 4 declarations
MatrixTreeSupport.lean 14 imports, no declarations
NoCollisionExtension.lean 18 declarations
ObservationPosterior.lean 7 declarations
ObservedBrownianMartingale.lean 3 declarations
OrderedMinorCounting.lean 10 declarations
PathConcatenation.lean 21 declarations
Picard.lean 18 declarations
PicardBounds.lean 18 declarations
PicardNonnegativeSampler.lean 5 declarations
PicardNonnegativeTime.lean 12 declarations
PicardSamplerLaw.lean 9 declarations
PicardSolution.lean 8 declarations
PicardUniqueness.lean 7 declarations
PolynomialGramUpdate.lean 4 declarations
PosteriorDrift.lean 11 declarations
PosteriorIndependentExtension.lean 9 declarations
PosteriorNullCoordinates.lean 3 declarations
PosteriorSupport.lean 9 declarations
PosteriorTiltLimit.lean 21 declarations
ProjectionLimit.lean 8 declarations
RandomReindex.lean 7 declarations
RandomSelection.lean 5 declarations
RawInnovationSampler.lean 4 declarations
ReducedCycleKernel.lean 16 declarations
ReducedLaplacian.lean 14 declarations
Relabeling.lean 15 declarations
ResponseLipschitz.lean 6 declarations
RuleExtension.lean 6 declarations
SampledPathConcatenation.lean 6 declarations
SampledUnitPath.lean 13 declarations
SchauderTail.lean 11 declarations
SchauderTents.lean 35 declarations
SlopeReadout.lean 14 declarations
StochasticBundle.lean 40 imports, no declarations
SubtypeSubsetSums.lean 8 declarations
Theory.lean 43 imports, no declarations
TiltResponse.lean 8 declarations
TotalTreeResponse.lean 5 declarations
TransferCurrent.lean 36 declarations
TransferCurrentLipschitz.lean 7 declarations
TransferProjection.lean 9 declarations
TreePosteriorBridge.lean 5 declarations
USTCylinder.lean 5 declarations
USTDeterminant.lean 3 declarations
USTFiniteDeterminantal.lean 4 declarations
USTFiniteTilt.lean 18 declarations
USTInclusionCount.lean 12 declarations
USTPosteriorResponse.lean 12 declarations
USTResponse.lean 33 declarations
UniformSampler.lean 15 declarations
WeightedCauchyBinet.lean 8 declarations
WeightedInnovation.lean 3 declarations
WeightedTreeBorel.lean 30 declarations
WeightedTreeEquiv.lean 11 declarations
WeightedTreeResponse.lean 5 declarations
WeightedTreeTransport.lean 3 declarations
WienerSampler.lean 13 declarations