OAI/NumberTheory/JointDickman/Probability/
825 declarations, 0 contain sorry, 0 declared as axioms; 186 files
Files
- AmplificationFairKernel.lean 5 declarations
- AmplificationFirstMoment.lean 5 declarations
- AmplificationHighCoins.lean 4 declarations
- AmplificationSecondMoment.lean 1 declarations
- AmplificationTensorProfile.lean 10 declarations
- ArithmeticCandidateKernel.lean 5 declarations
- ArithmeticFirstMoment.lean 1 declarations
- ArithmeticGraphKernel.lean 11 declarations
- ArithmeticKernelMass.lean 2 declarations
- ArithmeticKernelPeriod.lean 6 declarations
- ArithmeticMomentComparison.lean 5 declarations
- ArithmeticMomentDecay.lean 2 declarations
- ArithmeticSecondMoment.lean 2 declarations
- ArithmeticSplitWeights.lean 5 declarations
- BernoulliComparison.lean 15 declarations
- CandidateFairSplit.lean 4 declarations
- CandidateKernelMass.lean 6 declarations
- CandidateRetentionKernel.lean 4 declarations
- CandidateRootKernel.lean 13 declarations
- CandidateSiteKernel.lean 9 declarations
- CandidateSiteMean.lean 4 declarations
- CandidateSquareMoment.lean 3 declarations
- CandidateThirdSiteProbability.lean 4 declarations
- CenteredKernelRows.lean 9 declarations
- ChannelGrid.lean 14 declarations
- ChannelNorm.lean 1 declarations
- CoarseChannel.lean 4 declarations
- CoarseKernelComparison.lean 5 declarations
- CompactTensorApproximation.lean 4 declarations
- ConditionalCoinAverage.lean 4 declarations
- ConditionalCoinReindex.lean 2 declarations
- ConditionalCoinSupport.lean 1 declarations
- ConditionalCoinSwap.lean 1 declarations
- ConditionalFairSplit.lean 5 declarations
- ConsecutiveSiteMean.lean 1 declarations
- CorrectionMoments.lean 6 declarations
- CutNormParameter.lean 4 declarations
- CutNormTriangle.lean 4 declarations
- CyclicKernelPartialSums.lean 2 declarations
- CyclicKernelSum.lean 2 declarations
- EmpiricalResidueProfile.lean 5 declarations
- EndpointFourierMoments.lean 1 declarations
- EndpointHistogramIdentity.lean 4 declarations
- EndpointResiduePartition.lean 2 declarations
- EndpointSplitAverage.lean 2 declarations
- FairSplitChannel.lean 27 declarations
- FairSplitPairRegularity.lean 5 declarations
- FineGridKernel.lean 2 declarations
- FiniteArithmeticKernel.lean 3 declarations
- FiniteChannelSchur.lean 3 declarations
- FiniteChannels.lean 10 declarations
- FiniteFourierKernel.lean 2 declarations
- FiniteGraphKernel.lean 7 declarations
- FiniteHistogramFourier.lean 1 declarations
- FiniteKernelBilinear.lean 5 declarations
- FiniteKernelOrthogonality.lean 2 declarations
- FiniteMcDiarmidDischarge.lean 3 declarations
- FirstOrientedMoment.lean 1 declarations
- FixedResidueReduction.lean 6 declarations
- FlatExclusiveKernel.lean 8 declarations
- FourierSecondMoment.lean 1 import, no declarations
- FrozenHistogramError.lean 1 declarations
- FrozenSiteLaw.lean 6 declarations
- GeometricCoarseKernel.lean 5 declarations
- GeometricHistogramErrors.lean 2 declarations
- GeometricKernelIdentity.lean 3 declarations
- GeometricSquareKernel.lean 9 declarations
- GraphResidueFactors.lean 4 declarations
- GraphResidueMajorant.lean 3 declarations
- GraphResidueMean.lean 3 declarations
- GraphResidueNormalization.lean 4 declarations
- GroupedKernelFeatures.lean 8 declarations
- GrowingMomentParameters.lean 3 declarations
- HighCoinExponent.lean 2 declarations
- HistogramAmplitudeBound.lean 4 declarations
- HistogramConjugation.lean 4 declarations
- HistogramFourierBound.lean 1 declarations
- HistogramFourierRegularity.lean 8 declarations
- HistogramIntegralIdentity.lean 2 declarations
- HistogramLossBound.lean 1 declarations
- HistogramOppositeErrors.lean 3 declarations
- HistogramProductError.lean 6 declarations
- HistogramProductIntegral.lean 1 declarations
- HistogramResidueProjection.lean 3 declarations
- HistogramScaleDecay.lean 2 declarations
- IndependentKernelSplit.lean 25 declarations
- IndependentRootCutNorm.lean 4 declarations
- IntegratedResidueError.lean 2 declarations
- KernelDenominatorSum.lean 3 declarations
- KernelDifferenceMoments.lean 3 declarations
- LatentMassMoments.lean 2 declarations
- LiftedResidueSum.lean 2 declarations
- LogSampledKernel.lean 3 declarations
- LowExclusiveKernel.lean 16 declarations
- MajorArcHistogramBound.lean 2 declarations
- ManuscriptHistogramFourier.lean 3 declarations
- MaskedResidueModel.lean 10 declarations
- MaskedSiteMoments.lean 4 declarations
- NoChangeCoinOperator.lean 6 declarations
- NoChangeMoment.lean 1 declarations
- NoChangeSplitBound.lean 4 declarations
- NormalizedGraphKernel.lean 2 declarations
- OppositeResidueProduct.lean 2 declarations
- OrientedMoments.lean 1 declarations
- OrientedSplitBound.lean 4 declarations
- OrientedSplitExpansion.lean 2 declarations
- PairHitSites.lean 5 declarations
- PartialWeightedChannel.lean 3 declarations
- PolynomialKernelBounds.lean 2 declarations
- ProjectedHistogram.lean 6 declarations
- ProjectedHistogramError.lean 4 declarations
- ProjectedHistogramIntegral.lean 1 declarations
- ProjectedResidueKernel.lean 3 declarations
- PublishedCoarseChannel.lean 2 declarations
- PublishedResidueChannel.lean 2 declarations
- QuotientSiteUnion.lean 3 declarations
- RamanujanResidueFactor.lean 7 declarations
- RampedKernelVariation.lean 2 declarations
- RationalGeometricKernel.lean 4 declarations
- RationalKernelProgressions.lean 1 declarations
- RegularOrientedSplit.lean 2 declarations
- RemainderKernel.lean 4 declarations
- RemainderKernelEstimate.lean 2 declarations
- RemainingSplitRegularity.lean 1 declarations
- ResidueAttenuation.lean 1 declarations
- ResidueAverageMass.lean 5 declarations
- ResidueCentering.lean 17 declarations
- ResidueChannelDecay.lean 5 declarations
- ResidueChannelRate.lean 3 declarations
- ResidueFourierParseval.lean 5 declarations
- ResidueFourierProjection.lean 5 declarations
- ResidueHilbert.lean 7 declarations
- ResidueProductError.lean 2 declarations
- ResidueProductMean.lean 2 declarations
- ResidueProfileLimits.lean 6 declarations
- ResidueProfiles.lean 7 declarations
- ResidueQuotientMean.lean 2 declarations
- ResidueSummatory.lean 4 declarations
- RootSiteLaw.lean 5 declarations
- SampledHistogram.lean 7 declarations
- SampledHistogramError.lean 3 declarations
- SampledKernelInversion.lean 3 declarations
- SampledLogKernelBound.lean 3 declarations
- SampledMajorKernel.lean 5 declarations
- SampledSiteResponse.lean 6 declarations
- SignedChannelMass.lean 8 declarations
- SignedHistogramError.lean 2 declarations
- SignedSplitProduct.lean 6 declarations
- SingularSeriesMoments.lean 3 declarations
- SiteConditionedError.lean 3 declarations
- SiteConditionedRootProduct.lean 2 declarations
- SiteDegreeTail.lean 3 declarations
- SiteGoodEvent.lean 6 declarations
- SitePairFirstLaw.lean 1 declarations
- SitePairTestSum.lean 2 declarations
- SitePartition.lean 4 declarations
- SitePartitionProbability.lean 1 declarations
- SiteResponseConcentration.lean 1 declarations
- SiteTestRestriction.lean 5 declarations
- SplitChangeEvents.lean 10 declarations
- SplitOrientationCover.lean 3 declarations
- SplitProbabilityBounds.lean 6 declarations
- SplitProjectionSupport.lean 4 declarations
- SplitReindex.lean 2 declarations
- SplitSupport.lean 3 declarations
- SubsetKernelProductLaw.lean 1 declarations
- SymmetricSplitLaw.lean 5 declarations
- TensorBoxRegularity.lean 6 declarations
- TensorCutoff.lean 8 declarations
- TwoSiteCoinLaw.lean 2 declarations
- TwoSiteConditionalLaw.lean 1 declarations
- TwoSiteSplitModel.lean 13 declarations
- TwoSiteSplitProduct.lean 2 declarations
- TwoSiteSplitSums.lean 3 declarations
- TwoSplitKernelComparison.lean 5 declarations
- TwoSplitLaw.lean 27 declarations
- UniformCoarseChannel.lean 2 declarations
- UniformResidueChannel.lean 3 declarations
- UniformResidueFibers.lean 7 declarations
- UniformTensorApproximation.lean 7 declarations
- UnitResidueSum.lean 2 declarations
- WeightedCandidateKernel.lean 1 declarations
- WeightedFirstMoment.lean 4 declarations
- WeightedKernelCutoff.lean 7 declarations
- WeightedPolynomialTensor.lean 2 declarations
- WeightedRationalKernel.lean 2 declarations