`OAI/Probability/DilutedSpin/`

3184 declarations, 0 contain sorry, 0 declared as axioms; 405 files

Files

ActualCharging.lean 58 declarations
ActualLowIncrement.lean 4 declarations
ActualNegligible.lean 19 declarations
ActualPrefix.lean 17 declarations
ActualRootVariance.lean 1 declarations
ActualTreeSelector.lean 5 declarations
AdmissibleInterval.lean 3 declarations
AnchorExtension.lean 49 declarations
AveragedEnergyRoot.lean 11 declarations
AveragedMatrixSelection.lean 2 declarations
AveragedRootBounds.lean 2 declarations
BoundedCavityLower.lean 1 declarations
BranchingEvaluation.lean 5 declarations
CanonicalRegularMultileaf.lean 1 declarations
CavityAllocatedMean.lean 9 declarations
CavityAllocation.lean 7 declarations
CavityBounds.lean 9 declarations
CavityDatumProjection.lean 5 declarations
CavityEndpointCount.lean 5 declarations
CavityErrorLimit.lean 2 declarations
CavityGapFubini.lean 2 declarations
CavityIndex.lean 13 declarations
CavityInsertionAlgebra.lean 7 declarations
CavityInsertionFunctional.lean 2 declarations
CavityMaskEnergy.lean 8 declarations
CavityOldNewMean.lean 5 declarations
CavityPack.lean 6 declarations
CavityPoissonEndpoint.lean 2 declarations
CavityProxy.lean 14 declarations
CavityRateLimits.lean 13 declarations
CavitySeparable.lean 11 declarations
CavitySiteMean.lean 3 declarations
CavitySplit.lean 4 declarations
CavityTrialIdentity.lean 10 declarations
CenteredPressure.lean 8 declarations
CenteredTrialLocal.lean 9 declarations
ClippedCavityProxy.lean 4 declarations
ClippedModelFacts.lean 10 declarations
ClippedProxyRate.lean 2 declarations
ColorIterate.lean 6 declarations
ColorPolarization.lean 1 declarations
ColorSymmetry.lean 5 declarations
ColoredAnchor.lean 11 declarations
CommonFresh.lean 3 declarations
CommonTreeSample.lean 13 declarations
CompleteShapeSelection.lean 2 declarations
CompoundCoupling.lean 4 declarations
CompoundMoment.lean 4 declarations
CompoundPhysicalMean.lean 8 declarations
CompoundPoisson.lean 4 declarations
CompoundRate.lean 7 declarations
CompoundRateAverage.lean 2 declarations
CompoundSample.lean 5 declarations
CompoundSuperposition.lean 13 declarations
ConcentrationRate.lean 16 declarations
ConcreteAnalyticSelection.lean 1 declarations
ConcreteHistory.lean 7 declarations
ConcreteReservoir.lean 18 declarations
ConcreteSelection.lean 6 declarations
ConditionalScheduledMean.lean 17 declarations
ConditionalSpatialContinuity.lean 6 declarations
ConvexBounds.lean 10 declarations
CoordinateFiber.lean 13 declarations
Core.lean 1 import, no declarations
CountArrayBridge.lean 5 declarations
CountBridgeTools.lean 6 declarations
CountableFullSupport.lean 1 declarations
CountableReservoir.lean 15 declarations
CountableTagSelection.lean 1 declarations
CountedSizeCoupling.lean 3 declarations
CountedSpinMean.lean 12 declarations
CountedSteps.lean 22 declarations
DenseUpper.lean 2 declarations
DepthChildMoment.lean 6 declarations
DeviationLimitTools.lean 2 declarations
DictionaryAnalytic.lean 2 declarations
DictionaryExtraction.lean 1 declarations
DictionaryPalm.lean 2 declarations
DoubledStemProjection.lean 9 declarations
EarliestChildDepth.lean 4 declarations
EnergyInsertionMean.lean 7 declarations
ExactVariationalLower.lean 2 declarations
ExtendedExponents.lean 4 declarations
ExternalAverageTaylor.lean 4 declarations
ExternalCoefficientLaw.lean 3 declarations
ExternalCovariance.lean 4 declarations
ExternalFreshLaw.lean 1 declarations
ExternalRoot.lean 20 declarations
ExternalTaylor.lean 12 declarations
FiniteAnalytic.lean 7 declarations
FiniteEncoding.lean 20 declarations
FiniteHierarchyDense.lean 5 declarations
FiniteLaw.lean 74 declarations
FiniteLogExpansion.lean 25 declarations
FinitePiInjective.lean 7 declarations
FinitePoissonSplit.lean 6 declarations
FiniteProducts.lean 8 declarations
FiniteProjection.lean 12 declarations
FiniteTowerPi.lean 15 declarations
FirstMomentConditional.lean 1 declarations
FirstMomentCount.lean 1 declarations
FirstMomentFresh.lean 5 declarations
FirstMomentUpper.lean 6 declarations
FirstSplitSchedule.lean 4 declarations
ForkTree.lean 10 declarations
FullCountCorrection.lean 3 declarations
FullCubeConditionalContinuity.lean 11 declarations
FullPalm.lean 7 declarations
FullRegularSelection.lean 8 declarations
FullRootCounts.lean 4 declarations
FullRootIncrement.lean 14 declarations
FullRootPalm.lean 3 declarations
FullSelectedConcentration.lean 1 declarations
FullSelectedError.lean 7 declarations
FullSelectedRawConcentration.lean 3 declarations
FullSelectedRegularity.lean 16 declarations
FullSelectedThermal.lean 13 declarations
FullThermalAverage.lean 5 declarations
FullTreeScore.lean 4 declarations
FunctionalContinuity.lean 12 declarations
FunctionalStability.lean 17 declarations
GeneralPairSquare.lean 3 declarations
GeneralRootArrayLaw.lean 4 declarations
GlobalSelectedAverage.lean 6 declarations
GlobalSelectedConcentration.lean 1 declarations
GlobalSelectedError.lean 5 declarations
GridIncrementSupport.lean 5 declarations
HeightTransport.lean 12 declarations
HeterogeneousFullVariance.lean 1 declarations
HeterogeneousMarks.lean 21 declarations
HeterogeneousProjection.lean 8 declarations
HeterogeneousTwoPoisson.lean 2 declarations
HeterogeneousVariance.lean 1 declarations
HierarchyBasic.lean 16 declarations
HistoryDistinct.lean 5 declarations
HistoryGeometry.lean 66 declarations
HistoryRetained.lean 2 declarations
HistorySelector.lean 8 declarations
IncrementCavityProxy.lean 2 declarations
IncrementErrorLimit.lean 1 declarations
InsertionCoefficient.lean 4 declarations
InsertionPoint.lean 15 declarations
InsertionPoissonAlgebra.lean 6 declarations
InsertionStability.lean 6 declarations
IntegralError.lean 4 declarations
IntegratedFiniteUpper.lean 1 declarations
JointGridSelection.lean 1 declarations
JointPhysicalSelection.lean 1 declarations
JointRootLaw.lean 12 declarations
JointRootParam.lean 3 declarations
KernelTower.lean 26 declarations
LabeledColorHistory.lean 9 declarations
Main.lean 1 declarations
MarkInsertion.lean 15 declarations
MarkMeanProjection.lean 7 declarations
MarkSiteCoupling.lean 6 declarations
MarkedPoisson.lean 18 declarations
MarkerConcrete.lean 10 declarations
MarkerGeometry.lean 24 declarations
MarkerHistory.lean 3 declarations
MarkerHistoryTransport.lean 3 declarations
MarkerJointHistory.lean 3 declarations
MarkerNormalization.lean 3 declarations
MarkerPhysicalBridge.lean 4 declarations
MarkerRootIdentity.lean 1 declarations
MarkerScheduledIdentity.lean 1 declarations
MarkerVariance.lean 12 declarations
MatrixConstant.lean 3 declarations
MatrixEnergy.lean 10 declarations
MatrixHistory.lean 8 declarations
MatrixLeafProjection.lean 5 declarations
MatrixNormalization.lean 6 declarations
MatrixPair.lean 5 declarations
MatrixPhysical.lean 3 declarations
MatrixRoot.lean 6 declarations
MatrixTriple.lean 13 declarations
MeasurableEncoding.lean 4 declarations
MeasurableEnergy.lean 3 declarations
MeasurableProjectionError.lean 15 declarations
MeasurableProjector.lean 8 declarations
MeasurableShapeEnergy.lean 7 declarations
MeasureHierarchy.lean 27 declarations
MixedDeviation.lean 4 declarations
MixedEnergy.lean 10 declarations
MixedPatterns.lean 12 declarations
MixtureMeasures.lean 12 declarations
Model.lean 21 declarations
MultileafMatrixPointwise.lean 10 declarations
NormalizationSymmetry.lean 9 declarations
NormalizedCutoff.lean 18 declarations
NormalizedInsertion.lean 6 declarations
NormalizedPalm.lean 1 declarations
OldEnergyEmbedding.lean 3 declarations
OneNewLaw.lean 4 declarations
OverlapDepthAverage.lean 3 declarations
PairSquare.lean 16 declarations
PalmError.lean 2 declarations
ParameterConcentration.lean 1 declarations
ParameterPalm.lean 1 declarations
ParameterProduct.lean 8 declarations
ParameterRate.lean 16 declarations
ParameterScoreMeasurable.lean 6 declarations
PatternComparison.lean 45 declarations
Perturbations.lean 30 declarations
PerturbedEnergyMean.lean 3 declarations
PerturbedSizeCoupling.lean 6 declarations
PhysicalAverages.lean 9 declarations
PhysicalCavityPoisson.lean 2 declarations
PhysicalCavityRate.lean 4 declarations
PhysicalCavitySplit.lean 2 declarations
PhysicalCountLaw.lean 2 declarations
PhysicalEncodingInterior.lean 2 declarations
PhysicalFieldOrder.lean 7 declarations
PhysicalGridMultileaf.lean 1 declarations
PhysicalIndex.lean 11 declarations
PhysicalInsertionComparison.lean 8 declarations
PhysicalInsertionEnergy.lean 2 declarations
PhysicalInsertionIdentity.lean 2 declarations
PhysicalInsertionLimit.lean 3 declarations
PhysicalMarkerControl.lean 6 declarations
PhysicalMultileafMoments.lean 1 declarations
PhysicalNewSpin.lean 2 declarations
PhysicalOverlapAverage.lean 6 declarations
PhysicalOverlapConcentration.lean 8 declarations
PhysicalOverlapLimit.lean 7 declarations
PhysicalPairConnection.lean 11 declarations
PhysicalPairEnergy.lean 5 declarations
PhysicalReservoirIncrement.lean 8 declarations
PhysicalScheduledMultileaf.lean 1 declarations
PhysicalScheduledStep.lean 5 declarations
PhysicalScoreRate.lean 1 declarations
PhysicalSelectedConcentration.lean 1 declarations
PhysicalShapeError.lean 10 declarations
PhysicalSingleton.lean 4 declarations
PhysicalSubtreeConcentration.lean 5 declarations
PhysicalTreeMatrix.lean 3 declarations
PoissonCountThinning.lean 10 declarations
PoissonInsertionLimit.lean 1 declarations
PoissonMoments.lean 12 declarations
PoissonRateCoupling.lean 1 declarations
PoissonReplacement.lean 6 declarations
PoissonRootSelection.lean 2 declarations
PoissonSiteThinning.lean 4 declarations
PoissonSmoothing.lean 2 declarations
PoissonVariance.lean 46 declarations
Polarization.lean 16 declarations
PrefixProjection.lean 15 declarations
PressureLiminf.lean 2 declarations
ProductComparison.lean 1 declarations
ProductEvaluationContinuity.lean 6 declarations
ProductPatterns.lean 6 declarations
ProductTower.lean 3 declarations
ProductTowers.lean 43 declarations
ProfileHistory.lean 14 declarations
ProjectionShiftError.lean 7 declarations
ProperChildScheduleContinuity.lean 8 declarations
ProxyRateIncrement.lean 3 declarations
QIntegration.lean 6 declarations
QSubsetDeviation.lean 8 declarations
QSubtreePotential.lean 19 declarations
QTopologyBound.lean 15 declarations
QTreeLaw.lean 10 declarations
RandomInsertion.lean 4 declarations
RawPatternIdentity.lean 4 declarations
RealEncoding.lean 14 declarations
RegularBadMass.lean 9 declarations
RegularCovarianceConvergence.lean 4 declarations
RegularCovarianceLimit.lean 6 declarations
RegularDepth.lean 9 declarations
RegularFrameExtraction.lean 2 declarations
RegularNodeAverage.lean 8 declarations
RegularNodeEstimates.lean 17 declarations
RegularNodeGeometry.lean 8 declarations
RegularNodeProducer.lean 1 declarations
RegularOverlapGeometry.lean 5 declarations
RegularPhysicalShift.lean 4 declarations
RegularScheduleShift.lean 4 declarations
RegularizedNormalization.lean 4 declarations
ReservoirBondEnergy.lean 4 declarations
ReservoirEnergyBounds.lean 4 declarations
ReservoirInsertionEnergy.lean 1 declarations
ReservoirInsertionOnEnergy.lean 3 declarations
ReservoirRate.lean 11 declarations
ReservoirShapeLimit.lean 5 declarations
ReservoirSitePoisson.lean 1 declarations
ReservoirSiteTransport.lean 2 declarations
ReservoirTrees.lean 191 imports, no declarations
ReservoirVariance.lean 19 declarations
RetainedHistory.lean 4 declarations
RootAE.lean 3 declarations
RootChildMoment.lean 6 declarations
RootChildSumIntegrability.lean 7 declarations
RootCoefficients.lean 15 declarations
RootDeviationDistance.lean 2 declarations
RootEncoding.lean 7 declarations
RootIntegralOrder.lean 2 declarations
RootLogComparison.lean 1 declarations
RootMapLaw.lean 2 declarations
RootMarkerEstimate.lean 6 declarations
RootMatrixTriple.lean 8 declarations
RootMultileafMatrix.lean 11 declarations
RootOverlapBounds.lean 5 declarations
RootOverlapDeviation.lean 5 declarations
RootOverlapVariance.lean 8 declarations
RootPatternComparison.lean 7 declarations
RootPatternProduct.lean 6 declarations
RootProductLaw.lean 4 declarations
RootProjectionIntegrability.lean 12 declarations
RootProjectionShiftError.lean 7 declarations
RootShapeEnergy.lean 5 declarations
RootShiftIntegrability.lean 3 declarations
RootSplit.lean 3 declarations
SameInsertionAverage.lean 7 declarations
ScheduledContinuity.lean 4 declarations
ScheduledCovariance.lean 6 declarations
ScheduledEnergyBound.lean 6 declarations
ScheduledEvaluationContinuity.lean 6 declarations
ScheduledFrameError.lean 7 declarations
ScheduledFrameGeometry.lean 12 declarations
ScheduledGeometry.lean 4 declarations
ScheduledMarkerEstimate.lean 7 declarations
ScheduledMultileafMatrix.lean 1 declarations
ScheduledProtectedLabels.lean 6 declarations
ScheduledRegularFrame.lean 4 declarations
ScheduledRelativeCharge.lean 2 declarations
ScheduledRootMultileaf.lean 7 declarations
ScheduledSelection.lean 2 declarations
ScheduledSingleton.lean 5 declarations
ScheduledTopology.lean 12 declarations
ScoreIncrement.lean 2 declarations
SelectedPalm.lean 5 declarations
SelectedRegularity.lean 2 declarations
SelectedTree.lean 9 declarations
SelectorPolarization.lean 2 declarations
ShapeCharging.lean 2 declarations
ShapeEmbedding.lean 14 declarations
ShapeMarginal.lean 4 declarations
ShapeMatrix.lean 8 declarations
ShapeMatrixPhysical.lean 5 declarations
ShapeMean.lean 13 declarations
ShapeProjectionEnergy.lean 8 declarations
ShapeRoot.lean 8 declarations
ShiftedFrameGeometry.lean 11 declarations
ShiftedTree.lean 27 declarations
SimultaneousShift.lean 8 declarations
SingletonAverage.lean 5 declarations
SingletonRoot.lean 24 declarations
SingletonSelection.lean 1 declarations
SizeSpinRoot.lean 25 declarations
SpatialScheduledContinuity.lean 7 declarations
SpinBaseComparison.lean 5 declarations
SpinLogContinuous.lean 2 declarations
SpinMarginal.lean 7 declarations
SpinRootData.lean 21 declarations
SplitDepthContinuity.lean 20 declarations
StemCoupling.lean 6 declarations
StemCovarianceTransfer.lean 3 declarations
StemTwoSideProjection.lean 3 declarations
SubsetTree.lean 3 declarations
SymmetricTrialLower.lean 1 declarations
TargetEvaluationContinuity.lean 7 declarations
TargetScheduleContinuity.lean 9 declarations
TerminalInterior.lean 6 declarations
TerminalMarginal.lean 3 declarations
TerminalMeanCavity.lean 6 declarations
TerminalMeanField.lean 11 declarations
TerminalPiRoot.lean 2 declarations
TopologyChargeBound.lean 5 declarations
TopologyDecay.lean 10 declarations
TowerArraySplit.lean 3 declarations
TowerPadding.lean 7 declarations
TowerSum.lean 2 declarations
TowerTerminalPad.lean 3 declarations
TreeAnchor.lean 2 declarations
TreeDerivatives.lean 18 declarations
TreeMarkLaw.lean 12 declarations
TreeMeasurable.lean 3 declarations
TreeSampleProjection.lean 4 declarations
TreeSampling.lean 37 declarations
TrialPhysical.lean 4 declarations
TripleMarginal.lean 13 declarations
TwoPointLabeling.lean 2 declarations
TwoSideProjection.lean 2 declarations
UniformIndexCoupling.lean 12 declarations
UniformRootDecorrelation.lean 5 declarations
UniversalDictionary.lean 26 declarations
UpperCommonCoefficient.lean 9 declarations
UpperConditional.lean 4 declarations
UpperCountLocal.lean 1 declarations
UpperCountMean.lean 9 declarations
UpperCountState.lean 12 declarations
UpperDatum.lean 8 declarations
UpperDatumIntegral.lean 1 declarations
UpperFreshLocal.lean 8 declarations
UpperInsertion.lean 18 declarations
UpperMoments.lean 14 declarations
UpperPoissonBound.lean 1 declarations
UpperRealEndpoint.lean 8 declarations
UpperRegularized.lean 8 declarations
UpperReplicaPatterns.lean 7 declarations
UpperRootInsertion.lean 3 declarations
UpperTrial.lean 13 declarations
VariationalUpper.lean 5 declarations
VertexContinuity.lean 22 declarations
ZeroShape.lean 11 declarations