`OAI/Combinatorics/Progressions/Probability/`

2445 declarations, 0 contain sorry, 0 declared as axioms; 329 files

Files

ActualFixedSpatialSlicedDensityBounds.lean 6 declarations
ActualFixedSpatialSlicedDensityIdentification.lean 3 declarations
ActualFixedSpatialSlicedNumericalDensity.lean 9 declarations
ActualFixedSpatialUnchargedDensity.lean 7 declarations
AdaptiveCouplingComparison.lean 12 declarations
AllocatedAccuracyReferenceMass.lean 6 declarations
AllocatedActiveAxisSourceLaw.lean 25 declarations
AllocatedAmbientDensity.lean 2 declarations
AllocatedAmbientProjectedDensityMultiple.lean 4 declarations
AllocatedAnisotropicDensityComparison.lean 1 declarations
AllocatedAnisotropicSpatialLaw.lean 5 declarations
AllocatedCanonicalSlicedProbabilitySource.lean 3 declarations
AllocatedCenteredReferenceMassTransfer.lean 2 declarations
AllocatedChartDensityRadius.lean 1 declarations
AllocatedConditionalSampledError.lean 4 declarations
AllocatedDensityParameterBounds.lean 28 declarations
AllocatedDensitySourceFamily.lean 3 declarations
AllocatedEarlyCoverCoefficientMass.lean 18 declarations
AllocatedEarlyNormalizedMixture.lean 1 declarations
AllocatedEarlyScaledMixture.lean 2 declarations
AllocatedEmptyLayerLaw.lean 4 declarations
AllocatedErrorSampledMass.lean 8 declarations
AllocatedExternalCandidateAllKeptSliceLaw.lean 7 declarations
AllocatedExternalCandidateAllSiteLaw.lean 20 declarations
AllocatedExternalCandidateFixedLawSpatialFamily.lean 1 declarations
AllocatedExternalCandidateFrozenStageDensity.lean 2 declarations
AllocatedExternalCandidateRetainedSliceLaw.lean 17 declarations
AllocatedExternalLocalSliceLaw.lean 18 declarations
AllocatedFiberSlicedSourceLaw.lean 2 declarations
AllocatedFixedPathSlicedPhysicalDensityComparison.lean 4 declarations
AllocatedFixedPathSlicedRationalDensityComparison.lean 9 declarations
AllocatedFixedPositiveDensity.lean 10 declarations
AllocatedFixedReferenceMass.lean 7 declarations
AllocatedFrozenJetDensity.lean 21 declarations
AllocatedFullBoxPositiveLaw.lean 2 declarations
AllocatedGlobalMaskedDensity.lean 3 declarations
AllocatedIdealCoefficientMass.lean 2 declarations
AllocatedIdealDensitySourceFamily.lean 2 declarations
AllocatedJointAmbientDensity.lean 3 declarations
AllocatedJointMaskedDensityComparison.lean 18 declarations
AllocatedLongIntegralMass.lean 12 declarations
AllocatedLongJetMixture.lean 17 declarations
AllocatedMaskedCoefficientHaarLaw.lean 4 declarations
AllocatedMassTupleComparison.lean 12 declarations
AllocatedMixedIdealErrorMass.lean 2 declarations
AllocatedMixedLiftNormalizedMass.lean 10 declarations
AllocatedNarrowSpatialLaw.lean 5 declarations
AllocatedNormalizedConditionalHaar.lean 10 declarations
AllocatedNormalizedConstructedMixture.lean 1 declarations
AllocatedNormalizedCutoffMass.lean 1 declarations
AllocatedPhysicalCoveredDensity.lean 5 declarations
AllocatedPhysicalExpansionMass.lean 2 declarations
AllocatedPhysicalPointMixture.lean 3 declarations
AllocatedPlateauPointMixture.lean 10 declarations
AllocatedPrescribedRefinedDensity.lean 18 declarations
AllocatedProbabilityMajorantMass.lean 16 declarations
AllocatedProbabilityProfileMass.lean 6 declarations
AllocatedProbabilityWindowMesh.lean 17 declarations
AllocatedProductCutoffMass.lean 6 declarations
AllocatedProfileErrorSampledMass.lean 3 declarations
AllocatedProgressionDensityIdentity.lean 10 declarations
AllocatedRecenteredActualMass.lean 3 declarations
AllocatedRecenteredDensityMass.lean 7 declarations
AllocatedRecenteredSampledMass.lean 1 declarations
AllocatedRecenteredSeparatedMass.lean 3 declarations
AllocatedReconstructedCutoffMass.lean 2 declarations
AllocatedRecoveredChartMass.lean 7 declarations
AllocatedReferenceBufferMass.lean 4 declarations
AllocatedReferenceCoefficientMass.lean 1 declarations
AllocatedReferenceJetMass.lean 14 declarations
AllocatedRefinedCoefficientMass.lean 9 declarations
AllocatedRefinedCoverMixture.lean 1 declarations
AllocatedScaledSpatialMixture.lean 5 declarations
AllocatedSiteBufferSampledMass.lean 1 declarations
AllocatedSiteEnvelopeMass.lean 3 declarations
AllocatedSiteWindowProbability.lean 2 declarations
AllocatedSlicedCoveredExpectation.lean 2 declarations
AllocatedSlicedIdealDensity.lean 24 declarations
AllocatedSlicedProxyLaw.lean 9 declarations
AllocatedSpatialCoefficientReferenceLaw.lean 3 declarations
AllocatedSpatialLawDensity.lean 1 declarations
AllocatedSpatialMixture.lean 1 declarations
AllocatedSupportedRecenteringLaw.lean 1 declarations
AllocatedTailDensityComparison.lean 1 declarations
AllocatedWholeDeckLaw.lean 10 declarations
AllocatedWindowProbability.lean 4 declarations
AllocatedZeroLayerInitializationMassLoss.lean 2 declarations
AllocatedZeroLayerLaw.lean 4 declarations
AmbientTentMass.lean 4 declarations
AnchoredCoefficientDensityMass.lean 1 declarations
AnchoredMixtureBoxTail.lean 18 declarations
AnchoredOneSiteDensityComparison.lean 1 declarations
AnisotropicCanonicalDensity.lean 15 declarations
AnisotropicSmoothPairLaw.lean 21 declarations
AnisotropicSpatialLaw.lean 7 declarations
AuxiliaryBoxLaws.lean 6 declarations
AveragedJointImageLaw.lean 5 declarations
BSGDensity.lean 7 declarations
BaseAndCenterMixedLaw.lean 3 declarations
BinaryDensity.lean 7 declarations
BlockCubeDensity.lean 6 declarations
BooleanCubeGoodMass.lean 1 declarations
BooleanJetMassBudget.lean 3 declarations
BoundedSmoothTestDensity.lean 2 declarations
BoxCokernelProbability.lean 2 declarations
CandidateDetectionMassBudget.lean 1 declarations
CandidateFrontFactorMassBlockBudget.lean 4 declarations
CanonicalConstantDensityBound.lean 3 declarations
CanonicalCoverLaw.lean 14 declarations
CanonicalPairPointLaw.lean 3 declarations
CanonicalScalarFamilyMass.lean 2 declarations
CanonicalZeroSpatialDensity.lean 11 declarations
CanonicalZeroSpatialInputLaw.lean 9 declarations
CenteredPhysicalProductLaw.lean 3 declarations
CoefficientAmbientDensity.lean 5 declarations
CoefficientDeckDensityLawCongruence.lean 11 declarations
CoefficientDensityAverage.lean 1 declarations
CoefficientDensitySplit.lean 7 declarations
CoefficientJetDensityFactors.lean 32 declarations
CoefficientMajorantMassBudget.lean 3 declarations
CoefficientProductLaw.lean 6 declarations
CommonSectionAmbientDensityMultiple.lean 17 declarations
CommonSectionEuclideanDensity.lean 2 declarations
ComparableUnconditionedScalarFamilyDensity.lean 3 declarations
ComparableUnconditionedScalarProductiveFamilyDensity.lean 3 declarations
ComplexDensityScaledQuadrature.lean 2 declarations
ComplexPartitionMixture.lean 3 declarations
ConditionalCoordinateExceptions.lean 4 declarations
ConditionalWindowIntegral.lean 2 declarations
ConstantDensityBudget.lean 4 declarations
ContainedProgressionCubeLaw.lean 9 declarations
ContainedProgressionJetSourceLaw.lean 3 declarations
ContainedSupportedProgressionJetLaw.lean 5 declarations
CorrelatedModeratePointMass.lean 4 declarations
CouplingOneSidedTruncation.lean 2 declarations
CoveredPhysicalDensityComparison.lean 1 declarations
CubeMinorProbability.lean 2 declarations
CubeMixtureNativeDetection.lean 1 declarations
CubeMixtureVertex.lean 2 declarations
CylinderJointMass.lean 32 declarations
CylinderUniformMass.lean 2 declarations
DenseProductDensity.lean 1 declarations
DensityBoundFromInvariant.lean 2 declarations
DensityComparisonComposition.lean 3 declarations
DensityIntegralBound.lean 2 declarations
DensityMixtureAELaw.lean 33 declarations
DensityNormalization.lean 4 declarations
DensityNormalizationScales.lean 4 declarations
DensityTestParameter.lean 4 declarations
DiagonalDensityTransport.lean 21 declarations
DiagonalImageDensity.lean 38 declarations
DifferenceEventProbability.lean 7 declarations
EmptyCoefficientDensity.lean 22 declarations
EuclideanDerivativeDensityCovolume.lean 1 declarations
EuclideanJetDensity.lean 1 declarations
ExactPhysicalMixtureNativePartner.lean 1 declarations
FiniteArrayMeasure.lean 4 declarations
FiniteBoxDensityComparison.lean 1 declarations
FiniteConditionedMass.lean 21 declarations
FiniteCountDensityError.lean 4 declarations
FiniteCubeBlockLaw.lean 4 declarations
FiniteDensityConjugate.lean 1 declarations
FiniteDensityMassBound.lean 16 declarations
FiniteExcessMassCap.lean 7 declarations
FiniteFiberDensity.lean 5 declarations
FiniteFiberLawSupport.lean 1 declarations
FiniteMassErrorSelection.lean 1 declarations
FinitePairProbability.lean 1 declarations
FinitePointMassLp.lean 3 declarations
FiniteProbabilityLipschitz.lean 23 declarations
FiniteProbabilityMeanConjugate.lean 1 declarations
FiniteProbabilityUniformResidualGood.lean 3 declarations
FiniteProductMass.lean 2 declarations
FiniteProductMassBound.lean 1 declarations
FiniteProductPointMass.lean 1 declarations
FiniteProductWitnessProbability.lean 2 declarations
FiniteRelativeDensity.lean 4 declarations
FiniteSectionWeightMass.lean 2 declarations
FiniteSpatialReferenceMass.lean 2 declarations
FixedSpatialDensityBudget.lean 2 declarations
FullFrozenChartMass.lean 2 declarations
FullScalarCubeWindowLaw.lean 3 declarations
GenericProbabilityProductMapIntegral.lean 5 declarations
GenericSampleExpectation.lean 4 declarations
GeometricSelectedMass.lean 2 declarations
InactivePrincipalLaw.lean 8 declarations
IndependentEmbeddedMixture.lean 8 declarations
IntervalDivisorProbability.lean 34 declarations
JointBooleanCutoffLaw.lean 11 declarations
JointDensityConstantSubtraction.lean 2 declarations
JointProductiveMeasure.lean 24 declarations
LargeCokernelProbability.lean 5 declarations
LargeDivisorPairProbability.lean 3 declarations
LocalLayerOneSiteLaw.lean 13 declarations
LowDensityAmplification.lean 10 declarations
LowJetDensity.lean 1 declarations
LowerMassWeightNormalization.lean 3 declarations
MaskedDensityTranslation.lean 3 declarations
MassBoundedShearBudget.lean 1 declarations
MassConvolution.lean 16 declarations
MeasureExceptionalModeledPatchTransfer.lean 1 declarations
MeasureGoodAtomTransfer.lean 9 declarations
MixedCoveredAbsoluteMass.lean 4 declarations
MixedCoveredDensityMass.lean 5 declarations
MixedDensityInterpolation.lean 15 declarations
MixedMassLogBudget.lean 3 declarations
MixedSelectedCoefficientProbability.lean 13 declarations
NativeSliceLawVerticalPartners.lean 1 declarations
NormalizedCoveredDensity.lean 4 declarations
NormalizedDensityL1.lean 2 declarations
NormalizedExpectationWeights.lean 4 declarations
NormalizedJetDensityL1.lean 4 declarations
NormalizedJetDensitySupport.lean 8 declarations
ObservedDensityTesting.lean 24 declarations
ObservedProductDensity.lean 43 declarations
OneCubePairLaw.lean 7 declarations
OneCubeSlicedSourceLaw.lean 7 declarations
OneSiteDensityTestedError.lean 1 declarations
OrthonormalMixedLaw.lean 6 declarations
PMFPointMassMixture.lean 12 declarations
PairedProductDensity.lean 47 declarations
PairedProductLaw.lean 2 declarations
PartitionedProfileMassComparison.lean 11 declarations
PartitionedSlicedDensityComparison.lean 3 declarations
PerturbationCoefficientLaw.lean 3 declarations
PhysicalDensityNormalization.lean 10 declarations
PhysicalRowsDensityTransport.lean 2 declarations
PivotDensityCap.lean 3 declarations
PivotDensitySupport.lean 8 declarations
PositiveDensityNormalization.lean 28 declarations
PositiveDensityRetained.lean 12 declarations
PreparedCenteredProbabilityBadProduct.lean 1 declarations
PreparedCenteredShortProbabilityBadProduct.lean 1 declarations
PreparedCommonRadiusDensityCapNested.lean 7 declarations
PreparedFullChartConditionalNativeDetectionSharedWidth.lean 3 declarations
PreparedGeometryConditionalExcess.lean 1 declarations
PreparedModularGeneralCenteredLaw.lean 33 declarations
PreparedReadyNormalizationMassBudget.lean 8 declarations
PrincipalCoefficientLaw.lean 7 declarations
PrincipalMixedMassBound.lean 15 declarations
PrincipalSupportedJointLaw.lean 2 declarations
PrincipalSupportedUnitBlockLaw.lean 1 declarations
PrincipalTestMixture.lean 1 declarations
ProbabilityIntegralApproximation.lean 1 declarations
ProbabilityIntegralThresholdPoint.lean 2 declarations
ProductCoefficientSiteLaw.lean 1 declarations
ProductDensityRepresentative.lean 6 declarations
ProductEmbeddingConditional.lean 2 declarations
ProductMixedLaws.lean 1 declarations
ProductSliceAxisDensity.lean 2 declarations
ProgressionPartitionDensity.lean 1 declarations
RandomCoefficientMassComparison.lean 7 declarations
RawSourceDensityTransfer.lean 1 declarations
RawSourceLaw.lean 9 declarations
RawWeightCellMixture.lean 4 declarations
RealificationRationalDensity.lean 4 declarations
RecoveredChartMassEarlyPower.lean 1 declarations
RecoveredChartMassLogBounds.lean 3 declarations
RectangleDensity.lean 1 declarations
RecursiveDensityDiscount.lean 3 declarations
ReferenceJetPositiveMass.lean 2 declarations
RefinedSliceLaws.lean 5 declarations
RegularizedSigmaDensity.lean 20 declarations
RelativeFullSliceLaw.lean 9 declarations
RelativeRetainedLawTransport.lean 29 declarations
RelativeSliceFiniteLaw.lean 9 declarations
RelativeSliceParameterCellLaw.lean 7 declarations
RelativeSourceDensityParameter.lean 35 declarations
RestrictedComplexChartDensityComparison.lean 24 declarations
RestrictedWeightedLawModeledTransfer.lean 6 declarations
RetainedDensityNestedTest.lean 1 declarations
RetainedGroupedDensity.lean 1 declarations
RetainedJointUnitLaw.lean 3 declarations
RetainedWeightedDensityTest.lean 3 declarations
RoundedModelDensityBudget.lean 4 declarations
SampledWeightCellLaw.lean 29 declarations
SampledWeightedMixtureError.lean 2 declarations
ScalarCubeBoundaryMass.lean 15 declarations
ScalarCubeDensityBudget.lean 5 declarations
ScalarCubeDomainDensity.lean 7 declarations
ScalarCubeHistogramMeasure.lean 13 declarations
ScalarCubeWeightMassComparison.lean 4 declarations
ScalarCubeWindowLaw.lean 9 declarations
ScalarTupleSpatialMixture.lean 1 declarations
ScaledArrayLaw.lean 35 declarations
ScaledCoefficientLaw.lean 11 declarations
ScaledCubeProductMeasure.lean 29 declarations
ScaledInputProbability.lean 6 declarations
SelectedDensityNormalization.lean 10 declarations
SelectedDensityNormalizedTwistRoot.lean 11 declarations
SelectedDensityTestMass.lean 1 declarations
SelectedDependentMeasure.lean 5 declarations
SelectedSingletonSmoothIndexLaw.lean 4 declarations
ShiftedProductCoordinateLaw.lean 23 declarations
ShiftedSmoothLawBounds.lean 4 declarations
ShiftedSmoothProductLaw.lean 8 declarations
SiftingDensityBudget.lean 3 declarations
SigmaFiniteProductMeasure.lean 1 declarations
SigmaProductMeasure.lean 1 declarations
SiteDensityRestriction.lean 3 declarations
SlicedDensityBudget.lean 2 declarations
SlicedPairDensity.lean 6 declarations
SlicedRemainderDensityFamily.lean 66 declarations
SmallTensorDensityError.lean 2 declarations
SmoothModerateBlockLaw.lean 11 declarations
SmoothProbabilityProfile.lean 13 declarations
SmoothSelectedSpatialLaw.lean 4 declarations
SmoothSpatialProbability.lean 5 declarations
SmoothSpatialSiteMixture.lean 1 declarations
SmoothVectorSpatialLaw.lean 3 declarations
SourceOrderImageLaw.lean 2 declarations
SpatialProductDensity.lean 40 declarations
StableSiteDensityBounds.lean 2 declarations
SupportedRecoveredChartMassEarlyPower.lean 2 declarations
SymmetricCubeMeasure.lean 6 declarations
TranslatedMixtureL1.lean 14 declarations
TranslatedSelectedDensityCap.lean 5 declarations
TranslatedSelectedOneSiteLaw.lean 1 declarations
TranslatedWeightedCubeLaw.lean 6 declarations
UniformHomExpectation.lean 6 declarations
UniformImageLawCongruence.lean 3 declarations
UniformSelectedCoefficientProductLaw.lean 22 declarations
WeightedCoefficientDensityApproximation.lean 1 declarations
WeightedFundamentalMass.lean 2 declarations
WeightedModeratePointMass.lean 7 declarations
WeightedPlateauMixture.lean 13 declarations
WeightedPotentialMass.lean 3 declarations
WeightedSliceFamilyLaw.lean 22 declarations
WeightedSupportedComplexMixture.lean 8 declarations