`OAI/Combinatorics/Progressions/Estimates/`

16648 declarations, 0 contain sorry, 0 declared as axioms; 1561 files

Files

AbsorbedSiteTests.lean 4 declarations
ActiveAveragedProfileComparison.lean 32 declarations
ActiveProfileNoise.lean 48 declarations
ActiveProfileProduct.lean 6 declarations
ActiveScaledIdealRegularity.lean 2 declarations
ActiveTailSlicedProfileComparison.lean 2 declarations
ActualFiberSlicedBoundedTwistPrecision.lean 14 declarations
AdaptedAnchoredComparison.lean 4 declarations
AdaptedDiagramNativeExternalNet.lean 11 declarations
AdaptedMarkedMapHeight.lean 3 declarations
AdaptedTranslation.lean 2 declarations
AdaptiveRatioNormalization.lean 5 declarations
AlgebraicMajorUniformExponent.lean 1 declarations
AllocatedActiveContainedTupleMap.lean 4 declarations
AllocatedActivePlateauAverage.lean 11 declarations
AllocatedActiveSiteAverage.lean 1 declarations
AllocatedActualHaarComparison.lean 6 declarations
AllocatedActualNormalizedTupleComparison.lean 10 declarations
AllocatedActualNormalizedTupleStatement.lean 5 declarations
AllocatedActualProfileAccuracy.lean 2 declarations
AllocatedActualProfileControl.lean 15 declarations
AllocatedActualRationalMarginal.lean 2 declarations
AllocatedAmbientLogBounds.lean 15 declarations
AllocatedAnchoredRecoveredSource.lean 18 declarations
AllocatedApproximationError.lean 1 declarations
AllocatedBooleanMinor.lean 4 declarations
AllocatedBufferedAmbientCutoff.lean 5 declarations
AllocatedBufferedPhysicalFactorization.lean 5 declarations
AllocatedBufferedSiteTwist.lean 4 declarations
AllocatedCandidateCommonFastGeometry.lean 15 declarations
AllocatedCandidateForwardControlledTerminal.lean 2 declarations
AllocatedCandidateGeneratedFastTerminal.lean 18 declarations
AllocatedCandidateInnerSourceGain.lean 3 declarations
AllocatedCandidateStageDataConstruction.lean 7 declarations
AllocatedCandidateTerminalNextWork.lean 8 declarations
AllocatedCandidateZeroRestrictedNativeCommonPhysicalTerminal.lean 1 declarations
AllocatedCandidateZeroRestrictedNativeCommonTerminal.lean 9 declarations
AllocatedCanonicalNormalizer.lean 25 declarations
AllocatedCanonicalPeriodPrimitiveBounds.lean 3 declarations
AllocatedCanonicalProjectedNativeSource.lean 4 declarations
AllocatedCanonicalSliceConstructedFiniteSource.lean 2 declarations
AllocatedCanonicalSliceConstructedModelSource.lean 3 declarations
AllocatedCanonicalSliceHaar.lean 1 declarations
AllocatedCanonicalSourceExistence.lean 13 declarations
AllocatedCanonicalUniformCoarseSource.lean 6 declarations
AllocatedCenteredJointComparison.lean 2 declarations
AllocatedCenteredJointProductivity.lean 2 declarations
AllocatedCenteredJointSource.lean 10 declarations
AllocatedCenteredJointStatement.lean 5 declarations
AllocatedCenteredMeasurableBadTail.lean 3 declarations
AllocatedCenteredNarrowAmplitudeNormalization.lean 2 declarations
AllocatedCenteredNarrowPrescribedMarginal.lean 10 declarations
AllocatedChosenFunctionalCoarsening.lean 9 declarations
AllocatedChosenIdealComparison.lean 1 declarations
AllocatedChosenOriginalIdealAt.lean 7 declarations
AllocatedCoarseGenuineSource.lean 13 declarations
AllocatedCommonCoarsePartition.lean 2 declarations
AllocatedCommonCover.lean 23 declarations
AllocatedCommonFrozenSymbolFactors.lean 2 declarations
AllocatedCommonWeightedOriginal.lean 15 declarations
AllocatedComparisonScale.lean 6 declarations
AllocatedCompatibleSourceGrowth.lean 1 declarations
AllocatedConstructedCommonModulus.lean 2 declarations
AllocatedContinuousProxyAveraging.lean 8 declarations
AllocatedControlledApproximation.lean 2 declarations
AllocatedControlledFrozenPullbacks.lean 1 declarations
AllocatedCorrelatedModeratePlateau.lean 12 declarations
AllocatedCorrelatedModerateSites.lean 3 declarations
AllocatedCoverLogBounds.lean 24 declarations
AllocatedCoveredActualProfile.lean 1 declarations
AllocatedCoveredFixedTest.lean 20 declarations
AllocatedCoveredHaarTransfer.lean 6 declarations
AllocatedCoveredSiteBuffer.lean 9 declarations
AllocatedCoveredSiteExpansion.lean 26 declarations
AllocatedCutoffCoveredEnvelope.lean 12 declarations
AllocatedCutoffMaskedIdeal.lean 4 declarations
AllocatedCutoffReferenceEnvelope.lean 1 declarations
AllocatedDetectedCanonicalPeriod.lean 10 declarations
AllocatedEarlyCoarseWindowSelection.lean 1 declarations
AllocatedEarlyConstructedIdeal.lean 1 declarations
AllocatedEarlyGenuineError.lean 4 declarations
AllocatedEarlyGenuineSource.lean 1 declarations
AllocatedEarlyWindowVolume.lean 5 declarations
AllocatedEnormousProfiles.lean 68 declarations
AllocatedErrorInterpolation.lean 5 declarations
AllocatedExternalCandidateAdaptedOptionQuotientFactors.lean 33 declarations
AllocatedExternalCandidateAxisFreezingConclusion.lean 62 declarations
AllocatedExternalCandidateBoundedTwistComparison.lean 2 declarations
AllocatedExternalCandidateCoveredFamilySuccessor.lean 10 declarations
AllocatedExternalCandidateDenseSliceInput.lean 5 declarations
AllocatedExternalCandidateFiniteFreezingDictionaryProducer.lean 6 declarations
AllocatedExternalCandidateFixedCenterExcess.lean 1 declarations
AllocatedExternalCandidateFrozenNativeFactors.lean 29 declarations
AllocatedExternalCandidateGeneratedCoveredFamilySuccessor.lean 1 declarations
AllocatedExternalCandidateGeneratedFreezingSuccessor.lean 14 declarations
AllocatedExternalCandidateKeptSymbolFactors.lean 11 declarations
AllocatedExternalCandidateLocalFixedCenterFront.lean 11 declarations
AllocatedExternalCandidateObservableRestriction.lean 2 declarations
AllocatedExternalCandidateOptionJointConclusion.lean 53 declarations
AllocatedExternalCandidatePrecenterNativePartners.lean 3 declarations
AllocatedExternalCandidatePreparedPhysicalConclusion.lean 7 declarations
AllocatedExternalCandidatePrimitiveFrontDescentData.lean 37 declarations
AllocatedExternalCandidateRealThreshold.lean 9 declarations
AllocatedExternalCandidateRecursiveParameter.lean 1 declarations
AllocatedExternalCandidateRefinedQuotientAssembly.lean 1 declarations
AllocatedExternalCandidateRefinementLabels.lean 23 declarations
AllocatedExternalCandidateRoundedThresholdSuccessor.lean 1 declarations
AllocatedExternalCandidateSelectedDescentRegularity.lean 5 declarations
AllocatedExternalCandidateShearBufferedModel.lean 1 declarations
AllocatedExternalCandidateStepZero.lean 2 declarations
AllocatedExternalCandidateTaggedPairFamily.lean 48 declarations
AllocatedExternalCandidateTaggedPairLongUniformFactors.lean 9 declarations
AllocatedExternalCandidateTaggedPairUniformFactors.lean 24 declarations
AllocatedExternalCandidateTaggedSourceEvaluation.lean 5 declarations
AllocatedExternalCandidateThresholdSuccessor.lean 13 declarations
AllocatedExternalCandidateUniformSuccessor.lean 4 declarations
AllocatedExternalLocalFiniteFreezing.lean 6 declarations
AllocatedExternalLocalGlobalMarkedCandidate.lean 9 declarations
AllocatedExternalRetainedResidual.lean 35 declarations
AllocatedFiberCap.lean 35 declarations
AllocatedFiniteCoefficientComparisonWithCutoff.lean 1 declarations
AllocatedFiniteCoefficientL1.lean 5 declarations
AllocatedFiniteModelNativePartner.lean 8 declarations
AllocatedFiniteModelPhysicalExpansion.lean 14 declarations
AllocatedFiniteProxyRegularity.lean 1 declarations
AllocatedFittingCoverFamily.lean 5 declarations
AllocatedFixedCommonCover.lean 19 declarations
AllocatedFixedInitializedCover.lean 1 declarations
AllocatedFixedPositiveComparison.lean 1 declarations
AllocatedFixedProductComparison.lean 1 declarations
AllocatedFixedScaleJointMarginal.lean 10 declarations
AllocatedFixedScaleJointMarginalTransfer.lean 4 declarations
AllocatedFlexibleOriginalMesh.lean 17 declarations
AllocatedFrozenBlockPMF.lean 3 declarations
AllocatedFrozenMarkedPhysicalBounds.lean 1 declarations
AllocatedFrozenPrefixStageData.lean 21 declarations
AllocatedFrozenTaggedTwistStepDrop.lean 6 declarations
AllocatedFrozenTupleGrouping.lean 5 declarations
AllocatedFullAmbientSiteFactor.lean 10 declarations
AllocatedFullSiteRadius.lean 12 declarations
AllocatedGenuineCoverFromRaw.lean 16 declarations
AllocatedGenuineNativePartner.lean 7 declarations
AllocatedGenuineSourceComparison.lean 1 declarations
AllocatedGlobalProfileMajorant.lean 5 declarations
AllocatedGoodPartCoverAverage.lean 3 declarations
AllocatedIdealComparisonAssembly.lean 8 declarations
AllocatedIdealPhysicalCover.lean 25 declarations
AllocatedIdealReferenceInsertion.lean 23 declarations
AllocatedIdealReferenceTail.lean 8 declarations
AllocatedIdealRefinedPointwise.lean 21 declarations
AllocatedIdealSiteReconstruction.lean 2 declarations
AllocatedInactiveJointSite.lean 6 declarations
AllocatedInactiveNaturalCases.lean 3 declarations
AllocatedInactiveNaturalPlateau.lean 3 declarations
AllocatedInactiveNaturalShort.lean 6 declarations
AllocatedInactivePointCap.lean 4 declarations
AllocatedInactiveSiteCases.lean 2 declarations
AllocatedInitializedIdealCover.lean 1 declarations
AllocatedIntegratedGlobalIdeal.lean 1 declarations
AllocatedJetRootAllowance.lean 6 declarations
AllocatedJointPointApproximation.lean 1 declarations
AllocatedJointRationalReference.lean 3 declarations
AllocatedJointWindowIntegral.lean 19 declarations
AllocatedLongMixedCoefficientBound.lean 6 declarations
AllocatedMarkedDictionaryRecovery.lean 19 declarations
AllocatedMaskedCoefficientSampleAE.lean 6 declarations
AllocatedMaskedFactorBounds.lean 11 declarations
AllocatedMaskedProfileCap.lean 2 declarations
AllocatedMixedJointSite.lean 1 declarations
AllocatedModelCoefficientCover.lean 3 declarations
AllocatedNarrowJointCollision.lean 3 declarations
AllocatedNarrowPrincipalMeanComparison.lean 1 declarations
AllocatedNarrowReferenceTest.lean 3 declarations
AllocatedNaturalFullSiteScale.lean 5 declarations
AllocatedNormalizedCoefficientBounds.lean 4 declarations
AllocatedNormalizedIdealCover.lean 2 declarations
AllocatedNormalizedProductCover.lean 1 declarations
AllocatedNormalizedRefinedData.lean 8 declarations
AllocatedNormalizedScaleChoice.lean 5 declarations
AllocatedNormalizedSiteTwist.lean 3 declarations
AllocatedNormalizedSourceComparison.lean 1 declarations
AllocatedOrdinaryLongPhysicalTerminalConclusion.lean 15 declarations
AllocatedOriginalAmbientSelected.lean 5 declarations
AllocatedOriginalAmbientSelectedAt.lean 4 declarations
AllocatedOriginalCommonGenuine.lean 1 declarations
AllocatedOriginalCommonResources.lean 14 declarations
AllocatedOriginalCubeSelection.lean 1 declarations
AllocatedOriginalEarlyRawCover.lean 4 declarations
AllocatedOriginalExponentialCover.lean 11 declarations
AllocatedOriginalPrescribedMesh.lean 8 declarations
AllocatedOriginalSampleCongruenceOutput.lean 4 declarations
AllocatedOriginalSampleFullSliceLipschitz.lean 11 declarations
AllocatedOriginalSampleInactiveRead.lean 2 declarations
AllocatedOriginalSampleNormalizedTwist.lean 1 declarations
AllocatedOriginalSampleQuadratureUniformBounds.lean 28 declarations
AllocatedOriginalSampleSlicedPerturbedRiemann.lean 2 declarations
AllocatedOriginalSelected.lean 2 declarations
AllocatedOriginalWholeSiteSelected.lean 6 declarations
AllocatedPaddedRecoveredPreparedFreeze.lean 1 declarations
AllocatedPartitionedProfileJet.lean 9 declarations
AllocatedPeriodicAmbientSiteExpansion.lean 20 declarations
AllocatedPhysicalLongIdealCap.lean 31 declarations
AllocatedPhysicalLongImage.lean 17 declarations
AllocatedPlateauSiteApproximation.lean 8 declarations
AllocatedPrescribedCoveredComparison.lean 1 declarations
AllocatedPrimitiveFrontInitialLong.lean 13 declarations
AllocatedPrimitiveProfileCoarsening.lean 1 declarations
AllocatedPrincipalSourceScale.lean 2 declarations
AllocatedProductCoarseSourceAssembly.lean 1 declarations
AllocatedProductCutoffEnvelope.lean 12 declarations
AllocatedProductEarlyCoarsening.lean 2 declarations
AllocatedProductIdealCutoff.lean 12 declarations
AllocatedProductPrefactorMasks.lean 11 declarations
AllocatedProductPrefactorMeasurable.lean 2 declarations
AllocatedProductRawCoverData.lean 3 declarations
AllocatedProductSeparatedRawData.lean 10 declarations
AllocatedProductSourceAssembly.lean 1 declarations
AllocatedProductSourceCover.lean 10 declarations
AllocatedProductUniformContract.lean 1 declarations
AllocatedProductiveFrozenMajorDetection.lean 2 declarations
AllocatedProductivePaddedRelativeInitialization.lean 5 declarations
AllocatedProfileDimensions.lean 54 declarations
AllocatedProfileErrorLogBounds.lean 7 declarations
AllocatedProfileErrorMajorant.lean 6 declarations
AllocatedProjectedAmbientLogBounds.lean 3 declarations
AllocatedProjectedChosenComparison.lean 3 declarations
AllocatedProjectedFiniteModelSource.lean 2 declarations
AllocatedProjectedNormalizedComparison.lean 1 declarations
AllocatedProjectedReferenceData.lean 1 declarations
AllocatedProxyAccuracy.lean 12 declarations
AllocatedProxyL1Averaging.lean 2 declarations
AllocatedProxyOutputBounds.lean 2 declarations
AllocatedRecenteredIdealError.lean 22 declarations
AllocatedRecenteredL1Source.lean 10 declarations
AllocatedRecenteredProfileComparison.lean 1 declarations
AllocatedRecenteredProfileError.lean 2 declarations
AllocatedRecenteredSampledSource.lean 1 declarations
AllocatedRecenteredSquarePerturbation.lean 1 declarations
AllocatedRecoveredPreparedFreeze.lean 15 declarations
AllocatedRecoveredRelativeChild.lean 1 declarations
AllocatedReferenceErrorWindowBound.lean 1 declarations
AllocatedReferenceJetWindow.lean 19 declarations
AllocatedReferencePrescribeData.lean 14 declarations
AllocatedReferenceUniformError.lean 1 declarations
AllocatedReferenceWindowTest.lean 10 declarations
AllocatedRefinedCoverError.lean 8 declarations
AllocatedRefinedJointTolerance.lean 7 declarations
AllocatedRefinedLongJetComparison.lean 11 declarations
AllocatedRefinedWholeReference.lean 5 declarations
AllocatedRelativeChildSliceGeometry.lean 47 declarations
AllocatedRowSlicedIdealApproximation.lean 3 declarations
AllocatedRowsAmbientProjectedFamilyMultiple.lean 13 declarations
AllocatedSampledCoverIdeal.lean 3 declarations
AllocatedSampledPrincipalIdeal.lean 1 declarations
AllocatedScalarLogBounds.lean 34 declarations
AllocatedScaledIdealCover.lean 4 declarations
AllocatedSeparatedGeometry.lean 5 declarations
AllocatedShortAxis.lean 32 declarations
AllocatedShortDependence.lean 15 declarations
AllocatedShortRationalMarginal.lean 1 declarations
AllocatedSiteBufferLog.lean 22 declarations
AllocatedSiteEnvelopeControlled.lean 1 declarations
AllocatedSiteEnvelopeGain.lean 4 declarations
AllocatedSiteWindowLogBounds.lean 10 declarations
AllocatedSlicedBooleanSite.lean 6 declarations
AllocatedSlicedCoarseSource.lean 25 declarations
AllocatedSlicedCoveredComparison.lean 16 declarations
AllocatedSlicedDiscreteIdeal.lean 18 declarations
AllocatedSlicedEndpointComparison.lean 7 declarations
AllocatedSlicedEndpointIdentity.lean 53 declarations
AllocatedSlicedFiniteModelComparison.lean 9 declarations
AllocatedSlicedIdealCutoff.lean 2 declarations
AllocatedSlicedIdealTransferWithCutoff.lean 2 declarations
AllocatedSlicedLongReference.lean 1 declarations
AllocatedSlicedModularSeparateTailContinuousSource.lean 1 declarations
AllocatedSlicedNormalizedNativeModel.lean 12 declarations
AllocatedSlicedOneCube.lean 2 declarations
AllocatedSlicedOriginalLongComparison.lean 4 declarations
AllocatedSlicedProductPrefactorCap.lean 16 declarations
AllocatedSlicedProxyQuadrature.lean 1 declarations
AllocatedSlicedRowsProjectedSource.lean 19 declarations
AllocatedSourceNormalization.lean 4 declarations
AllocatedStrideRefinedStatement.lean 3 declarations
AllocatedTailProfileIdentity.lean 29 declarations
AllocatedTestUniformCoarseJointComparison.lean 6 declarations
AllocatedTestUniformCoarseJointStatement.lean 10 declarations
AllocatedTestUniformNormalizedComparison.lean 5 declarations
AllocatedTrimmedNormalization.lean 1 declarations
AllocatedTrimmedVectorSite.lean 27 declarations
AllocatedTupleSideThreshold.lean 8 declarations
AllocatedTwistVariationEarlyPower.lean 1 declarations
AllocatedUniformCommonCover.lean 4 declarations
AllocatedUniformPeriodSizes.lean 1 declarations
AllocatedUniformReferencePrescribed.lean 3 declarations
AllocatedUniformWidthObstruction.lean 1 declarations
AllocatedUnitSiteFactors.lean 10 declarations
AllocatedWeightedProfileError.lean 1 declarations
AllocatedWholeProfileEnvelope.lean 16 declarations
AllocatedWholeProfileRowReindex.lean 12 declarations
AllocatedWholeProfileUniformCap.lean 3 declarations
AllocatedWindowMajorant.lean 1 declarations
AllocatedWindowPrefactor.lean 4 declarations
AllocatedZeroLayerCommonSideInitializationUniform.lean 5 declarations
AllocatedZeroLayerDetectorReturn.lean 9 declarations
AllocatedZeroLayerFixedCenterExcess.lean 12 declarations
AllocatedZeroLayerForwardFrontSourceProfile.lean 6 declarations
AllocatedZeroLayerScalarPassage.lean 6 declarations
AmbientBooleanReconstruction.lean 2 declarations
AmbientImageExtension.lean 7 declarations
AmplificationFinalCostGrowth.lean 33 declarations
AnchoredCoefficientCongruenceRemoval.lean 1 declarations
AnchoredCoefficientHaarApproximation.lean 2 declarations
AnchoredCubeCongruenceRemoval.lean 1 declarations
AnchoredFixedCenterDomination.lean 1 declarations
AnchoredProductFactorization.lean 1 declarations
AnchoredReferenceDomination.lean 19 declarations
AnchoredReflectedFamily.lean 11 declarations
AnchoredSelectedNormalization.lean 1 declarations
AnchoredSelectedOneSiteComparison.lean 1 declarations
AnchoredSparseFamilies.lean 2 declarations
AnchoredSquareImagePartition.lean 2 declarations
AnchoredTranslatedNormalization.lean 1 declarations
AnchoredTrimmedReference.lean 2 declarations
AnisotropicTupleErrorChoice.lean 6 declarations
AnnihilatorIntervalBound.lean 3 declarations
AntisymmetricMiddleQuotient.lean 2 declarations
AntisymmetricPairVerticalModel.lean 40 declarations
AntisymmetricPartitionApproximation.lean 18 declarations
ApproxMomentCutoff.lean 2 declarations
ApproxMomentEnvelope.lean 4 declarations
ArrayFunctionalSection.lean 4 declarations
AuxiliaryCellMeans.lean 3 declarations
AuxiliaryIntervalCells.lean 3 declarations
AuxiliaryStrideGeometry.lean 4 declarations
AveragedModeledPatchTransfer.lean 31 declarations
AxisCompression.lean 24 declarations
BSGIndicator.lean 14 declarations
BaselineNoIncrementTree.lean 4 declarations
BiasedNativeTerminal.lean 5 declarations
BiasedSynchronizedSquareFamily.lean 19 declarations
BinaryTupleSorting.lean 9 declarations
BlockQuotientRows.lean 1 declarations
BlockQuotientTriangular.lean 1 declarations
BlockSubsetCount.lean 6 declarations
BooleanAxisLogEnvelope.lean 12 declarations
BooleanCubeGoodTest.lean 2 declarations
BooleanCubeGoodTranslation.lean 2 declarations
BooleanCubeModeWitness.lean 60 declarations
BooleanCubeProduct.lean 71 declarations
BooleanMinorDimension.lean 46 declarations
BooleanSelectedDerivativeBound.lean 31 declarations
BoundedAmbientModeWitness.lean 1 declarations
BoundedAnisotropicTupleChoices.lean 1 declarations
BoundedCoefficientEvaluation.lean 1 declarations
BoundedCoefficientExpansion.lean 5 declarations
BoundedCommonSiteResidual.lean 6 declarations
BoundedExtendedSiteSection.lean 11 declarations
BoundedFastCoefficientGenerators.lean 4 declarations
BoundedFreeWords.lean 7 declarations
BoundedHomogeneousFactorization.lean 1 declarations
BoundedInequalityGoodCutoff.lean 24 declarations
BoundedNativeDependentApproximations.lean 13 declarations
BoundedPowerStackConstruction.lean 1 declarations
BoundedProductDifference.lean 1 declarations
BoundedQuotientFunctional.lean 4 declarations
BoundedRealifiedSquareOrbit.lean 25 declarations
BoundedRightInverseMinor.lean 3 declarations
BoundedSparseGenerators.lean 1 declarations
BoundedSubmoduleIntersection.lean 9 declarations
BoundedWeightedSliceAxis.lean 2 declarations
BufferedSiteExpansion.lean 27 declarations
BufferedTranslationIncrement.lean 2 declarations
CanonicalCoefficientCoverLift.lean 11 declarations
CanonicalCubeMinorThreshold.lean 15 declarations
CanonicalEmptyLayerGeometry.lean 58 declarations
CanonicalScalarSourceEnvelope.lean 40 declarations
CanonicalSiteBlocks.lean 34 declarations
CanonicalSlicedSourcePositivity.lean 5 declarations
CanonicalUnconditionedScalarTransfer.lean 9 declarations
CappedDistanceReconstruction.lean 4 declarations
CappedNormalizedComparison.lean 1 declarations
CenteredFiniteNoiseEventBound.lean 1 declarations
CenteredFiniteReferenceComparison.lean 1 declarations
CenteredFiniteSliceResidualEnvelope.lean 36 declarations
CenteredFullParameterGeometry.lean 2 declarations
CenteredNormalizedNativeDetection.lean 1 declarations
CenteredReferenceCap.lean 4 declarations
CentralAdaptedRebase.lean 3 declarations
CircleFejerAverage.lean 11 declarations
CoarseLocalizationError.lean 2 declarations
CocycleHorizontalNormalization.lean 16 declarations
CoefficientAverageL1.lean 1 declarations
CoefficientCoverSampleTower.lean 2 declarations
CoefficientDeckImageCongruence.lean 26 declarations
CoefficientDeckMaskedIntegral.lean 1 declarations
CoefficientFamilyLocalization.lean 1 declarations
CoefficientFiberOrthogonality.lean 3 declarations
CoefficientJetHaar.lean 2 declarations
CoefficientJetScalar.lean 29 declarations
CoefficientLengthProduct.lean 1 declarations
CoefficientModeLowerTerms.lean 21 declarations
CoefficientModeRationalDecomposition.lean 1 declarations
CoefficientNormalization.lean 19 declarations
CoefficientPairCover.lean 7 declarations
CoefficientProductHaar.lean 1 declarations
CoefficientRowEvaluation.lean 26 declarations
CoefficientRowReindex.lean 25 declarations
CoefficientScaleGap.lean 3 declarations
CoefficientSignedExpansion.lean 5 declarations
CoefficientSliceEmbedding.lean 53 declarations
CoefficientTailScaling.lean 11 declarations
CoefficientTensorApproximation.lean 3 declarations
CoefficientUniformSmallError.lean 1 declarations
CommonCoefficientFourAnnihilators.lean 35 declarations
CommonDenominatorMultiples.lean 4 declarations
CommonDependentCoveredModel.lean 5 declarations
CommonDependentIntegralModel.lean 20 declarations
CommonDependentWordLayers.lean 41 declarations
CommonFixedNativeSquareFamily.lean 12 declarations
CommonFreeSunflower.lean 63 declarations
CommonInducedCorrelation.lean 6 declarations
CommonIntegralModelEquivalences.lean 17 declarations
CommonMarkedDirectionModel.lean 2 declarations
CommonMarkedModel.lean 3 declarations
CommonMarkedMultidegree.lean 37 declarations
CommonMarkedUnitModel.lean 2 declarations
CommonNativeScaledCorrections.lean 1 declarations
CommonNativeSquareFactors.lean 27 declarations
CommonPivotQuotientTop.lean 19 declarations
CommonPositivePartitionRefinement.lean 8 declarations
CommonProjectedCorrections.lean 2 declarations
CommonRefilteredFactorization.lean 17 declarations
CommonRefilteredFactorsNestedFreeze.lean 3 declarations
CommonRefilteredMappedOrbitFactors.lean 16 declarations
CommonSideExponentialAbsorption.lean 1 declarations
CommonStrideCorrelation.lean 1 declarations
CommonStrideGowersTransfer.lean 10 declarations
CommonSubspaceFamily.lean 2 declarations
CommonUniformCoefficientCorrections.lean 3 declarations
CommonWeightedExchange.lean 1 declarations
CompactIntervalIntegral.lean 2 declarations
CompactSliceErrorIntegral.lean 3 declarations
CompactSmoothApproximation.lean 1 declarations
ComparableScalarPhysicalFamilyPatch.lean 13 declarations
ComparableUnconditionedScalarFamily.lean 10 declarations
ComparableUnconditionedScalarTransfer.lean 7 declarations
ComparisonAmbient.lean 44 declarations
ComplexDiagonalVolumeIntegral.lean 5 declarations
ComplexExchangeTransfer.lean 6 declarations
ComplexFiniteMeans.lean 32 declarations
ComplexModelComparisonL1.lean 3 declarations
ComplexNormalizationError.lean 1 declarations
ComplexPolarization.lean 6 declarations
ComplexPositiveMasks.lean 9 declarations
ComplexSampledSquarePerturbation.lean 12 declarations
ComplexTestScaling.lean 4 declarations
ComplexUnitLocalLipschitz.lean 2 declarations
ConditioningShellError.lean 6 declarations
ConfigurationCenteredCounting.lean 1 declarations
ConstantCenterUniformLifts.lean 16 declarations
ConstantJetPostprocessing.lean 2 declarations
ConstantObservableMemberNets.lean 2 declarations
ConstructedNoPivotTopDescent.lean 2 declarations
ContainedProgressionCubeMap.lean 4 declarations
ContinuousCosetMap.lean 2 declarations
ContinuousImageFactor.lean 1 declarations
ControlledAdaptedRebase.lean 1 declarations
ControlledComparisonModel.lean 28 declarations
ControlledDetectedTranslationBaseBounds.lean 25 declarations
ControlledFixedMarkedNativeFactorization.lean 4 declarations
ControlledFullFastHorizontal.lean 1 declarations
ControlledLinearSubspaceLift.lean 10 declarations
ControlledMarkedDirectionModel.lean 2 declarations
ControlledNativeMarkedFreezing.lean 2 declarations
ControlledPrescribedMarkedNativeFactorization.lean 15 declarations
ControlledProductReconstruction.lean 8 declarations
ControlledRealFastCoefficientAction.lean 3 declarations
ControlledRefilteredCyclicExpansion.lean 4 declarations
ControlledRefilteredRecoveredExpansion.lean 9 declarations
ControlledSingleRefilteredReconstruction.lean 8 declarations
ControlledSurjectiveReconstruction.lean 4 declarations
ConvexEmpiricalApproximation.lean 4 declarations
CopiedLayerSpace.lean 18 declarations
CorePairingSplit.lean 2 declarations
CorrelatedModerateSiteComparison.lean 1 declarations
CorrelatingVerticalPair.lean 11 declarations
CorrelationDerivative.lean 66 declarations
CosetPairInjective.lean 1 declarations
CountingDeficitDetection.lean 5 declarations
CoveredInducedCorrelationFamily.lean 32 declarations
CoveredJetAmbientLift.lean 2 declarations
CoveredJetReference.lean 6 declarations
CoveredJetSampleMeasurable.lean 1 declarations
CoveredMixedArrayImage.lean 14 declarations
CoveredQuotientCorrelation.lean 11 declarations
CovolumeFactorBounds.lean 1 declarations
CubeSignalAlgebra.lean 15 declarations
CubeTranslation.lean 9 declarations
CubicAnchorExpansion.lean 2 declarations
CubicAntisymmetricModel.lean 20 declarations
CubicAntisymmetricTransfer.lean 38 declarations
CubicApproximatedModel.lean 1 declarations
CubicDerivativeModel.lean 29 declarations
CubicFactoredModel.lean 1 declarations
CubicFrozenLinearRows.lean 2 declarations
CubicFrozenMiddleExpansion.lean 3 declarations
CubicOriginalDiagonalComparison.lean 24 declarations
CubicPairFactoredModel.lean 25 declarations
CubicPairPartitionPrecision.lean 26 declarations
CubicPermutedSeven.lean 45 declarations
CubicPreciseDiagonalExchange.lean 2 declarations
CubicPrimitiveGowers.lean 1 declarations
CubicPrimitiveRows.lean 11 declarations
CubicResidualCrossGowers.lean 3 declarations
CubicRootExchange.lean 14 declarations
CubicRootPermutation.lean 37 declarations
CubicSevenCornerSymmetry.lean 10 declarations
CurrentLayerPreservation.lean 28 declarations
CurrentLayerSplitting.lean 4 declarations
CutoffImageTest.lean 3 declarations
CyclicBilinearBound.lean 2 declarations
CyclicCellAnchors.lean 1 declarations
CyclicComparisonMean.lean 2 declarations
CyclicCutNeighborhood.lean 58 declarations
CyclicIntervalCubeComparison.lean 3 declarations
CyclicMixedReflection.lean 14 declarations
CyclicOrdinaryShiftBranches.lean 4 declarations
CyclicProductDetection.lean 4 declarations
CyclicProgressionHom.lean 16 declarations
CyclicRelativeChang.lean 20 declarations
CyclicShortShiftSet.lean 5 declarations
CylinderUniformSections.lean 1 declarations
DehomogenizedExponent.lean 3 declarations
DenseCommonStrideCardRatio.lean 2 declarations
DenseCorrelationPairs.lean 14 declarations
DenseCyclicFreimanModel.lean 1 declarations
DenseModelFourfoldLift.lean 1 declarations
DenseProductApproximation.lean 16 declarations
DenseProductCardDeficit.lean 4 declarations
DenseProgressionInnerFamily.lean 22 declarations
DenseSubboxCost.lean 1 declarations
DenseTranslate.lean 1 declarations
DependentPatchValue.lean 59 declarations
DependentPiProduct.lean 2 declarations
DerivativeHorizontalLifts.lean 8 declarations
DerivativeIndexBounds.lean 16 declarations
DescendedLinearMapBounds.lean 2 declarations
DescentPartitionLengths.lean 4 declarations
DetectedCanonicalEarlyRadiusFreeTrimDetection.lean 6 declarations
DetectedCanonicalEarlyRadiusLateFloorSource.lean 7 declarations
DetectedCanonicalEarlyRadiusModelBounds.lean 5 declarations
DetectedTranslationMajorBase.lean 12 declarations
DetectedTranslationNormalizedLogBounds.lean 3 declarations
DeterminantCutoffScale.lean 1 declarations
DiagonalRowTransfer.lean 15 declarations
DiagonalSliceBounds.lean 4 declarations
DiagonalWrapComparison.lean 27 declarations
DiagramNativeExternalNetMonotone.lean 3 declarations
DilationCost.lean 5 declarations
DilationPairFiltration.lean 15 declarations
DiscreteMinorThreshold.lean 5 declarations
DisjointPowersetSum.lean 1 declarations
DivergenceExponentialBounds.lean 2 declarations
DyadicCountingParameters.lean 1 declarations
DynkinTrees.lean 24 declarations
EmbeddedFiniteConditioning.lean 31 declarations
EmptyLayerDetectionGeometry.lean 8 declarations
EmptyLayerPrescribedScale.lean 9 declarations
EmptyVariableCommonFactors.lean 4 declarations
EstimatesProductiveAllocatedFreezing.lean 2 declarations
EuclideanBallVolumeBound.lean 1 declarations
EuclideanBisectorNull.lean 2 declarations
EuclideanDerivativeCovolume.lean 3 declarations
EuclideanGraphNorm.lean 8 declarations
EuclideanGraphResidual.lean 7 declarations
EvenMomentChoice.lean 1 declarations
ExternalPhysicalMemberPivotMasks.lean 11 declarations
ExternalPivotMaskSelection.lean 3 declarations
ExternalUnitFamilyVerticalExpansion.lean 5 declarations
ExtractedInitialState.lean 21 declarations
FactoredC2Difference.lean 3 declarations
FactoredPositiveShiftContradiction.lean 22 declarations
FamilyDerivativeCorrelation.lean 1 declarations
FastCoefficientBlocks.lean 6 declarations
FastCoefficientImage.lean 69 declarations
FastCoefficientOperationBounds.lean 2 declarations
FastGradedRelativeInvariance.lean 8 declarations
FastHorizontalFactorization.lean 56 declarations
FilteredLieTree.lean 9 declarations
FiniteApproximationComparison.lean 3 declarations
FiniteAssignmentPartition.lean 7 declarations
FiniteBiasedSlice.lean 1 declarations
FiniteBoundedListEnumeration.lean 2 declarations
FiniteCellRefinement.lean 69 declarations
FiniteClassifiedRepresentatives.lean 4 declarations
FiniteCommonStrideFamily.lean 4 declarations
FiniteConvolution.lean 3 declarations
FiniteCorrectionHistory.lean 7 declarations
FiniteCubeBlockBounds.lean 4 declarations
FiniteDependentPMFBind.lean 29 declarations
FiniteDifferenceStability.lean 6 declarations
FiniteEnumerationFilter.lean 2 declarations
FiniteEqualityPatternCard.lean 7 declarations
FiniteEvenMomentTransfer.lean 4 declarations
FiniteEventUnion.lean 1 declarations
FiniteExceptionalMean.lean 1 declarations
FiniteFiberPMF.lean 2 declarations
FiniteFiberRepresentatives.lean 1 declarations
FiniteFiberTest.lean 53 declarations
FiniteFiberTsum.lean 6 declarations
FiniteFiberVolumeBound.lean 5 declarations
FiniteFourPointAnchors.lean 5 declarations
FiniteGoodPartTransfer.lean 13 declarations
FiniteGradedBranchPrefixLog.lean 17 declarations
FiniteGraphEnergy.lean 8 declarations
FiniteHypergraphAbstract.lean 38 declarations
FiniteImageCover.lean 1 declarations
FiniteImageProducts.lean 3 declarations
FiniteInnerProgressionFamily.lean 17 declarations
FiniteInversePerturbation.lean 2 declarations
FiniteLowLevelSeries.lean 1 declarations
FiniteMarkedFreezingCellBound.lean 4 declarations
FiniteMixedArrayRefresh.lean 7 declarations
FiniteMixedPermutation.lean 19 declarations
FiniteNoSingletonRows.lean 1 declarations
FiniteOrderedSubsetSum.lean 1 declarations
FiniteProductCellMean.lean 16 declarations
FiniteProductDiscount.lean 1 declarations
FiniteProductDomination.lean 2 declarations
FiniteProductImageDecay.lean 11 declarations
FiniteProductSumEstimate.lean 1 declarations
FiniteProductWeightL1.lean 4 declarations
FiniteProductWitness.lean 2 declarations
FinitePushforwardComplexWeights.lean 5 declarations
FiniteReciprocalTenthTail.lean 13 declarations
FiniteRetainedCellMean.lean 4 declarations
FiniteSectionCountBounds.lean 2 declarations
FiniteSectionOrderedFree.lean 4 declarations
FiniteSectionPermutation.lean 50 declarations
FiniteSectionVanishing.lean 2 declarations
FiniteSeriesCoefficientBounds.lean 14 declarations
FiniteShellSum.lean 1 declarations
FiniteTriangularRationalCorrection.lean 5 declarations
FiniteTripleAssembly.lean 2 declarations
FiniteTupleFibers.lean 2 declarations
FiniteWeightedConjugate.lean 1 declarations
FiniteWeightedErrorIntegral.lean 1 declarations
FiniteWeightedExpansion.lean 15 declarations
FiniteWindowVolumeCancellation.lean 2 declarations
FiniteWindowWeightError.lean 2 declarations
FirstCoefficientDerivativeBounds.lean 34 declarations
FirstCoefficientDimension.lean 6 declarations
FixedAnchoredQuotientModes.lean 1 declarations
FixedBilinearRefinement.lean 1 declarations
FixedObservableCorrelation.lean 16 declarations
FixedObservableMarkedFiberGlobalLift.lean 4 declarations
FixedPartnerPower.lean 31 declarations
FixedPatchFunction.lean 1 declarations
FixedPositiveCoefficientSource.lean 12 declarations
FixedTwoShiftBranches.lean 1 declarations
FlatWeightedComparison.lean 47 declarations
FormalCurrentDerivativeAdvance.lean 1 declarations
FormalCurrentInputBounds.lean 8 declarations
FormalExpLog.lean 6 declarations
FormalHorizontalReabsorption.lean 7 declarations
FormalInductionStage.lean 1 declarations
FormalInductionTerminal.lean 28 declarations
FormalLinearLiftReabsorption.lean 4 declarations
FormalMarkedOrbitTranslation.lean 1 declarations
FourBalancedRelations.lean 14 declarations
FourProductSmoothing.lean 9 declarations
FourSlicedProductSmoothing.lean 9 declarations
FreeCoefficientCorrectionControl.lean 2 declarations
FreeCorrelationRelationRefinement.lean 18 declarations
FreeLieTreeCoefficientBounds.lean 40 declarations
FreePrimitiveCriterion.lean 100 declarations
FreeWeightedEvaluationBounds.lean 7 declarations
FreeWeightedLayerBounds.lean 14 declarations
FreeWeightedModelBounds.lean 8 declarations
FreimanFivefoldCardinality.lean 5 declarations
FreimanInverseLift.lean 49 declarations
FrozenCosetVariation.lean 13 declarations
FrozenMarkedLeftOrbitBound.lean 12 declarations
FrozenPMFMixedComparison.lean 1 declarations
FullFastHorizontalNormalization.lean 3 declarations
FullMarkedNativeFactorization.lean 7 declarations
FullRestrictedGradeMajorMatching.lean 3 declarations
FullTaggedRationalRetraction.lean 13 declarations
GaussianNonzeroIndex.lean 2 declarations
GaussianPerturbation.lean 3 declarations
GaussianScaledShortVectorBound.lean 5 declarations
GaussianTailRadius.lean 6 declarations
GlobalCutoffAtomComparison.lean 1 declarations
GlobalMarkedOuterNormalization.lean 8 declarations
GlobalMarkedPhysicalValueBounds.lean 3 declarations
GowersWeightedDerivative.lean 6 declarations
GradedNormalizedRelativeLog.lean 12 declarations
GradedPieceRepresentative.lean 1 declarations
GradedUnitEvaluation.lean 32 declarations
GramCovolume.lean 1 declarations
GroupReductionFactors.lean 4 declarations
GroupedSiteTensor.lean 15 declarations
HaarMixedCenter.lean 1 declarations
HaarShiftImage.lean 1 declarations
HigherResidualRowDifferences.lean 8 declarations
HomogeneousComponentTopSubstitution.lean 1 declarations
HomogeneousQuotientSymbolLiftBounds.lean 44 declarations
HomogeneousRealSymbolPullback.lean 9 declarations
HomogeneousScaledSubstitution.lean 1 declarations
HomogeneousSubspaceCorrections.lean 4 declarations
HomogenizedModeFactorization.lean 5 declarations
HorizontalAmbientQuotient.lean 8 declarations
HorizontalPivotExclusion.lean 1 declarations
ImageCosetReconstruction.lean 9 declarations
ImageExtensionInverseBounds.lean 5 declarations
ImageRepresentatives.lean 27 declarations
InactiveAxisScale.lean 8 declarations
InactiveFiberProductComparison.lean 2 declarations
InactiveShortLogBounds.lean 16 declarations
IndependentColumnsMinor.lean 2 declarations
IndependentEmbeddingConditioning.lean 1 declarations
IndependentFiniteConditioning.lean 10 declarations
IndependentPMFOption.lean 1 declarations
IndependentProductMeans.lean 3 declarations
IndependentProductPMFSum.lean 1 declarations
IndependentReturnScale.lean 17 declarations
IndexedComparableScalarGeometryData.lean 24 declarations
InheritedTaggedQuotientPrecenterMasks.lean 25 declarations
InitialReplacementMeshWidths.lean 3 declarations
InitialShellFiniteSum.lean 1 declarations
InitializedEarlyCanonicalSliceScales.lean 8 declarations
IntegralHyperplaneCorrection.lean 7 declarations
IntegralOrthogonalSection.lean 2 declarations
IntegralSlowSlice.lean 1 declarations
InteriorIntervalCutoff.lean 34 declarations
InvariantUnitFamily.lean 5 declarations
InverseDerivativeBound.lean 3 declarations
InverseSqrtMoment.lean 10 declarations
IteratedCircleAverageIntegral.lean 35 declarations
JetAxisReference.lean 3 declarations
JoinedCoefficientProfile.lean 7 declarations
JoinedPairQuotientRefiltration.lean 17 declarations
JointBooleanGoodWeight.lean 44 declarations
JointBooleanRegularization.lean 23 declarations
JointBooleanRegularizationChoice.lean 4 declarations
JointBooleanStability.lean 15 declarations
JointCoefficientRetainedTest.lean 24 declarations
JointComparisonTolerance.lean 4 declarations
JointL1TupleQuadrature.lean 1 declarations
JointMixedCoefficientComparison.lean 4 declarations
JointPrincipalCoefficientComparison.lean 2 declarations
JointRationalSpaceGenerators.lean 4 declarations
JointTupleTolerance.lean 21 declarations
LargeCokernelReciprocalBound.lean 1 declarations
LayeredCoverSiteExtension.lean 19 declarations
LengthDyadicCutoff.lean 3 declarations
LieFiniteProduct.lean 12 declarations
LieTreeMultidegree.lean 51 declarations
LiftedPointwiseSplitting.lean 1 declarations
LinearCoefficientMap.lean 4 declarations
LinearCoefficientSplitting.lean 1 declarations
LinearCutoff.lean 6 declarations
LinearDerivativeRemoval.lean 7 declarations
LinearLiftSheetCompatibility.lean 3 declarations
LinearMapIntegralCover.lean 4 declarations
LinearQuotientCoverAverage.lean 23 declarations
LinearRestrictionDenominatorSize.lean 3 declarations
LinearRestrictionHeight.lean 4 declarations
LipschitzExtensionAlongMap.lean 7 declarations
LipschitzLocalLifts.lean 2 declarations
LocalAverageAmplitude.lean 8 declarations
LocalBoostedAlmostPeriods.lean 24 declarations
LocalConvolutionAlternatives.lean 1 declarations
LocalCorrelationBounds.lean 2 declarations
LocalCorrelationEnergy.lean 3 declarations
LocalImageComparison.lean 2 declarations
LocalMajorSliceSites.lean 2 declarations
LocalMomentScale.lean 38 declarations
LocalProductContinuity.lean 1 declarations
LocalShiftFiber.lean 23 declarations
LocalWeightCaps.lean 5 declarations
LocalWeightedSifting.lean 10 declarations
LocalizedAverageScaleOrder.lean 4 declarations
LocalizedCorrelationMoment.lean 2 declarations
LocalizedSiftingAlmostPeriods.lean 25 declarations
LowJetAmbientReconstruction.lean 3 declarations
LowTaggedGradedSpace.lean 7 declarations
LowTaggedRationalLiftRewrite.lean 2 declarations
LowWeightFibers.lean 14 declarations
LowerRefilteredCyclicExpansion.lean 13 declarations
LowerStepSquare.lean 51 declarations
LowerTriangularMinor.lean 8 declarations
LowestWeightScheduledSourcePreparation.lean 1 declarations
LowestWeightSourceReadyPreparation.lean 1 declarations
MajorRationalLiftInputScale.lean 3 declarations
MajorTranslationJointLower.lean 2 declarations
MajorTranslationPureFactorValues.lean 3 declarations
MarginalTailModeling.lean 27 declarations
MarkedEvaluationJointBounds.lean 8 declarations
MarkedLocalCoefficientValue.lean 11 declarations
MarkedParameterOrbit.lean 2 declarations
MarkedPureEvaluation.lean 16 declarations
MarkedRefilteredLowerNativeDiagram.lean 9 declarations
MarkedShiftGeneratorBounds.lean 59 declarations
MarkedUnitOrbit.lean 23 declarations
MaskedCenteredCounting.lean 11 declarations
MaskedFiniteComparison.lean 2 declarations
MaskedIntervalApproximation.lean 4 declarations
MatchedFlatDecay.lean 11 declarations
McShaneEnvelope.lean 8 declarations
MeasurableConstantCenterRepresentative.lean 3 declarations
MinkowskiSecondInduction.lean 9 declarations
MixedAnchorExpansion.lean 6 declarations
MixedArrayReference.lean 18 declarations
MixedBooleanSiteValues.lean 44 declarations
MixedCoefficientCounting.lean 4 declarations
MixedCoveredRowReindex.lean 23 declarations
MixedCoveredSiteExtraction.lean 10 declarations
MixedFactoredCorrelation.lean 1 declarations
MixedFixedReduction.lean 9 declarations
MixedFrozenMiddleRows.lean 48 declarations
MixedPairComparison.lean 31 declarations
MixedPairFrozenEquivalence.lean 18 declarations
MixedPairPartitionPrecision.lean 18 declarations
MixedPairStepDrop.lean 3 declarations
MixedPermutationTensor.lean 23 declarations
MixedPreciseSampledExchange.lean 16 declarations
MixedPrimitiveGowers.lean 31 declarations
MixedProductTranslation.lean 5 declarations
MixedRealPoint.lean 4 declarations
MixedRootCyclicComparison.lean 8 declarations
MixedRootLosses.lean 68 declarations
MixedSelectedOneSite.lean 1 declarations
MixedTranslationCorrelation.lean 1 declarations
ModeRemovalThresholds.lean 24 declarations
ModeShiftLengths.lean 3 declarations
ModelTransferPrecision.lean 3 declarations
ModerateSliceTensorApproximation.lean 8 declarations
ModularDesignatedCoefficientMarkov.lean 4 declarations
ModularHalfExponentExceptions.lean 1 declarations
ModularMultilinearAmbientSublevel.lean 16 declarations
ModularMultilinearSublevelFiber.lean 9 declarations
ModularMultilinearSublevelNumerics.lean 3 declarations
ModularTagGap.lean 6 declarations
ModularUnitGCD.lean 2 declarations
ModularVectorCoefficientDecomposition.lean 2 declarations
ModularVectorCoefficientExceptions.lean 2 declarations
MomentEvaluationBounds.lean 6 declarations
MonotoneRegularPoint.lean 1 declarations
MonotoneWeightLayer.lean 1 declarations
MultiaffineBias.lean 2 declarations
MultiaffineExpansion.lean 2 declarations
MultiaffineOptionExpansion.lean 4 declarations
MultidegreeDilationPair.lean 57 declarations
MultidegreeIntegralModel.lean 7 declarations
MultidegreePredecessor.lean 2 declarations
MultilinearFirstOrder.lean 2 declarations
NativeAbsorbedIntervals.lean 34 declarations
NativeAnchoredDerivativeCorrelation.lean 3 declarations
NativeAnchoredInputPartition.lean 4 declarations
NativeAnchoredSquarePartition.lean 4 declarations
NativeBinaryAssignments.lean 36 declarations
NativeBoundedSubalgebraRepresentatives.lean 2 declarations
NativeBoundedVariablePatchExpansion.lean 15 declarations
NativeCentralSeed.lean 8 declarations
NativeCommonModelQuadruples.lean 21 declarations
NativeCorrelatedFactorFamily.lean 8 declarations
NativeCoveredCommonFactorization.lean 15 declarations
NativeCrossFactorization.lean 28 declarations
NativeDependentRepresentativeFamily.lean 2 declarations
NativeDetectorContradiction.lean 10 declarations
NativeDetectorContradictionSpec.lean 14 declarations
NativeDilationDescent.lean 22 declarations
NativeDilationObservable.lean 19 declarations
NativeDilationOrbit.lean 6 declarations
NativeEqualDimension.lean 7 declarations
NativeEquivalenceTransitivity.lean 16 declarations
NativeFiniteMarkedFreezing.lean 1 declarations
NativeFixedFactoredQuadruples.lean 8 declarations
NativeFixedVerticalPower.lean 8 declarations
NativeFrozenComparison.lean 13 declarations
NativeFrozenMarkedLocalMark.lean 22 declarations
NativeGlobalErrorSplitting.lean 9 declarations
NativeGraphSmallDifference.lean 56 declarations
NativeIntervalWeightPairs.lean 1 declarations
NativeIteratedDifferencing.lean 10 declarations
NativeLocalPivotVerticalPartners.lean 7 declarations
NativeMajorCorrelationFamily.lean 3 declarations
NativeMarkedDiagramOrbitLift.lean 26 declarations
NativeMarkedFreezingPhysicalData.lean 6 declarations
NativeMeanRowCorrelation.lean 9 declarations
NativeMixedCubeResiduals.lean 5 declarations
NativeMixedDerivativeResiduals.lean 2 declarations
NativeMixedReflectionBridge.lean 23 declarations
NativeMixedSeparatedFamily.lean 1 declarations
NativeModelOrbit.lean 28 declarations
NativeMultidegreeDilation.lean 2 declarations
NativeMultilinearQuadruples.lean 6 declarations
NativeMultilinearityCorrelation.lean 13 declarations
NativeNilcharacterTranslationEquivalence.lean 12 declarations
NativeOptionFixedSourceQuotientMarkStrong.lean 29 declarations
NativeOptionOriginalOrbit.lean 21 declarations
NativeOptionPivotQuotientStrong.lean 22 declarations
NativeOptionTargetObservableRegularity.lean 2 declarations
NativeOrbitFreezing.lean 11 declarations
NativeOrbitOuterControl.lean 6 declarations
NativePartitionFreezing.lean 2 declarations
NativePhysicalHaarExpansion.lean 40 declarations
NativePositiveCoefficientBases.lean 3 declarations
NativePositiveCorrelation.lean 1 declarations
NativePresentPivotQuotientModel.lean 1 declarations
NativeProductCoefficient.lean 33 declarations
NativeProductPartition.lean 1 declarations
NativeProductVerticalization.lean 15 declarations
NativeRationalRepresentatives.lean 1 declarations
NativeRefilteredSymbolConditions.lean 1 declarations
NativeResidualCrossInduction.lean 18 declarations
NativeResidualMultiplier.lean 41 declarations
NativeRetainedInverseIntervals.lean 6 declarations
NativeRetainedTargetCubeIntervals.lean 18 declarations
NativeRoundedCyclicModel.lean 6 declarations
NativeRoundedGraphEnergy.lean 26 declarations
NativeRoundedHomModel.lean 2 declarations
NativeSampleModelFamily.lean 12 declarations
NativeSelectedCorrelators.lean 19 declarations
NativeSeparatedSumIntervals.lean 16 declarations
NativeSharedFreeFamily.lean 5 declarations
NativeSharedFrozenCorrelations.lean 15 declarations
NativeSixVariablePatchExpansion.lean 1 declarations
NativeSlowConstantProduct.lean 1 declarations
NativeSpaceMap.lean 4 declarations
NativeSquareOrbit.lean 4 declarations
NativeSquareRecovery.lean 10 declarations
NativeSquarefreeCoefficientBases.lean 3 declarations
NativeSubspaceFreeModel.lean 34 declarations
NativeTrimmedTwistedSliceStepDrop.lean 2 declarations
NativeTwoSitePartition.lean 1 declarations
NativeTwoVariableSplitFreezing.lean 11 declarations
NativeWeightPairRemoval.lean 48 declarations
NestedDiracIntegral.lean 2 declarations
NestedProgressionReindex.lean 2 declarations
NonprincipalDilation.lean 16 declarations
NormalizedAmbientTent.lean 5 declarations
NormalizedCoefficientRemainder.lean 3 declarations
NormalizedCommonFamily.lean 10 declarations
NormalizedComparisonOrbit.lean 9 declarations
NormalizedCutoffs.lean 8 declarations
NormalizedDeterminantCutoff.lean 17 declarations
NormalizedFiberRescaling.lean 2 declarations
NormalizedFixedPatchFunction.lean 3 declarations
NormalizedImageMask.lean 3 declarations
NormalizedIntervalWindow.lean 16 declarations
NormalizedJetColumns.lean 10 declarations
NormalizedJetL1Parameter.lean 2 declarations
NormalizedJetMeasurability.lean 4 declarations
NormalizedMeshLengths.lean 3 declarations
NormalizedMinorBounds.lean 2 declarations
NormalizedNativeFamilyMonotone.lean 3 declarations
NormalizedSampledHistogram.lean 18 declarations
NormalizedSiteSections.lean 2 declarations
NormalizedSmallLiftHaar.lean 3 declarations
NormalizedTupleParameterBounds.lean 3 declarations
NormalizedTwistCellSelection.lean 11 declarations
NormalizedTwistNativeApproximation.lean 1 declarations
NormalizedTwistNativeMembership.lean 4 declarations
NormalizedTwistOne.lean 4 declarations
NormalizedTwistParameterPartition.lean 9 declarations
NormalizedTwistSliceVariationPairCorrelation.lean 11 declarations
NormalizedTwistTrimmedOuterCells.lean 1 declarations
NormalizedTwistUniformAmbientHaar.lean 1 declarations
NormalizedVectorLipschitz.lean 2 declarations
ObservedMarginalTesting.lean 2 declarations
ObservedSourceEquivalence.lean 4 declarations
ObservedTruncationResidual.lean 7 declarations
ObservedUnitTruncation.lean 14 declarations
OldLayerPreparation.lean 1 declarations
OneCubePrincipalSliceRiemann.lean 7 declarations
OneSiteCoefficientFactorization.lean 6 declarations
OneSiteResidualFactor.lean 1 declarations
OneSiteWeightIdentity.lean 1 declarations
OptionComplementCover.lean 24 declarations
OptionMarkedSurjective.lean 19 declarations
OrbitBasepointNormalization.lean 5 declarations
OrderedLayerSplit.lean 3 declarations
OrdinaryMeshMarginals.lean 1 declarations
OriginalDiagonalComparison.lean 4 declarations
OriginalMixedRootEquivalence.lean 60 declarations
OrthogonalBlockGram.lean 2 declarations
OrthogonalSection.lean 1 declarations
OverlapCubeWeights.lean 2 declarations
PMFLipschitzAverage.lean 2 declarations
PaddedBooleanFeatures.lean 3 declarations
PairedDiagonalApproximation.lean 18 declarations
ParentControlledMatching.lean 2 declarations
PartialComplexScaledQuadrature.lean 48 declarations
PartialProductDifference.lean 2 declarations
PartiallyBoundedNormalization.lean 1 declarations
PartitionedSlicedProfileComparison.lean 2 declarations
PeelingCellCaps.lean 5 declarations
PeelingChildBound.lean 7 declarations
PeelingCost.lean 5 declarations
PeelingDecomposition.lean 37 declarations
PeriodicCongruenceEvent.lean 5 declarations
PeriodicIsometricAction.lean 41 declarations
PerturbedOpenImageComparison.lean 1 declarations
PetalComparisonTree.lean 51 declarations
PhysicalActiveIdealSite.lean 20 declarations
PhysicalAmbientDifferenceWindow.lean 1 declarations
PhysicalAmbientVolumeRatio.lean 11 declarations
PhysicalBaseInjection.lean 4 declarations
PhysicalBoundaryLabels.lean 6 declarations
PhysicalCellLogCost.lean 3 declarations
PhysicalCellResidual.lean 2 declarations
PhysicalChildComparison.lean 2 declarations
PhysicalCubeNativeDetection.lean 13 declarations
PhysicalCubeWindowReindex.lean 2 declarations
PhysicalJetCoverCancellation.lean 26 declarations
PhysicalJetIntegralComparison.lean 3 declarations
PhysicalL1SourceAccuracy.lean 8 declarations
PhysicalOrbitRecovery.lean 2 declarations
PhysicalPairAccuracyLogBounds.lean 36 declarations
PhysicalResidualCorrelation.lean 1 declarations
PhysicalRowCoverCancellation.lean 2 declarations
PhysicalRowsCoveredL1Perturbation.lean 1 declarations
PhysicalRowsSiteReconstruction.lean 49 declarations
PhysicalSingleSiteAmbient.lean 1 declarations
PhysicalSingleSiteCommonCover.lean 52 declarations
PhysicalSliceCost.lean 6 declarations
PhysicalStabilityParameters.lean 14 declarations
PhysicalZeroExtension.lean 6 declarations
PinnedSectionMeans.lean 52 declarations
PivotJacobianBound.lean 9 declarations
PivotOutputLipschitz.lean 3 declarations
PivotStageBoundary.lean 37 declarations
PointwiseNormalization.lean 1 declarations
PointwiseSymbolComparison.lean 1 declarations
PolarizedCoefficientPermutation.lean 36 declarations
PolarizedLogDiagonal.lean 1 declarations
PolarizedLogPermutation.lean 1 declarations
PositiveCyclicCorrelation.lean 43 declarations
PositiveFiberMarginal.lean 3 declarations
PositiveNormalizationError.lean 4 declarations
PositiveReconstruction.lean 7 declarations
PositiveRetainedDenominatorLog.lean 22 declarations
PositiveShiftAnchor.lean 1 declarations
PositiveShiftNativePartners.lean 1 declarations
PositiveShiftProductData.lean 19 declarations
PositiveShiftRefilteredExpansion.lean 3 declarations
PositiveShiftRefilteredExpansionSpec.lean 8 declarations
PositiveShiftTestingGowers.lean 16 declarations
PositiveWeightContradiction.lean 2 declarations
PositiveWeightNormalization.lean 4 declarations
PositiveWeightedExpansion.lean 1 declarations
PowerIndexFromOrderedGenerators.lean 11 declarations
PowerSubgroup.lean 11 declarations
PreparationLogCost.lean 3 declarations
PreparationReindex.lean 8 declarations
PreparationSliceComposition.lean 8 declarations
PreparedActualShearPatchEndpoint.lean 6 declarations
PreparedCanonicalInitializedRelativeSource.lean 11 declarations
PreparedCanonicalInitializedRelativeSourceConclusion.lean 3 declarations
PreparedCanonicalNativeSource.lean 29 declarations
PreparedCanonicalRelativeEndpointBounds.lean 17 declarations
PreparedCenteredDeterminingSlots.lean 20 declarations
PreparedCenteredModelMarginalData.lean 10 declarations
PreparedCenteredShortJointBadProduct.lean 4 declarations
PreparedCenteredShortJointGoodData.lean 4 declarations
PreparedCenteredShortMeasurableBadProduct.lean 1 declarations
PreparedCenteredStagedModelProductiveGood.lean 10 declarations
PreparedCertifiedPhysicalBadProduct.lean 4 declarations
PreparedDetectedCanonicalGeometry.lean 10 declarations
PreparedDetectedCanonicalNativeSource.lean 15 declarations
PreparedDetectedCanonicalNativeSourceGeometry.lean 4 declarations
PreparedDetectionFixedNativePartners.lean 3 declarations
PreparedDilatedDeterminingSlots.lean 13 declarations
PreparedEarlyCanonicalSource.lean 1 declarations
PreparedEmptyLayerFiniteScheduleLocalDirectSource.lean 1 declarations
PreparedEnlargedModularAllocation.lean 8 declarations
PreparedFamilyCanonicalGeometry.lean 1 declarations
PreparedFiniteForwardDescendingAnchoredPaddedSource.lean 8 declarations
PreparedFiniteForwardDescendingPaddedSource.lean 7 declarations
PreparedFiniteForwardFixedCenterThreshold.lean 38 declarations
PreparedFiniteForwardIndexedAnchoredProductiveSource.lean 1 declarations
PreparedFiniteForwardLocalProductiveSource.lean 1 declarations
PreparedFiniteForwardPaddedProductiveSource.lean 1 declarations
PreparedFiniteForwardPairedLocalProductiveSource.lean 1 declarations
PreparedFiniteForwardProductiveSource.lean 2 declarations
PreparedFiniteForwardResidualAllowance.lean 1 declarations
PreparedFiniteForwardSeededIndexedProductiveSource.lean 1 declarations
PreparedFiniteForwardTreeStorage.lean 35 declarations
PreparedFiniteNestedAnchorRequiredPower.lean 5 declarations
PreparedFiniteNestedEndpointRequirement.lean 3 declarations
PreparedFiniteNestedForwardCanonicalFixedCenterSource.lean 19 declarations
PreparedFiniteNestedInitializedRelativeSource.lean 2 declarations
PreparedFiniteNestedSourceArrays.lean 19 declarations
PreparedFiniteNestedSourceRelativeInitializerBounds.lean 16 declarations
PreparedFiniteScheduleActualModelFamily.lean 1 declarations
PreparedFiniteScheduleCandidateDetection.lean 7 declarations
PreparedFiniteScheduleLocalProductiveSource.lean 5 declarations
PreparedFiniteScheduleLocalScalarConstruction.lean 21 declarations
PreparedFiniteScheduleModelAttachment.lean 6 declarations
PreparedFiniteScheduleUniversalMaskProductiveGood.lean 31 declarations
PreparedFiniteScheduleWitnessScalarPower.lean 1 declarations
PreparedLateToleranceCertifiedSource.lean 14 declarations
PreparedLayerFreezing.lean 18 declarations
PreparedModularCanonicalDetectorAmbientConsumer.lean 10 declarations
PreparedModularCanonicalDetectorPositive.lean 8 declarations
PreparedModularCanonicalDetectorPositiveBounds.lean 12 declarations
PreparedModularCanonicalDetectorThreshold.lean 9 declarations
PreparedModularCanonicalNativeSource.lean 1 declarations
PreparedModularDetectorBadProduct.lean 7 declarations
PreparedModularDetectorCertifiedBadProduct.lean 1 declarations
PreparedModularGeneralCenteredDetection.lean 2 declarations
PreparedModularGeneralDetectorLateCoarseConsumer.lean 8 declarations
PreparedModularGeneralDetectorLateFloor.lean 5 declarations
PreparedModularGeneralDetectorNativeBounds.lean 24 declarations
PreparedModularGeneralDetectorProductive.lean 9 declarations
PreparedModularGeneralDetectorThreshold.lean 5 declarations
PreparedModularGeneralDirectDetectionLateFloor.lean 7 declarations
PreparedModularGeneralProductivityEarlyGain.lean 14 declarations
PreparedModularProductivityPrecision.lean 7 declarations
PreparedModularWitnessCanonicalGeometry.lean 7 declarations
PreparedOldPatchFreezePower.lean 1 declarations
PreparedPerturbativeCertifiedSource.lean 2 declarations
PreparedPhysicalBadProductSource.lean 5 declarations
PreparedReadyPaddedRelativeInitialization.lean 6 declarations
PreparedRelativeEndpointNumericalBounds.lean 15 declarations
PreparedRelativeEndpointSourceBounds.lean 24 declarations
PreparedRelativeFinalPower.lean 20 declarations
PreparedRelativeInitializerScalarInputs.lean 11 declarations
PreparedRelativePositiveNativeRuleCanonical.lean 31 declarations
PreparedRelativePositivePassage.lean 8 declarations
PreparedScalarFiniteScheduleCandidateDetection.lean 5 declarations
PreparedScalarNestedPowerDetection.lean 13 declarations
PreparedScalarStructuralBasePower.lean 11 declarations
PreparedShortLateFloorCertifiedBadProduct.lean 12 declarations
PreparedShortLateToleranceCertifiedAttachment.lean 4 declarations
PreparedSourceGeometryNormalizedPatchConclusion.lean 4 declarations
PreparedUniformEarlyRadiusWithCutoff.lean 38 declarations
PrescribedComplementInputPartition.lean 8 declarations
PrescribedCoveredInputPartition.lean 2 declarations
PrescribedInvariantUnit.lean 8 declarations
PrescribedPartitionExpansionCore.lean 5 declarations
PrescribedSquareImagePartition.lean 5 declarations
PrimitiveExtension.lean 20 declarations
PrimitiveNormalDilation.lean 4 declarations
PrincipalAxisInterpolation.lean 4 declarations
PrincipalBlockExponent.lean 6 declarations
PrincipalCoefficientComparison.lean 3 declarations
PrincipalCoefficientMarginal.lean 56 declarations
PrincipalCoefficientSource.lean 6 declarations
PrincipalJointL1Comparison.lean 1 declarations
PrincipalMixedComparison.lean 2 declarations
PrincipalRetainedIntegral.lean 2 declarations
ProductCoefficientMixedCenter.lean 1 declarations
ProductCutoffLipschitz.lean 44 declarations
ProductDependsOnMix.lean 1 declarations
ProductDifferenceBias.lean 1 declarations
ProductFamilyMomentComparison.lean 1 declarations
ProductMarginalAtomError.lean 5 declarations
ProductMeanPullback.lean 18 declarations
ProductOperatorInverse.lean 5 declarations
ProductOrbitCongruence.lean 18 declarations
ProductPMFMap.lean 7 declarations
ProductReferenceFiber.lean 2 declarations
ProductRestrictionWeightedCommonFactors.lean 20 declarations
ProductRestrictionsCommonRefiltration.lean 1 declarations
ProductTensorGroupedBound.lean 9 declarations
ProductTensorNormalizedUniform.lean 2 declarations
ProductTensorSectionPointwise.lean 8 declarations
ProductiveAllocatedFreezing.lean 2 declarations
ProductiveFrozenLocalMajorFamily.lean 51 declarations
ProductiveLocalMajorFamily.lean 6 declarations
ProgressionCubeEmbedding.lean 59 declarations
ProgressionPartitionComposition.lean 51 declarations
ProgressionRefinedConditioning.lean 4 declarations
ProgressionSliceApproximation.lean 1 declarations
ProgressionSliceUniformMesh.lean 2 declarations
ProgressionTupleSliceRiemann.lean 1 declarations
ProjectedHorizontalFactorization.lean 1 declarations
ProjectedNativeCoefficient.lean 20 declarations
ProjectedPointwiseCoefficient.lean 17 declarations
ProjectedTranslationGroup.lean 18 declarations
ProjectedTranslationImageGrading.lean 3 declarations
ProperSubspaceCount.lean 3 declarations
QuadraticAntisymmetricCorrelation.lean 7 declarations
QuadraticAntisymmetricOrbit.lean 5 declarations
QuadraticBoundedFamily.lean 44 declarations
QuadraticCyclicAntisymmetric.lean 12 declarations
QuadraticCyclicIntegration.lean 3 declarations
QuadraticPairCorrelatingAnchor.lean 2 declarations
QuadraticPairCorrelator.lean 17 declarations
QuadraticPairStepDrop.lean 28 declarations
QuadraticWeightedSymmetry.lean 4 declarations
QuantitativeNoninjectivity.lean 25 declarations
QuarticAnchoredMixedModel.lean 3 declarations
QuarticAntisymmetricModel.lean 10 declarations
QuarticAntisymmetricTransfer.lean 7 declarations
QuarticCorrelatingVerticalPair.lean 19 declarations
QuarticCyclicDiagonalComparison.lean 66 declarations
QuarticCyclicInverse.lean 2 declarations
QuarticCyclicPositiveCorrelation.lean 21 declarations
QuarticDiagonalWrap.lean 23 declarations
QuarticFactoredModel.lean 1 declarations
QuarticFrozenMiddleExpansion.lean 4 declarations
QuarticFrozenRows.lean 23 declarations
QuarticNativeMixed.lean 4 declarations
QuarticPairComparison.lean 19 declarations
QuarticPairFactors.lean 14 declarations
QuarticPairFrozenEquivalence.lean 18 declarations
QuarticPairPartitionPrecision.lean 24 declarations
QuarticPairPartitionedModel.lean 17 declarations
QuarticPreciseSampledExchange.lean 25 declarations
QuarticPrimitiveGowers.lean 34 declarations
QuarticRootExchange.lean 31 declarations
QuarticSurvivorMultilinearization.lean 68 declarations
QuotientInducedMark.lean 33 declarations
QuotientSubspaceFunctional.lean 1 declarations
QuotientTopSymbol.lean 5 declarations
QuotientTranslatePartition.lean 4 declarations
RationalApproximationScaling.lean 1 declarations
RationalCentralCircle.lean 13 declarations
RationalFormalStageGeometry.lean 4 declarations
RationalHeight.lean 12 declarations
RationalImageIntersections.lean 11 declarations
RationalInactiveJointComparisonInstances.lean 4 declarations
RationalInactivePartialReference.lean 3 declarations
RationalLieSubalgebra.lean 19 declarations
RationalOutputAxisReindex.lean 7 declarations
RationalPowerHeight.lean 20 declarations
RationalRealSubgroup.lean 4 declarations
RationalRowReduction.lean 26 declarations
RationalSubspaces.lean 4 declarations
RationalTagConstraintSpaces.lean 22 declarations
RationalTaggedConstraintHistory.lean 68 declarations
RawProductArrayNormalization.lean 8 declarations
RawSourceTolerance.lean 24 declarations
RealAnnihilatorCorrections.lean 2 declarations
RealBooleanInterpolation.lean 5 declarations
RealCoefficientFourAnnihilators.lean 1 declarations
RealDirectionExtension.lean 3 declarations
RealFiniteZeroExtension.lean 13 declarations
RealFirstCoefficientHorizontal.lean 42 declarations
RealGeneratorCombinations.lean 4 declarations
RealGradedDerivativeBounds.lean 4 declarations
RealImageFactorCorrection.lean 2 declarations
RealMultidegreeQuotientOrbit.lean 5 declarations
RealNormalizedSquareFactorization.lean 1 declarations
RealOrderedSlots.lean 3 declarations
RealPolarizedLogDiagonal.lean 1 declarations
RealProductInclusion.lean 11 declarations
RealProjectedCoefficientLift.lean 30 declarations
RealReducedCoefficientMap.lean 6 declarations
RealSubquotientEquiv.lean 18 declarations
RealSubspaceIntersectionCorrections.lean 13 declarations
RealSymbolGradeEvaluation.lean 11 declarations
RealSymbolGradeQuotientSplitting.lean 27 declarations
RealSymbolGradedCoefficientBound.lean 6 declarations
RealSymbolRepresentativeSplitting.lean 38 declarations
RealTranslationEvaluationContinuity.lean 5 declarations
RealWeightPMF.lean 3 declarations
RealificationFixedSubmodule.lean 3 declarations
RealificationModuleTopology.lean 1 declarations
RealifiedDilationMultidegree.lean 13 declarations
RealifiedMultidegree.lean 25 declarations
RealifiedReconstruction.lean 18 declarations
RealifiedTopQuotient.lean 27 declarations
RealifiedTripleLayers.lean 45 declarations
RebasedUnitVerticalObservable.lean 2 declarations
ReconstructedCubeNativePartner.lean 2 declarations
RecoveryPrecision.lean 1 declarations
RectangularCellGeometry.lean 4 declarations
RectangularDetExpansion.lean 1 declarations
RectangularPMFComparison.lean 1 declarations
RecursiveExceptionalPatchTransfer.lean 1 declarations
ReducedDiagonalBounds.lean 8 declarations
ReducedNativeFactorization.lean 70 declarations
ReducedProjectedComparison.lean 5 declarations
ReducedRelativeCoefficientBounds.lean 41 declarations
ReducedSquareSymbol.lean 45 declarations
ReducedSymbolDimensions.lean 8 declarations
ReducedTranslationMajorTwistedVerticalSelection.lean 2 declarations
RefilteredPointwiseSplitting.lean 20 declarations
RefilteredReconstructionDiagram.lean 4 declarations
RefinementEnlargement.lean 29 declarations
RefinementErrorNormalization.lean 6 declarations
RefinementMatchingGeometry.lean 15 declarations
RegularCylinderDecomposition.lean 32 declarations
ReindexSymbolFactorization.lean 6 declarations
ReindexedCubeDomain.lean 5 declarations
ReindexedDerivativePoints.lean 3 declarations
ReindexedFastCoefficientSection.lean 17 declarations
RelativeAmplificationDiscount.lean 1 declarations
RelativeChildSliceGeometry.lean 6 declarations
RelativeCoefficientGeometry.lean 16 declarations
RelativeFiberSlicePatch.lean 24 declarations
RelativePatchAmplification.lean 48 declarations
RelativePatchPositivePowerInduction.lean 25 declarations
RelativePatchRecoveredEndpoint.lean 1 declarations
RelativePatchScalarBaseFin.lean 1 declarations
RelativePatchSourceTestFinBounds.lean 10 declarations
RelativePatchWeightDescent.lean 8 declarations
RelativeRetainedCubeSource.lean 37 declarations
RelativeScalarPassageDiscount.lean 5 declarations
RelativeSliceTargetCap.lean 1 declarations
RelativeWidthProfileScale.lean 1 declarations
ReplicatedLieAction.lean 42 declarations
RepresentativeWindowPatch.lean 39 declarations
ResidualErrorAllocation.lean 34 declarations
RestrictedGradeMajorMatching.lean 6 declarations
RestrictedMajorCorrectionOnSet.lean 3 declarations
RestrictedSymbolAlgebraicMajorStep.lean 5 declarations
RetainedCoefficientSlice.lean 15 declarations
RetainedJointUnitOrder.lean 1 declarations
RetainedPatchCutoffChoice.lean 5 declarations
RetainedPhysicalDifference.lean 2 declarations
RetainedRefiltering.lean 2 declarations
RetainedShellComparison.lean 4 declarations
RetainedSliceAverages.lean 4 declarations
RetainedSlicedCoefficientSource.lean 7 declarations
ReweightedFiberDomination.lean 3 declarations
RiemannianLipschitz.lean 4 declarations
RightCosetEDistance.lean 15 declarations
RootDifferencePeriod.lean 3 declarations
RoundingRecoveryScale.lean 3 declarations
RowRestrictedDeckSiteMask.lean 33 declarations
RowShiftTopSymbol.lean 6 declarations
SampledCommonSlice.lean 13 declarations
SampledNativeDetectionEmptyTags.lean 8 declarations
SampledNativeModel.lean 41 declarations
SampledSliceFixedModelPartners.lean 2 declarations
SaturatedFlag.lean 35 declarations
ScalarBadSublevelRamp.lean 5 declarations
ScalarCubeBoundaryCost.lean 8 declarations
ScalarCubeBoundaryVolume.lean 8 declarations
ScalarCubeCokernelCutoff.lean 10 declarations
ScalarCubeDomain.lean 29 declarations
ScalarCubeFaceSlab.lean 33 declarations
ScalarCubeRootTranslation.lean 8 declarations
ScalarCubeWindowDomain.lean 8 declarations
ScalarDominatedSlack.lean 20 declarations
ScalarExtensionSubstitution.lean 1 declarations
ScalarInitialThreshold.lean 2 declarations
ScalarInputLogFactor.lean 1 declarations
ScalarWindowPartitions.lean 3 declarations
ScaledConditionedComparison.lean 30 declarations
ScaledFloorPerturbation.lean 2 declarations
ScaledJointFrozenSource.lean 14 declarations
ScaledLinearResidual.lean 5 declarations
ScaledSectionGram.lean 3 declarations
SecondDifferenceVectorEquivalence.lean 8 declarations
SecondaryMeshGeometry.lean 9 declarations
SelectedChildBound.lean 2 declarations
SelectedCoefficientEvaluation.lean 41 declarations
SelectedImageCorrections.lean 1 declarations
SelectedJointLifts.lean 4 declarations
SelectedJointSiteDomination.lean 1 declarations
SelectedJointWeightedReferenceComparison.lean 2 declarations
SelectedOutputL1.lean 9 declarations
SelectedPhysicalReferenceCap.lean 3 declarations
SelectedProductEnvelope.lean 1 declarations
SelectedProfileTranslationL1.lean 2 declarations
SelectedSingletonSmoothTestQuadrature.lean 8 declarations
SelectedSplitUnitSource.lean 7 declarations
SelectedWindowIndicator.lean 10 declarations
SeparatedCosetBalls.lean 4 declarations
SeparatedInterpolationBound.lean 4 declarations
SeparatedLabelExtension.lean 2 declarations
SeparatedPositiveSum.lean 1 declarations
SeparatedRealSamples.lean 2 declarations
Separation.lean 2 declarations
SharedFreeComparisonDescent.lean 2 declarations
SharedFreeComparisonLift.lean 21 declarations
SharedFreeComparisonOrbit.lean 1 declarations
SharedFreeCorrelatedFactorization.lean 1 declarations
SharedFreeFrozenComparison.lean 7 declarations
SharedFreeLowerFactorization.lean 7 declarations
SharedFreeRoundingThreshold.lean 18 declarations
SharedWidthPreparedChoice.lean 3 declarations
SharedWidthPreparedLateToleranceFreeTrimSource.lean 8 declarations
SharedWidthPreparedModularGeneralDirectDetectionFreeTrim.lean 8 declarations
SharedWidthPreparedPerturbativeCertifiedSource.lean 15 declarations
ShiftDifferenceCount.lean 13 declarations
ShiftTestingGowers.lean 12 declarations
ShiftedAdaptedIdeal.lean 7 declarations
ShiftedGradedCalculus.lean 64 declarations
ShiftedProductTestError.lean 17 declarations
ShiftedSiteCoverTilt.lean 1 declarations
ShiftedSmoothProductAmplitudeTransfer.lean 4 declarations
ShiftedSmoothSelectedMarginal.lean 30 declarations
ShiftedVerticalExpansion.lean 4 declarations
ShortConditionedCubeAxis.lean 2 declarations
SigmaAxisOperator.lean 8 declarations
SigmaProductPeriodization.lean 5 declarations
SigmaWeightDerivative.lean 5 declarations
SimultaneousAxisCompression.lean 1 declarations
SimultaneousDirichlet.lean 3 declarations
SimultaneousSymbolSplitting.lean 7 declarations
SitePlateauCutoff.lean 8 declarations
SiteTwistCommonModulus.lean 50 declarations
SlicedOneCubeSiteExpansion.lean 2 declarations
SlicedPairAmplitude.lean 27 declarations
SlicedPrincipalInverse.lean 15 declarations
SlicedSourceAccuracy.lean 3 declarations
SlicedSourceUniformAccuracy.lean 1 declarations
SlicedToleranceMonotonicity.lean 6 declarations
SlicedUniformTailTolerance.lean 3 declarations
SlowInverseControl.lean 1 declarations
SmallDifferenceGrowth.lean 1 declarations
SmallWeightedPhysicalReplacement.lean 23 declarations
SmoothCoefficientSlice.lean 21 declarations
SmoothHalfspaceCutoff.lean 8 declarations
SmoothModerateBlockBounds.lean 1 declarations
SmoothPairErrorLogBounds.lean 31 declarations
SmoothProfileReindexing.lean 4 declarations
SmoothSublevelCutoff.lean 9 declarations
SmoothWindowChange.lean 8 declarations
SmoothedImageTest.lean 7 declarations
SortedPositiveWeights.lean 1 declarations
SourceDetectionError.lean 1 declarations
SourceUnitCover.lean 33 declarations
SpecifiedSquareObservable.lean 1 declarations
SpectralCylinderDecomposition.lean 1 declarations
SplitGroupRelative.lean 6 declarations
SplitPivotParameter.lean 2 declarations
SplitSmoothProductProfile.lean 52 declarations
SquareGradedRelative.lean 49 declarations
SquareRationalModel.lean 4 declarations
SquareStructureHeight.lean 4 declarations
SquareSymbolRelative.lean 15 declarations
SquarefreeAdaptedLieAlgebra.lean 3 declarations
SquarefreeCoefficients.lean 6 declarations
SquarefreeExponents.lean 7 declarations
SquarefreeLayerBases.lean 6 declarations
SquarefreePermutationFiltration.lean 63 declarations
SquarefreeQuotientAction.lean 7 declarations
SquarefreeRealAction.lean 33 declarations
SquarefreeSplitCount.lean 34 declarations
SquarefreeStructureHeight.lean 2 declarations
StableReferenceMean.lean 5 declarations
StableRetainedAtom.lean 4 declarations
StableSiteSectionLengths.lean 2 declarations
StepDropTerminalContainment.lean 27 declarations
StepOneSymbolLinearPart.lean 10 declarations
StrideProductBounds.lean 24 declarations
StrongRefiltrationReconstruction.lean 32 declarations
SublevelThresholdBalance.lean 1 declarations
SubmoduleSupRestriction.lean 1 declarations
SubsetAlternatingInversion.lean 3 declarations
SubspaceLayeredModeSmoothRemoval.lean 27 declarations
SymbolAbsorptionBounds.lean 39 declarations
SymbolCommonCorrections.lean 20 declarations
SymbolFastMembership.lean 28 declarations
SymmetricCubeSublevel.lean 2 declarations
SymmetricCubeVolume.lean 4 declarations
SymmetricEvaluationLowerBound.lean 14 declarations
SymmetricIntervalDilation.lean 2 declarations
SymmetricScalarSublevel.lean 5 declarations
SymmetricSquarefreeMonotonicity.lean 24 declarations
TaggedZModOrderBounds.lean 5 declarations
TailReflectionInduction.lean 12 declarations
TangentModelVector.lean 1 declarations
TemperaturePrimitiveNormal.lean 2 declarations
TensorContraction.lean 5 declarations
TensorSquarePairComparison.lean 18 declarations
TerminalControlledFactorization.lean 15 declarations
TranslatedCyclicDetection.lean 2 declarations
TranslatedLocalAverage.lean 1 declarations
TranslatedSelectedNormalization.lean 1 declarations
TranslatedSelectedOneSite.lean 1 declarations
TranslatedShiftTesting.lean 9 declarations
TranslatedStabilityStep.lean 4 declarations
TranslationLogSlowNormalization.lean 6 declarations
TranslationMajorCorrelationDecomposition.lean 15 declarations
TranslationMajorCorrelationIdentity.lean 28 declarations
TranslationMajorTwistedCorrelationStepDrop.lean 23 declarations
TranslationShearExponentialOver.lean 3 declarations
TriangularCorrectionRows.lean 6 declarations
TruncatedSeries.lean 20 declarations
TruncatedSeriesFiltration.lean 4 declarations
TwoDownsetPrecision.lean 8 declarations
UnconditionalStepDrop.lean 13 declarations
UnconditionedAbsolutePatchFamily.lean 1 declarations
UnconditionedArbitraryFixedPatchFamily.lean 12 declarations
UnconditionedArbitraryNormalizedBase.lean 1 declarations
UnconditionedCommonSideScalarRatioBounds.lean 1 declarations
UnconditionedFixedPatchFamily.lean 4 declarations
UnconditionedSmoothSlopeCap.lean 6 declarations
UnconditionedTrimmedSliceFamily.lean 7 declarations
UniformCommutingCircleDecomposition.lean 21 declarations
UniformControlledCurrentStage.lean 2 declarations
UniformControlledNativeExternalNetsOfRecovery.lean 30 declarations
UniformFamilyMemberNet.lean 8 declarations
UniformFastCoefficientSpec.lean 2 declarations
UniformFiniteMarkedFactorParameters.lean 10 declarations
UniformFormalCurrentLayerStep.lean 17 declarations
UniformFrozenDescent.lean 12 declarations
UniformHomFiberWeights.lean 1 declarations
UniformIntegralSeries.lean 1 declarations
UniformParameterNet.lean 1 declarations
UniformPhysicalStackConstruction.lean 1 declarations
UniformPhysicalVisitBounds.lean 13 declarations
UniformProductAccuracy.lean 7 declarations
UniformProductAccuracyLogBounds.lean 4 declarations
UniformProfileRadiusLog.lean 8 declarations
UniformRegularizedProfileComparison.lean 6 declarations
UniformRelativePatchSource.lean 22 declarations
UniformRestrictedMean.lean 1 declarations
UniformScaledRetainedLogBounds.lean 13 declarations
UniformStridedBlockEntry.lean 4 declarations
UnitBoundProductDifference.lean 2 declarations
UnitCoefficientSourceMarginal.lean 12 declarations
UnitExpansionCorrelation.lean 9 declarations
UnitProductOrbitFamily.lean 3 declarations
UnitRangeLocalLipschitz.lean 1 declarations
UnitTestClipping.lean 6 declarations
UnitVerticalCyclicDifference.lean 31 declarations
UnitVerticalDifference.lean 8 declarations
UnitVerticalMeanRowCorrelation.lean 23 declarations
UnitVerticalNativeInverseModels.lean 17 declarations
UnnormalizedCommonSymbolFactorization.lean 34 declarations
UnnormalizedTensorL1.lean 1 declarations
VectorAlgebraicMajorDecomposition.lean 34 declarations
VectorApproximationPrecomposition.lean 7 declarations
VectorCoefficientScaling.lean 3 declarations
VectorHomogenization.lean 7 declarations
VectorRealSubstitutionBound.lean 4 declarations
VectorSubspaceCorrectionRepresentatives.lean 11 declarations
VerticalTranslations.lean 1 declarations
WeightedApproximationCaps.lean 3 declarations
WeightedAxisScaling.lean 20 declarations
WeightedCenteredExpansion.lean 2 declarations
WeightedCoefficientSplit.lean 1 declarations
WeightedCubeNativeDetection.lean 1 declarations
WeightedCubePlateau.lean 12 declarations
WeightedDerivationDrop.lean 8 declarations
WeightedFundamentalApproximation.lean 2 declarations
WeightedImageDerivative.lean 9 declarations
WeightedLinearBounds.lean 1 declarations
WeightedListError.lean 2 declarations
WeightedLoweringAction.lean 7 declarations
WeightedLoweringGroup.lean 24 declarations
WeightedLoweringTriangular.lean 3 declarations
WeightedOrbitNormalization.lean 23 declarations
WeightedOverlapCorrelation.lean 10 declarations
WeightedPatchReparam.lean 27 declarations
WeightedPlateauSiteApproximation.lean 31 declarations
WeightedRetainedCoefficients.lean 12 declarations
WeightedRudin.lean 4 declarations
WeightedSmoothSampledError.lean 11 declarations
WeightedSummandCorrelation.lean 11 declarations
WeightedTestComparison.lean 1 declarations
WeightedTranslationAssociatedGraded.lean 5 declarations
WeightedTranslationBaseGrading.lean 21 declarations
WeightedTranslationCentralCircleAction.lean 6 declarations
WeightedTranslationCentralTop.lean 3 declarations
WeightedTranslationRealPureFactors.lean 12 declarations
WeightedTranslationShearExponential.lean 62 declarations
WeightedTranslationStructureConstants.lean 5 declarations
WeightedTwistedTranslationLipschitz.lean 8 declarations
ZeroBasedExtremalSet.lean 1 declarations