`OAI/MeasureTheory/Falconer/Estimates/`

2154 declarations, 0 contain sorry, 0 declared as axioms; 629 files

Files

ActualClassFamilies.lean 2 declarations
ActualClassMass.lean 6 declarations
ActualComparableDepthSum.lean 1 declarations
ActualComparableFarError.lean 2 declarations
ActualDirectBuffer.lean 2 declarations
ActualDistanceEquation12.lean 1 declarations
ActualDistanceEquation20.lean 2 declarations
ActualDistanceEstimate.lean 1 declarations
ActualDistanceTerminal.lean 2 declarations
ActualFarBuffer.lean 4 declarations
ActualFarEquation24.lean 1 declarations
ActualFarPower.lean 1 declarations
ActualFarSourceBuffer.lean 1 declarations
ActualFarSourceEquation24.lean 1 declarations
ActualFarSpatialError.lean 1 declarations
ActualNoncomparableFar.lean 2 declarations
ActualNoncomparableMain.lean 1 declarations
ActualNoncomparableSpatial.lean 1 declarations
ActualOuterMasks.lean 12 declarations
ActualProductEquation13.lean 1 declarations
ActualProductEstimate.lean 1 declarations
ActualRegularizedClasses.lean 2 declarations
ActualRootEquation21.lean 1 declarations
ActualSuccessorUpperBounds.lean 10 declarations
ActualTransformSplitting.lean 3 declarations
ActualTwoPointDerivatives.lean 1 declarations
AdaptedFailure.lean 2 declarations
AllDimensionalMain.lean 1 declarations
AllDimensionalOccupiedClasses.lean 4 declarations
AllDimensionalParallelExceptional.lean 1 declarations
AllDimensionalRegularizationCardinality.lean 5 declarations
AllDimensionalRegularizationLabels.lean 14 declarations
AllDimensions.lean 17 declarations
AllTestsRestoration.lean 5 declarations
AnchoredBufferedMasks.lean 6 declarations
AnchoredMasks.lean 8 declarations
AnchoredPairFailure.lean 10 declarations
Assembly.lean 8 declarations
Availability.lean 11 declarations
BadTriplePower.lean 2 declarations
BadTripleRelation.lean 5 declarations
BuildRegularRefinement.lean 2 declarations
CellClassifier.lean 9 declarations
CellwisePairDeletion.lean 3 declarations
CenteredPacketGain.lean 1 declarations
CenteredPacketPower.lean 1 declarations
ChargedPlane.lean 1 declarations
ChildRetention.lean 2 declarations
ClassBadRecombination.lean 1 declarations
ClassPairCandidate.lean 8 declarations
ClassPairWeights.lean 2 declarations
ClassPruning.lean 8 declarations
ClassRecombination.lean 4 declarations
CoarseFloorPowers.lean 2 declarations
CoarseFreezingBudget.lean 3 declarations
CoarsePlanarRounding.lean 8 declarations
CollisionFubini.lean 2 declarations
CommonRegularFamily.lean 2 declarations
CommonRegularReference.lean 1 declarations
CommonTubeKernel.lean 4 declarations
CommonTubePacking.lean 2 declarations
CommonTubePower.lean 2 declarations
CommonUnbalancedReference.lean 1 declarations
ComparableBands.lean 9 declarations
ComparableComplexRebin.lean 1 declarations
ComparableContributionPartition.lean 1 declarations
ComparablePositiveRebin.lean 3 declarations
ComparableProfileFactor.lean 1 declarations
ConditionalCollision.lean 2 declarations
ConditionalPlanar.lean 4 declarations
ConeSections.lean 10 declarations
ControlledEndpointGain.lean 1 declarations
CriticalScale.lean 2 declarations
CrossOriginalKernel.lean 1 declarations
DescriptorAmbient.lean 8 declarations
DescriptorEnvelope.lean 11 declarations
DescriptorExceptional.lean 1 declarations
DescriptorFiberBad.lean 3 declarations
DescriptorInverseFactors.lean 1 declarations
DescriptorInverseRegime.lean 8 declarations
DescriptorMaskExceptional.lean 1 declarations
DescriptorMasks.lean 14 declarations
DescriptorPairBudget.lean 3 declarations
DescriptorRemoval.lean 2 declarations
DescriptorScaledKernel.lean 3 declarations
DescriptorSeededInverse.lean 5 declarations
DescriptorTestBad.lean 3 declarations
DescriptorTests.lean 6 declarations
DilationNoncharging.lean 2 declarations
DimensionDescent.lean 2 declarations
DirectedPacketRows.lean 1 declarations
DirectedSampledRows.lean 1 declarations
DistanceActivityStrip.lean 4 declarations
DistanceCandidateWidth.lean 2 declarations
DistanceEligibleIndices.lean 6 declarations
DistanceForm.lean 7 declarations
DistanceFormFubini.lean 6 declarations
DistanceFormRemoval.lean 4 declarations
DistanceMatrixData.lean 8 declarations
DistanceOccupiedSum.lean 5 declarations
DistanceProfileFactor.lean 2 declarations
DistanceWeightSum.lean 2 declarations
DominatedBand.lean 1 declarations
DyadicAncestors.lean 4 declarations
DyadicAveraging.lean 12 declarations
DyadicCells.lean 7 declarations
DyadicCenters.lean 7 declarations
DyadicDisplacements.lean 4 declarations
DyadicEnergyStep.lean 1 declarations
DyadicFailedTests.lean 2 declarations
DyadicLinearApproximation.lean 3 declarations
DyadicLocalGain.lean 1 declarations
DyadicLocalization.lean 1 declarations
DyadicLossAbsorption.lean 2 declarations
DyadicPolynomialBudget.lean 2 declarations
DyadicSecantError.lean 7 declarations
DyadicSlopeEnergy.lean 8 declarations
DyadicSlopeVariance.lean 8 declarations
DyadicTree.lean 16 declarations
Eligibility.lean 6 declarations
EligibilityExcision.lean 4 declarations
EndpointApplicationNumerics.lean 4 declarations
EndpointAvailabilityGain.lean 1 declarations
EndpointBadTriples.lean 1 declarations
EndpointCoarsening.lean 6 declarations
EndpointCountBudget.lean 2 declarations
EndpointDyadicScale.lean 4 declarations
EndpointOneScale.lean 1 declarations
EndpointOrientedGain.lean 1 declarations
EndpointOriginalMiddle.lean 1 declarations
EndpointPowerAbsorption.lean 2 declarations
EndpointRowBudget.lean 3 declarations
EndpointScaleInputs.lean 2 declarations
EndpointSelectionLift.lean 2 declarations
EndpointSelectionLosses.lean 3 declarations
EndpointSphericalPreparation.lean 1 declarations
EndpointSubprobability.lean 1 declarations
EndpointTwoSidedScale.lean 1 declarations
EnergyOriginalKernel.lean 1 declarations
EnergySplitting.lean 6 declarations
EvenPreparation.lean 1 declarations
FarCellCount.lean 5 declarations
FarComparableSplit.lean 2 declarations
FarData.lean 12 declarations
FarDataBound.lean 1 declarations
FarEnvelope.lean 6 declarations
FarError.lean 4 declarations
FarErrorOrder.lean 2 declarations
FarKernelDataEstimates.lean 3 declarations
FarOriginalPartition.lean 2 declarations
FarPolicyScales.lean 3 declarations
FarRebin.lean 1 declarations
FarRegionScales.lean 5 declarations
FarRegionSplit.lean 6 declarations
FiberRegularityBudget.lean 3 declarations
FilteredLimit.lean 8 declarations
FinePacketCounts.lean 4 declarations
FiniteAnchorLabels.lean 6 declarations
FiniteCellwiseCollision.lean 2 declarations
FiniteClassFactors.lean 6 declarations
FiniteEnergyRegularity.lean 5 declarations
FiniteFamilyOverlap.lean 3 declarations
FiniteHolder.lean 1 declarations
FiniteNearbyImages.lean 3 declarations
FiniteOverlap.lean 2 declarations
FinitePartitionMask.lean 5 declarations
FinitePopularity.lean 4 declarations
FiniteSquareIntegrable.lean 1 declarations
FiniteTripleCounting.lean 1 declarations
FirstExclusionShift.lean 1 declarations
FiveInputsMain.lean 1 declarations
FourInputsMain.lean 1 declarations
FourPointPartition.lean 5 declarations
FrechetCompositionScale.lean 5 declarations
FrechetProductScale.lean 2 declarations
GeneralColumns.lean 10 declarations
GeneralRegularFineGain.lean 1 declarations
GeneralRegularSetAlternative.lean 1 declarations
GeneralTransverseCount.lean 2 declarations
GeometricRegularFiber.lean 1 declarations
GlobalDescriptorBounds.lean 4 declarations
GoodCoarseRows.lean 1 declarations
GoodRegularFiber.lean 1 declarations
GoodRowSelection.lean 1 declarations
GoodRowSelectionAE.lean 1 declarations
IidSampling.lean 13 declarations
InactivePairMass.lean 3 declarations
IncidentCoarseRounding.lean 5 declarations
IndependentClassEquation27.lean 1 declarations
IntermediateProfiles.lean 6 declarations
InterpolatedTubeKernel.lean 2 declarations
InverseBudget.lean 2 declarations
InverseClassExpansion.lean 8 declarations
InverseLeibniz.lean 5 declarations
InversePowerSum.lean 2 declarations
InverseScalarPullout.lean 3 declarations
InverseScale.lean 1 declarations
KernelL1Comparison.lean 3 declarations
LaplacianBounds.lean 15 declarations
LaplacianIsometry.lean 5 declarations
LinearNonstationary.lean 2 declarations
LinearPieces.lean 2 declarations
ListBoundedFunctions.lean 1 declarations
LocalCellLines.lean 10 declarations
LocalInverse.lean 7 declarations
LocalLineResolution.lean 1 declarations
LocalPacketRegularity.lean 5 declarations
LocalPacketRows.lean 4 declarations
LocalPrefixCenters.lean 2 declarations
LocalizationSum.lean 1 declarations
MaskLoss.lean 3 declarations
MaskedInverseRemainder.lean 1 declarations
MaskedLowBand.lean 1 declarations
MaskedNested.lean 1 declarations
MixedComposition.lean 4 declarations
MixedMaskBounds.lean 2 declarations
MonotoneLowpass.lean 18 declarations
NearFarSplit.lean 3 declarations
NearPinDeletion.lean 4 declarations
NoncomparableCommonBound.lean 2 declarations
NoncomparableKernelScale.lean 5 declarations
NoncomparableOriginalPointwise.lean 3 declarations
NoncomparablePower.lean 1 declarations
NonendpointAvailabilityGain.lean 1 declarations
NonendpointOneScale.lean 1 declarations
NonendpointOriginalMiddle.lean 1 declarations
NonendpointTwoSidedScale.lean 1 declarations
NonstationaryPower.lean 3 declarations
NonstationaryScales.lean 2 declarations
OccupiedClasses.lean 4 declarations
OccupiedPacking.lean 2 declarations
OddDescent.lean 1 declarations
OddNonchargingPreparation.lean 1 declarations
OddPreparedPair.lean 2 declarations
OddProjectedPieces.lean 1 declarations
OffPoleAmbient.lean 5 declarations
OneInputMain.lean 1 declarations
OneScaleParameters.lean 1 declarations
OrderedLeibniz.lean 9 declarations
OriginalPairFilter.lean 6 declarations
OriginalWeakCosts.lean 2 declarations
OuterChildProfileBound.lean 2 declarations
OuterDescriptors.lean 6 declarations
OuterEntryProfile.lean 1 declarations
OuterMaskFailure.lean 5 declarations
OuterParameters.lean 1 declarations
OuterRestrictedConversion.lean 2 declarations
OuterRootEquation21.lean 4 declarations
OuterRootGain.lean 6 declarations
OuterScalarConversion.lean 2 declarations
PacketCardinalityScales.lean 2 declarations
PacketCentering.lean 13 declarations
PacketGoodRegularFiber.lean 1 declarations
PacketGrowthGap.lean 1 declarations
PacketLocalEnergyGain.lean 1 declarations
PacketLogBounds.lean 4 declarations
PacketParameterBounds.lean 1 declarations
PacketPolynomialLoss.lean 1 declarations
PacketRepresentativeBand.lean 1 declarations
PacketResidualRows.lean 2 declarations
PacketSamplingBudget.lean 1 declarations
PacketScaleCombination.lean 2 declarations
Packing.lean 3 declarations
PairExceptional.lean 4 declarations
ParallelCandidateCount.lean 3 declarations
ParallelCount.lean 1 declarations
ParallelExceptional.lean 3 declarations
ParallelGood.lean 5 declarations
ParallelMean.lean 3 declarations
ParallelNumerics.lean 3 declarations
ParallelScaleMean.lean 1 declarations
ParentChildRetention.lean 1 declarations
ParentPrefixRetention.lean 1 declarations
ParentRefinedEndpointSelection.lean 1 declarations
PatchedInverseFactors.lean 8 declarations
PathDifferenceBound.lean 2 declarations
PlanarCommonBudget.lean 1 declarations
PlanarGain.lean 1 declarations
PlanarGainNumerics.lean 6 declarations
PlanarLossBudget.lean 2 declarations
PlanarPathCenters.lean 1 declarations
PlanarPrefixTruncation.lean 4 declarations
PlanarQuarter.lean 7 declarations
PlanarSampling.lean 12 declarations
PlanarSelectedGain.lean 3 declarations
PlanarSquash.lean 11 declarations
PlanarTreeUniformization.lean 3 declarations
PlanarWeakParameters.lean 1 declarations
PointClassRatios.lean 1 declarations
PointSamples.lean 5 declarations
PolicyCommonBudgets.lean 5 declarations
PolicyEnergy.lean 9 declarations
PolicyEnergyInduction.lean 2 declarations
PolicyEnergySteps.lean 3 declarations
PolicyFarCoefficients.lean 5 declarations
PolicyFarRecurrence.lean 1 declarations
PolicyFarStep.lean 3 declarations
PolicyLowBand.lean 3 declarations
PolicyPrefixLowpass.lean 1 declarations
PolicyPrefixScales.lean 2 declarations
PolicyRootApplication.lean 2 declarations
PolicyRootCoefficient.lean 4 declarations
PolicyRootDecay.lean 1 declarations
PolicyScalarConversion.lean 1 declarations
PolicySuffixRecurrence.lean 3 declarations
PopularRegularity.lean 2 declarations
PositiveDistanceGoodSet.lean 5 declarations
PositiveDistanceJetSupport.lean 3 declarations
PositiveDistanceMasks.lean 5 declarations
PositiveDistanceOriginalSpatial.lean 5 declarations
PositiveDistancePushforward.lean 19 declarations
PositiveDistanceRebinBound.lean 4 declarations
PositiveDistanceWeight.lean 10 declarations
PrefixCenters.lean 7 declarations
PrefixCounting.lean 10 declarations
PrefixRetention.lean 1 declarations
PreparedPair.lean 2 declarations
ProductCandidateWidth.lean 2 declarations
ProductMatrix.lean 8 declarations
ProductMatrixIntegrand.lean 3 declarations
ProductMatrixReindex.lean 2 declarations
ProductOccupiedCount.lean 2 declarations
ProductOccupiedIntegrand.lean 2 declarations
ProductOccupiedSum.lean 2 declarations
ProductOccupiedVertices.lean 5 declarations
ProductTransformPartition.lean 4 declarations
ProductWeightSum.lean 3 declarations
ProfileAffine.lean 3 declarations
ProfileEnvelopes.lean 4 declarations
ProfileInterpolation.lean 14 declarations
ProfileMassError.lean 2 declarations
ProfilePacking.lean 1 declarations
ProjectedCompactPieces.lean 2 declarations
ProjectedIndependentTuples.lean 3 declarations
ProjectedPacketRows.lean 7 declarations
ProjectedPair.lean 3 declarations
ProjectedSubsetRegularity.lean 1 declarations
PrunedVariation.lean 5 declarations
Published.lean 4 declarations
QuadraticBudget.lean 6 declarations
QuadraticCoefficients.lean 2 declarations
QuadraticDampingLimit.lean 4 declarations
QuadraticDifferential.lean 8 declarations
QuadraticDischarge.lean 2 declarations
QuadraticTaylorRemainder.lean 4 declarations
QuantitativeDifferentiation.lean 2 declarations
QuantitativePacketPoints.lean 1 declarations
QuarterEndpointMap.lean 9 declarations
ReachedMasks.lean 4 declarations
ReducedInputsMain.lean 1 declarations
RefinedEndpointSelection.lean 2 declarations
RefinedPlanarClass.lean 1 declarations
RegularCellConfiguration.lean 1 declarations
RegularClassSmallTrouble.lean 1 declarations
RegularClasses.lean 3 declarations
RegularCoarseCells.lean 2 declarations
RegularCoarsePreparation.lean 1 declarations
RegularFineGain.lean 1 declarations
RegularListRestoration.lean 1 declarations
RegularOuterMask.lean 4 declarations
RegularRefinementBound.lean 1 declarations
RegularRefinementContradiction.lean 1 declarations
RegularRefinementData.lean 1 declarations
RegularRefinementPreparation.lean 1 declarations
RegularRoot.lean 6 declarations
RegularScaleCoefficients.lean 3 declarations
RegularSetAlternative.lean 1 declarations
RegularSourceClasses.lean 1 declarations
RegularizationCardinality.lean 5 declarations
RegularizationClasses.lean 18 declarations
RegularizationCount.lean 3 declarations
RegularizationLabels.lean 14 declarations
RegularizationPairBounds.lean 4 declarations
RegularizationPairMask.lean 5 declarations
RegularizationProperties.lean 6 declarations
RegularizationQuantifiers.lean 1 declarations
RegularizationScales.lean 4 declarations
RegularizationSelection.lean 8 declarations
RegularizationSubpower.lean 4 declarations
RegularizationTestBad.lean 5 declarations
RegularizationVariation.lean 3 declarations
RegularizedCellCounts.lean 4 declarations
RegularizedMass.lean 3 declarations
RelativePairCore.lean 3 declarations
RelativeRegularizationGain.lean 1 declarations
RescaledCellPackets.lean 1 declarations
RescaledConditional.lean 6 declarations
RestorationSeries.lean 4 declarations
RetainedEnergy.lean 1 declarations
RetainedPairs.lean 10 declarations
RetainedRegularCells.lean 1 declarations
RetainedTubeTest.lean 2 declarations
ReverseLawTransfer.lean 2 declarations
RootCoefficientSubpower.lean 1 declarations
RootEquation21.lean 1 declarations
RootFiniteSeparation.lean 1 declarations
RootLeibniz.lean 9 declarations
RootLeibnizBounds.lean 6 declarations
RootPairDerivatives.lean 1 declarations
RootSpatialTerms.lean 4 declarations
RootSupremum.lean 4 declarations
RootWeightedDistance.lean 8 declarations
RootWeightedInverse.lean 1 declarations
RotatedInverse.lean 6 declarations
RotatedInverseCoefficient.lean 5 declarations
RotatedInverseCost.lean 2 declarations
RotatedInverseExpansion.lean 5 declarations
RotatedInverseRemainder.lean 1 declarations
RotatedInverseScalar.lean 2 declarations
RotatedLaws.lean 9 declarations
RotatedMaskedRemainder.lean 1 declarations
RotatedNonstationary.lean 2 declarations
RotatedTubeData.lean 6 declarations
RotatedWeightedInverse.lean 4 declarations
RoundedEndpointGain.lean 1 declarations
RoundedPlanarObstruction.lean 1 declarations
RowRegularity.lean 1 declarations
SampledPacketRows.lean 1 declarations
SampledRowCardinality.lean 2 declarations
SamplingScales.lean 5 declarations
SamplingTail.lean 6 declarations
ScalarActualClusterGain.lean 1 declarations
ScalarActualPorousGain.lean 1 declarations
ScalarBinaryEmbedding.lean 1 declarations
ScalarBinaryGeometric.lean 4 declarations
ScalarBinaryGrowth.lean 1 declarations
ScalarBinaryParameters.lean 5 declarations
ScalarBoundedCoefficients.lean 1 declarations
ScalarBunchBudget.lean 2 declarations
ScalarBunchClusterTree.lean 1 declarations
ScalarBunchMargins.lean 3 declarations
ScalarBunchSizes.lean 5 declarations
ScalarBunchTransfer.lean 3 declarations
ScalarBunchTree.lean 7 declarations
ScalarBunchedPrefix.lean 2 declarations
ScalarBunchingSuffix.lean 7 declarations
ScalarBunchingTotals.lean 5 declarations
ScalarChildChoice.lean 2 declarations
ScalarClosestScale.lean 3 declarations
ScalarClusterBunching.lean 1 declarations
ScalarClusterGain.lean 2 declarations
ScalarClusterPathTree.lean 2 declarations
ScalarClusterPorousGain.lean 1 declarations
ScalarClusterSums.lean 3 declarations
ScalarClusterTree.lean 4 declarations
ScalarClusterWeights.lean 3 declarations
ScalarCoefficientAdd.lean 1 declarations
ScalarCoefficientBudget.lean 5 declarations
ScalarCoefficientClosure.lean 4 declarations
ScalarCoefficientExpressions.lean 4 declarations
ScalarCoefficientLogBudget.lean 3 declarations
ScalarCoefficientMul.lean 1 declarations
ScalarCoefficientNeg.lean 1 declarations
ScalarCollisionKernel.lean 6 declarations
ScalarCompressedBunching.lean 3 declarations
ScalarCompressedLevels.lean 5 declarations
ScalarCorrelatedWeights.lean 5 declarations
ScalarDenseGroup.lean 1 declarations
ScalarDifferenceDoubling.lean 1 declarations
ScalarDilatedRefinement.lean 3 declarations
ScalarDilationBound.lean 2 declarations
ScalarDivideBudget.lean 4 declarations
ScalarDivideCoefficient.lean 2 declarations
ScalarDyadicPowers.lean 3 declarations
ScalarEnergyRefinement.lean 3 declarations
ScalarErrorBudget.lean 2 declarations
ScalarForkSumset.lean 1 declarations
ScalarForwardRegularization.lean 2 declarations
ScalarGreedyPorousGain.lean 1 declarations
ScalarGroupOverlap.lean 1 declarations
ScalarGroupReverseOverlap.lean 1 declarations
ScalarGroupedGain.lean 1 declarations
ScalarGroupedHalfGain.lean 1 declarations
ScalarGroupedPaths.lean 3 declarations
ScalarGroupedTreeGain.lean 2 declarations
ScalarGroupedWeights.lean 1 declarations
ScalarIncrementSelection.lean 1 declarations
ScalarInitialChildren.lean 2 declarations
ScalarInitialDyadic.lean 1 declarations
ScalarInitialGrowth.lean 2 declarations
ScalarInitialPathChildren.lean 1 declarations
ScalarInitialRegularization.lean 1 declarations
ScalarInverseTransfer.lean 1 declarations
ScalarLevelEnumeration.lean 3 declarations
ScalarLogAverages.lean 10 declarations
ScalarLossAbsorption.lean 3 declarations
ScalarMixedRefinement.lean 2 declarations
ScalarNonporousDoubling.lean 1 declarations
ScalarNonporousEntropy.lean 3 declarations
ScalarNonporousFraction.lean 1 declarations
ScalarNonporousGrowth.lean 1 declarations
ScalarNonporousPowers.lean 6 declarations
ScalarNonporousTail.lean 3 declarations
ScalarPairGrouping.lean 1 declarations
ScalarParameterChoice.lean 1 declarations
ScalarPartialSums.lean 5 declarations
ScalarPathCenters.lean 7 declarations
ScalarPathLevel.lean 7 declarations
ScalarPathNodes.lean 12 declarations
ScalarPluennecke.lean 1 declarations
ScalarPointPaths.lean 7 declarations
ScalarPorousEndpoints.lean 1 declarations
ScalarPorousGroupingGain.lean 2 declarations
ScalarPorousGrowth.lean 1 declarations
ScalarPorousLevel.lean 2 declarations
ScalarPorousLevels.lean 7 declarations
ScalarPorousTreeGain.lean 2 declarations
ScalarPrefixEntropy.lean 3 declarations
ScalarPrefixNonconcentration.lean 3 declarations
ScalarPrefixTruncation.lean 6 declarations
ScalarRatioCard.lean 2 declarations
ScalarRatioFamily.lean 3 declarations
ScalarRatioTransfer.lean 2 declarations
ScalarReferenceObstruction.lean 2 declarations
ScalarRegularizationBudget.lean 2 declarations
ScalarRegularizedGrowth.lean 1 declarations
ScalarRepeatedSums.lean 3 declarations
ScalarResolution.lean 2 declarations
ScalarRestrictedSums.lean 1 declarations
ScalarReverseGroupedGain.lean 1 declarations
ScalarReverseGroupedHalfGain.lean 1 declarations
ScalarReverseGroupedWeights.lean 1 declarations
ScalarReverseWeights.lean 3 declarations
ScalarRounding.lean 7 declarations
ScalarRoundingScale.lean 1 declarations
ScalarRuzsa.lean 4 declarations
ScalarScaleAlignment.lean 3 declarations
ScalarScaledCard.lean 2 declarations
ScalarSelectedForks.lean 3 declarations
ScalarSeparatedPathTree.lean 1 declarations
ScalarSeparatedTree.lean 4 declarations
ScalarSignedRuzsa.lean 3 declarations
ScalarSingletonFibers.lean 1 declarations
ScalarSubsetTransfer.lean 3 declarations
ScalarSumCells.lean 6 declarations
ScalarSumsetLogBound.lean 2 declarations
ScalarSumsetPacking.lean 1 declarations
ScalarSwitchProgression.lean 5 declarations
ScalarSwitchSums.lean 5 declarations
ScalarTaggedPrefix.lean 4 declarations
ScalarTreeAmplification.lean 2 declarations
ScalarTreeUniformization.lean 3 declarations
ScalarUnbalancedRefinement.lean 2 declarations
ScalarUniformTrim.lean 1 declarations
ScalarWeakReference.lean 1 declarations
ScalarWeakRefinement.lean 2 declarations
ScalarWeakScaleParameters.lean 1 declarations
ScalarWeakToUniform.lean 1 declarations
ScalarZoom.lean 6 declarations
ScalarZoomBounds.lean 2 declarations
ScaleThinning.lean 2 declarations
ScaleUniformNonstationary.lean 2 declarations
ScaledInverseRemainder.lean 4 declarations
ScaledWeightedInverse.lean 5 declarations
ScopedMaskVariation.lean 1 declarations
SeededInverse.lean 9 declarations
SelectBoundedCommonTriple.lean 1 declarations
SelectCommonTriple.lean 1 declarations
SelectedDistanceAssembly.lean 6 declarations
SelectedRegularFiber.lean 2 declarations
SeparatedInverse.lean 9 declarations
SeparatedThinning.lean 1 declarations
SevenInputsMain.lean 1 declarations
SignedConvolution.lean 4 declarations
SixInputsMain.lean 2 declarations
SliceAverage.lean 17 declarations
SmallUnionLogs.lean 2 declarations
SmoothCompositionScale.lean 9 declarations
SmoothConvolution.lean 6 declarations
SourceAssemblyParameters.lean 3 declarations
SourceClassMiddleData.lean 1 declarations
SourceClassOriginalLaws.lean 4 declarations
SourceCollisionMultiplication.lean 1 declarations
SourceFamily.lean 1 declarations
SourceProfileEquation25.lean 2 declarations
SourceRelativeRegularization.lean 1 declarations
SourceRepresentatives.lean 1 declarations
SourceStateTerminal.lean 3 declarations
SourceStrongSeparation.lean 2 declarations
SpatialAnchorMasks.lean 8 declarations
SpatialAnnulusKernel.lean 7 declarations
SpatialDistanceFormSeparation.lean 1 declarations
SpatialEndpoint.lean 2 declarations
SpatialEndpointFamily.lean 4 declarations
SpatialLeibnizSubpower.lean 3 declarations
SpatialPhasedDistanceForm.lean 2 declarations
SpatialPlancherel.lean 2 declarations
SpatialSharedBound.lean 1 declarations
SpatialSharedRegularity.lean 2 declarations
SphericalEnergy.lean 11 declarations
SquashGainBudget.lean 1 declarations
StartingDescent.lean 1 declarations
StartingPreparation.lean 1 declarations
SuffixCollision.lean 4 declarations
SuffixGrouping.lean 7 declarations
SuffixReduction.lean 1 declarations
SuffixScales.lean 8 declarations
TestWidths.lean 9 declarations
ThreeInputsMain.lean 1 declarations
ThreeTubePullback.lean 1 declarations
TransversePhysicalCount.lean 1 declarations
TripleColumns.lean 9 declarations
TripleGram.lean 9 declarations
TripleGramStability.lean 5 declarations
TroublesomePair.lean 6 declarations
TruncatedDyadicBound.lean 1 declarations
TubePacketDilation.lean 11 declarations
TubeSecondMoment.lean 5 declarations
TubeUniformization.lean 2 declarations
TwoInputsMain.lean 1 declarations
TwoPolicyEnergy.lean 8 declarations
TwoProjectedLaws.lean 1 declarations
TwoScaleRatio.lean 2 declarations
UniformDescriptorFactors.lean 1 declarations
UniformDescriptorFamily.lean 1 declarations
UniformLowerPlanes.lean 2 declarations
UniformPacketBounds.lean 1 declarations
UniformSamples.lean 5 declarations
UniformScaleCombination.lean 1 declarations
ValidDescriptors.lean 3 declarations
WeightedCauchy.lean 1 declarations
WeightedCubicMoment.lean 1 declarations
WeightedDistanceNestedDomination.lean 2 declarations
WeightedDistanceNestedSupport.lean 1 declarations
WeightedDistancePushforward.lean 9 declarations
WeightedDistanceSourceMapping.lean 3 declarations
WeightedDyadicRegularity.lean 1 declarations
WeightedInverse.lean 3 declarations
WeightedLowpass.lean 8 declarations