`OAI/Combinatorics/Progressions/Sampling/`

2841 declarations, 0 contain sorry, 0 declared as axioms; 340 files

Files

ActualFixedSpatialBufferedScore.lean 3 declarations
ActualFixedSpatialCenteredForecastModel.lean 12 declarations
ActualFixedSpatialSlicedForecastSourceLaw.lean 56 declarations
ActualFixedSpatialSlicedGridErrorIdentification.lean 2 declarations
ActualFixedSpatialSlicedInactiveGridCap.lean 6 declarations
ActualFixedSpatialSlicedNumericalGridCap.lean 2 declarations
ActualFixedSpatialSlicedRetainedKernelGridCap.lean 2 declarations
ActualForecastDataNativeProductBudget.lean 20 declarations
ActualForecastModelPrecision.lean 21 declarations
ActualMarkedFiniteScoreComparison.lean 6 declarations
ActualSlicedForecastLateData.lean 17 declarations
AllocatedActiveGridPlateau.lean 22 declarations
AllocatedAllGridScale.lean 4 declarations
AllocatedAnchoredDensityNativeForecastSource.lean 1 declarations
AllocatedBooleanRowsSampling.lean 3 declarations
AllocatedBufferedGridIdeal.lean 6 declarations
AllocatedClippedFullGridGlobal.lean 51 declarations
AllocatedClippedFullGridIdealCover.lean 5 declarations
AllocatedCoefficientSampler.lean 6 declarations
AllocatedCommonUniformSampling.lean 3 declarations
AllocatedDenseFiberSliceForecastGeometry.lean 5 declarations
AllocatedExternalCandidateActualShearForecastScore.lean 12 declarations
AllocatedExternalCandidateDenseForecastData.lean 5 declarations
AllocatedExternalCandidateForecastComparisonSource.lean 8 declarations
AllocatedExternalCandidateFreezingScoreBudget.lean 3 declarations
AllocatedExternalCandidateNativeFrozenScore.lean 11 declarations
AllocatedExternalCandidatePhysicalScore.lean 6 declarations
AllocatedExternalCandidateSamplerFacts.lean 3 declarations
AllocatedExternalCandidateSamplerFamily.lean 27 declarations
AllocatedExternalCandidateShearBufferedScore.lean 1 declarations
AllocatedExternalLocalGoodForecastPath.lean 39 declarations
AllocatedExternalRetainedForecastModel.lean 1 declarations
AllocatedFiniteModelGridCover.lean 1 declarations
AllocatedFiniteModelSquareSampling.lean 8 declarations
AllocatedFixedPathForecastErrorBudget.lean 23 declarations
AllocatedFixedPathRecoveredJointGridComparison.lean 18 declarations
AllocatedFixedSamplingCover.lean 1 declarations
AllocatedFixedScaleProductiveNarrowSampler.lean 2 declarations
AllocatedForecastPrimitiveCapBound.lean 7 declarations
AllocatedForecastShortRawDependence.lean 16 declarations
AllocatedFrozenGridLaw.lean 8 declarations
AllocatedFullGridChartModelMeasurable.lean 12 declarations
AllocatedFullGridCoefficientBudget.lean 11 declarations
AllocatedFullGridRecenteredCover.lean 9 declarations
AllocatedFullGridRefinedMixture.lean 3 declarations
AllocatedFullGridSeparatedRecentered.lean 2 declarations
AllocatedFullGridSiteFactors.lean 6 declarations
AllocatedFullGridSpatialWeighted.lean 9 declarations
AllocatedGridFamilyAccuracy.lean 9 declarations
AllocatedGridNaturalWindow.lean 33 declarations
AllocatedGridlessEnvelopeCap.lean 5 declarations
AllocatedGridlessProfileBound.lean 32 declarations
AllocatedGridlessWindowMajorant.lean 1 declarations
AllocatedIdealGridEnvelope.lean 12 declarations
AllocatedKernelForecastSourceDecoupling.lean 2 declarations
AllocatedLongGridCoordinates.lean 9 declarations
AllocatedLongGridIntegral.lean 23 declarations
AllocatedModularForecastRationalSource.lean 1 declarations
AllocatedNaturalGridPoint.lean 6 declarations
AllocatedOriginalCommonSampling.lean 2 declarations
AllocatedOriginalForecastSpatialIntegral.lean 11 declarations
AllocatedOriginalSampleConditionalForecastComparison.lean 1 declarations
AllocatedOriginalSampleForecastAtom.lean 25 declarations
AllocatedOriginalSampleForecastDensityRiemann.lean 4 declarations
AllocatedOriginalSampleForecastMeanRiemann.lean 23 declarations
AllocatedOriginalSampleForecastMeasurable.lean 9 declarations
AllocatedOriginalSampleJointNarrowForecast.lean 3 declarations
AllocatedPeriodicGridQuadrature.lean 23 declarations
AllocatedPhysicalDensityNativeForecastSource.lean 1 declarations
AllocatedPhysicalGridMask.lean 7 declarations
AllocatedPrimitiveSiteSampling.lean 1 declarations
AllocatedProbabilityGrid.lean 32 declarations
AllocatedProductiveRelativeScore.lean 4 declarations
AllocatedProxyMixedGrid.lean 2 declarations
AllocatedRecenteredSamplingData.lean 1 declarations
AllocatedReconstructedCutoffSampling.lean 1 declarations
AllocatedRecoveredForecastDecay.lean 10 declarations
AllocatedRecoveredNativeJointGridComparison.lean 1 declarations
AllocatedReferenceEnvelopeSampling.lean 1 declarations
AllocatedReferenceIdealSampling.lean 7 declarations
AllocatedRetainedActualForecastFactory.lean 6 declarations
AllocatedSamplerRelativeInduction.lean 11 declarations
AllocatedScalarEmptyLayerSampler.lean 1 declarations
AllocatedScalarSamplingBudget.lean 3 declarations
AllocatedScoredFreezing.lean 3 declarations
AllocatedSiteSamplingBudget.lean 10 declarations
AllocatedSlicedGridGeometryBudget.lean 17 declarations
AllocatedSlicedGridResourceBudget.lean 3 declarations
AllocatedSlicedMixedGrid.lean 1 declarations
AllocatedSlicedModularForecastContinuousSource.lean 1 declarations
AllocatedSpatialWeightedSampling.lean 1 declarations
AllocatedSupportedGridMixture.lean 1 declarations
AllocatedSupportedSlicedAmbientGrid.lean 4 declarations
AllocatedSupportedSlicedFullGridSite.lean 12 declarations
AllocatedSupportedSlicedGridMarginal.lean 8 declarations
AllocatedSupportedSlicedInactiveGridSite.lean 10 declarations
AllocatedTranslatedCutoffSampling.lean 8 declarations
AllocatedUnifiedSamplingBudget.lean 4 declarations
AllocatedUniformGeometricSampling.lean 11 declarations
AllocatedUniformGridVolumeCap.lean 24 declarations
AllocatedWeightedGridMixture.lean 9 declarations
AllocatedZeroLayerDetectionFromEmptySampler.lean 1 declarations
AllocatedZeroLayerPhysicalPatchScore.lean 3 declarations
AmbientL1SamplingBudget.lean 4 declarations
AnchoredObservationPartition.lean 1 declarations
AnchoredSamplerDomination.lean 1 declarations
AnchoredSamplerGeometry.lean 1 declarations
AveragedNormalizedTwistForecastJointModel.lean 30 declarations
BooleanProductSampler.lean 6 declarations
BooleanSamplerDivergence.lean 1 declarations
BooleanSamplerMeasurability.lean 6 declarations
BooleanSamplerPerturbation.lean 1 declarations
BoundedKernelGridEnumerationBudget.lean 12 declarations
BudgetedGridProjection.lean 2 declarations
BufferedScalarScoreBound.lean 5 declarations
BufferedScoreDiscount.lean 4 declarations
CanonicalRawSampler.lean 3 declarations
CanonicalSamplerTuple.lean 22 declarations
CeilGridScaleRatio.lean 8 declarations
CenteredNormalizedTwistForecastJointModel.lean 2 declarations
CoefficientGridRate.lean 14 declarations
CoefficientUniformPerturbationSampling.lean 8 declarations
ConjugationGridBudget.lean 1 declarations
ContainedProgressionForecastDisintegration.lean 3 declarations
ControlledIntegralGrid.lean 1 declarations
ControlledJointGrid.lean 19 declarations
CoveredJetSampler.lean 6 declarations
CoveredSamplerGlobalDensity.lean 4 declarations
CoveredSamplerHaarDensity.lean 6 declarations
CubeSamplerGoodRegion.lean 1 declarations
CyclicInteriorScore.lean 2 declarations
CyclicIntervalSampling.lean 2 declarations
CyclicSamplingMoments.lean 3 declarations
DenseSliceGridScale.lean 2 declarations
DerivativeGridPoints.lean 8 declarations
DetectedTranslationMajorSamplingContainment.lean 7 declarations
ExplicitCollisionSampler.lean 2 declarations
ExplicitSpatialSampler.lean 12 declarations
ExternalCandidateStepZeroScores.lean 1 declarations
ExternalNetMaskedScores.lean 7 declarations
FiniteLawForecastModelTransfer.lean 1 declarations
FiniteNormalizedRealGridCorrection.lean 4 declarations
FiniteObservationRetraction.lean 5 declarations
FiniteSamplingMoment.lean 13 declarations
FiniteWeightedScorePerturbation.lean 4 declarations
FixedObservationRefinement.lean 3 declarations
FixedPatchShearFiberCandidateScore.lean 8 declarations
FixedPathSlicedGridMeshBudget.lean 28 declarations
FixedSpatialKernelNativeForecastSource.lean 8 declarations
FixedSpatialKernelProgressionForecastIntegral.lean 45 declarations
FixedSpatialSliceNativeJointGridDetComparison.lean 2 declarations
ForecastActiveGridIntegralComparison.lean 24 declarations
ForecastActualBufferedNativeExpansion.lean 4 declarations
ForecastActualPhysicalSourceContinuous.lean 24 declarations
ForecastAmbientPrecision.lean 1 declarations
ForecastContinuousNormalization.lean 2 declarations
ForecastContinuousRetainedExpansion.lean 31 declarations
ForecastDensityPhysicalApproximation.lean 11 declarations
ForecastEarlyBufferRadius.lean 3 declarations
ForecastFiniteSpatialFamily.lean 2 declarations
ForecastGoodPathMeanNorm.lean 13 declarations
ForecastInactiveFiberLaw.lean 3 declarations
ForecastInactiveFixedPath.lean 2 declarations
ForecastInactiveFixedPhysical.lean 15 declarations
ForecastInactiveFixedProduct.lean 8 declarations
ForecastInactiveFixedSupport.lean 22 declarations
ForecastInactiveProduct.lean 3 declarations
ForecastInactiveShortAxis.lean 1 declarations
ForecastInactiveSlicedCappedContinuousSource.lean 12 declarations
ForecastInactiveSlicedFixedAxisCap.lean 10 declarations
ForecastInactiveSlicedFixedGridCap.lean 1 declarations
ForecastInactiveSlicedFixedPath.lean 2 declarations
ForecastInactiveSlicedFixedProduct.lean 7 declarations
ForecastInactiveSlicedFixedScalarCapBudget.lean 6 declarations
ForecastInactiveSlicedNativeSource.lean 1 declarations
ForecastInactiveSmoothSupport.lean 2 declarations
ForecastJacobianBudget.lean 5 declarations
ForecastJointScaleNormalization.lean 25 declarations
ForecastLawCenteredRecoveredKernel.lean 8 declarations
ForecastLawNativeRawJointMean.lean 17 declarations
ForecastLawOriginalNativeHaarJointMean.lean 10 declarations
ForecastLawPhysicalAmbientHaarComparison.lean 8 declarations
ForecastLawPhysicalTargetReal.lean 8 declarations
ForecastLawRecoveredRationalCardinalityCap.lean 21 declarations
ForecastModerateWeightedSite.lean 5 declarations
ForecastModularCutoff.lean 27 declarations
ForecastNativeJointTestBudget.lean 31 declarations
ForecastNativePullbackBudget.lean 52 declarations
ForecastNativeRawSpatialFamily.lean 13 declarations
ForecastNormalizedTwistExtension.lean 1 declarations
ForecastOriginalDensityRegularity.lean 3 declarations
ForecastOriginalNativeHaarJointMean.lean 6 declarations
ForecastOriginalSampleUniformBudget.lean 10 declarations
ForecastPhysicalQuarterRecovery.lean 3 declarations
ForecastPhysicalTargetReal.lean 8 declarations
ForecastPhysicalTargetSpatialSplit.lean 6 declarations
ForecastPreparedScaleBudget.lean 71 declarations
ForecastPrimitiveEnvelopes.lean 1 declarations
ForecastRawSpatialBoxReorder.lean 33 declarations
ForecastResidualExponentialBudget.lean 1 declarations
ForecastRetainedTermCount.lean 1 declarations
ForecastShortGridEquiv.lean 2 declarations
ForecastSlicedPrimitiveCutoffBudget.lean 3 declarations
FrozenMarkedRightOrbitGrid.lean 1 declarations
FrozenPartitionScore.lean 13 declarations
FullParameterJointSampler.lean 4 declarations
FullTaggedRationalChartGrid.lean 2 declarations
GridNormalizationDenominator.lean 9 declarations
GridNormalizationTransport.lean 6 declarations
IntegralGridBudget.lean 2 declarations
IntegralGridFunctional.lean 7 declarations
IntegralScoredKernel.lean 3 declarations
JointBooleanRetainedGrid.lean 1 declarations
JointCoefficientGridComparison.lean 1 declarations
JointFrozenSamplerLaw.lean 5 declarations
JointGridAccuracy.lean 7 declarations
JointMeasureProductiveNarrowSampler.lean 11 declarations
JointSamplerProductivity.lean 7 declarations
JointTupleGrid.lean 1 declarations
KernelControlledGrid.lean 1 declarations
KernelSamplerThreshold.lean 4 declarations
L1SamplingSurrogate.lean 1 declarations
LayerSamplerWitnessScale.lean 35 declarations
LocalSamplingBudget.lean 4 declarations
LocalWeightedSampling.lean 3 declarations
LowTaggedSamplingRank.lean 7 declarations
MarkedExternalKernelProjectionScoreRestoration.lean 1 declarations
MarkedKernelProjectionScoreRestoration.lean 15 declarations
MarkedKernelRationalGrid.lean 1 declarations
MeasureExceptionalBufferedScore.lean 1 declarations
MixedAssignmentSampling.lean 6 declarations
MixedGridBudget.lean 12 declarations
MixedOutputGrid.lean 18 declarations
ModelScoreComparison.lean 2 declarations
NativeGridRightDictionary.lean 5 declarations
NativeMarkedDiagramScoreLift.lean 2 declarations
NativeMarkedFreezingSliceScore.lean 3 declarations
NativeSquarefreeGrids.lean 3 declarations
NormalizedLayerScoreStep.lean 2 declarations
NormalizedRealBoxHalfGrid.lean 12 declarations
NormalizedTwistRationalForecast.lean 18 declarations
PatchKernelGridBudget.lean 14 declarations
PhysicalCoveredL1Sampling.lean 1 declarations
PhysicalGridCorrelation.lean 7 declarations
PhysicalGridCostFromLogs.lean 2 declarations
PhysicalJetTentSampling.lean 1 declarations
PhysicalRowsCoveredL1Sampling.lean 1 declarations
PhysicalRowsProbabilityMassSampling.lean 3 declarations
PivotGridBounds.lean 4 declarations
PivotGridErrorTransfer.lean 2 declarations
PositiveGridFamily.lean 37 declarations
PositivePartitionScore.lean 1 declarations
PositiveScoreComparison.lean 3 declarations
PrecenterForecastNativeAtomDictionary.lean 8 declarations
PrecenterForecastNativePartners.lean 16 declarations
PreparedActualForecastSetup.lean 35 declarations
PreparedActualSlicedForecastModelExtension.lean 2 declarations
PreparedActualSlicedForecastSetup.lean 19 declarations
PreparedCanonicalPaddedSamplerData.lean 5 declarations
PreparedCenteredForecastCramer.lean 1 declarations
PreparedCenteredForecastEarlyWidth.lean 10 declarations
PreparedCenteredForecastGoodModel.lean 3 declarations
PreparedCenteredForecastModelExtensionAnd.lean 7 declarations
PreparedCenteredForecastPathLogEnvelope.lean 9 declarations
PreparedCenteredForecastSpatialBounds.lean 4 declarations
PreparedCenteredShortForecastGoodInterface.lean 16 declarations
PreparedCenteredShortForecastProductiveGoodModel.lean 6 declarations
PreparedConcreteComparisonGridBudget.lean 9 declarations
PreparedConcreteSlicedForecastModelLogs.lean 15 declarations
PreparedConcreteSlicedForecastModelPacket.lean 2 declarations
PreparedConcreteSlicedForecastPrecision.lean 4 declarations
PreparedConcreteSlicedForecastPrimitiveCapBudget.lean 4 declarations
PreparedEarlyLateSamplerGeometry.lean 6 declarations
PreparedFiniteUniversalSlicedForecastModelExtension.lean 4 declarations
PreparedForecastPrimitiveParameters.lean 1 declarations
PreparedForecastRequiredPowerBudget.lean 21 declarations
PreparedLayerScore.lean 2 declarations
PreparedModularCanonicalDetectorSamplingBounds.lean 6 declarations
PreparedModularGeneralDetectorSamplingBounds.lean 6 declarations
PreparedProductiveGoodForecastSource.lean 10 declarations
PreparedProductiveShortGoodForecastSource.lean 2 declarations
PreparedRelativeEndpointForecastBudget.lean 5 declarations
PreparedRelativePositiveForecastSource.lean 1 declarations
PreparedShearForecastScoreBridge.lean 4 declarations
PreparedShortForecastCertificateSpecialization.lean 1 declarations
PreparedShortForecastRawSourceBounds.lean 10 declarations
PreparedShortGoodForecastSource.lean 4 declarations
PreparedSlicedForecastComparisonLogs.lean 29 declarations
PreparedSlicedForecastScalarEnvelope.lean 2 declarations
PreparedSourceSlicedForecastNumerics.lean 4 declarations
PrincipalCoefficientGridFamily.lean 1 declarations
PrincipalGridMixture.lean 5 declarations
PrincipalSamplingScale.lean 4 declarations
PrincipalZeroRationalForecast.lean 2 declarations
ProductiveCanonicalSampler.lean 1 declarations
QuantitativeKernelJointGrid.lean 3 declarations
QuarticSamplingBudget.lean 6 declarations
RationalForecastCoefficientPeriod.lean 3 declarations
RationalForecastGridTail.lean 36 declarations
RationalGridMajorSet.lean 6 declarations
RationalHomogeneousSymbolPullbackGrid.lean 5 declarations
RationalInactiveGridIntegralComparison.lean 9 declarations
RationalPowerGrid.lean 2 declarations
RationalSpanGrid.lean 50 declarations
RealAdaptedCoefficientGrid.lean 4 declarations
RealGridRationalLift.lean 3 declarations
RealGridSeparation.lean 2 declarations
RealMatrixSpecifiedGrid.lean 3 declarations
RecursivePatchScore.lean 3 declarations
RelativePatchScoreObstruction.lean 4 declarations
RelativeSliceScalarMeshScore.lean 1 declarations
SamplerParameterLog.lean 3 declarations
SamplerSeparatedVariables.lean 7 declarations
SamplingLowTaggedSamplingRank.lean 7 declarations
SamplingRankProjectedContainment.lean 30 declarations
ScalarCubeGridCoordinates.lean 4 declarations
ScalarFunctionalCoefficientGrid.lean 3 declarations
ScalarSymbolFamilyCoefficientGrid.lean 3 declarations
ScoredPatchDensityStep.lean 2 declarations
SelectedPhysicalGridBudget.lean 1 declarations
SelectedSamplerNormalization.lean 5 declarations
SharedWidthPreparedFiniteSlicedForecastModelFromPrepared.lean 5 declarations
SharedWidthPreparedProductiveShortGoodForecastSource.lean 9 declarations
SharedWidthPreparedShortForecastProductiveModelAttachment.lean 3 declarations
SharedWidthPreparedShortForecastSourceModelAttachment.lean 13 declarations
ShiftedSmoothFiniteGridLaw.lean 16 declarations
SmallKernelSamplerThreshold.lean 4 declarations
SmoothPairPhysicalGrid.lean 7 declarations
SmoothSplitSampling.lean 26 declarations
SpatialGridVolume.lean 2 declarations
SpatialSamplingSize.lean 2 declarations
SquareSamplingAccuracy.lean 2 declarations
StagedForecastResidualBudget.lean 3 declarations
SupportedQuotientExactGrid.lean 3 declarations
TranslatedPartialPeriodicGridIntegrability.lean 5 declarations
TranslatedSamplerDomination.lean 1 declarations
TranslationLogCoordinateInputGrid.lean 12 declarations
WeightedCubeGridDensity.lean 5 declarations
WeightedTranslationProjectionGridBudget.lean 5 declarations
WeightedUniformGridDensity.lean 8 declarations