OAI/Analysis/IrrationalRotation/Sampling/
1207 declarations, 0 contain sorry, 0 declared as axioms; 157 files
Files
- BlockPhaseConstruction.lean 7 declarations
- CharacterLawConvergence.lean 6 declarations
- CharacterPhaseRealization.lean 2 declarations
- CharacterSamplingBlocks.lean 2 declarations
- CharacterSamplingLimit.lean 2 declarations
- CharacterSamplingLp.lean 4 declarations
- CharacterSamplingLpRealization.lean 1 declarations
- CharacterSamplingRealization.lean 1 declarations
- CharacterSamplingStage.lean 1 declarations
- CharacterSamplingTests.lean 18 declarations
- CharacterSamplingTrial.lean 5 declarations
- CharacterWeakConvergence.lean 6 declarations
- CircleCharacterDynamics.lean 7 declarations
- CircleDigitCrossings.lean 4 declarations
- CircleDigitDensity.lean 7 declarations
- CircleDigitDisintegration.lean 9 declarations
- CircleDigitEndpointLoss.lean 5 declarations
- CircleDigitEnergy.lean 6 declarations
- CircleDigitGeometry.lean 7 declarations
- CircleDigitMarginalLaws.lean 3 declarations
- CircleDigitSecondMoment.lean 2 declarations
- CirclePhaseSummability.lean 9 declarations
- CirclePhaseTails.lean 5 declarations
- CircleRationalSamplingIndex.lean 4 declarations
- CircleSamplingGraph.lean 19 declarations
- CircleSamplingGraphLimits.lean 12 declarations
- CircleSamplingKernelBridge.lean 8 declarations
- CircleSamplingLp.lean 5 declarations
- CircleSamplingStageSupply.lean 1 declarations
- CircleSamplingStageTransport.lean 4 declarations
- DigitAveraging.lean 9 declarations
- ErgodicCharacterCriterion.lean 4 declarations
- FinitePrefixLaw.lean 1 declarations
- FourierSampling.lean 12 declarations
- IntegerPhaseWindow.lean 5 declarations
- LargePhaseAssembly.lean 10 declarations
- MixedRadix.lean 52 declarations
- MixedRadixCircle.lean 14 declarations
- MixedRadixConditioning.lean 4 declarations
- MixedRadixHaarLaw.lean 9 declarations
- MixedRadixLaw.lean 8 declarations
- MixedRadixNonterminal.lean 6 declarations
- MixedRadixTransport.lean 7 declarations
- NonresonantPhaseTrials.lean 4 declarations
- OrthogonalPrefixLimit.lean 2 declarations
- PhaseBlockWeight.lean 2 declarations
- PhaseFailureSummability.lean 7 declarations
- PhaseFailureSummability2.lean 5 declarations
- PhaseRanges.lean 2 declarations
- PrefixCocycleCap.lean 6 declarations
- PrefixCompactTransfer.lean 4 declarations
- PrefixDomination.lean 9 declarations
- PrefixPatternDomination.lean 18 declarations
- PrefixReferenceCompletion.lean 14 declarations
- PrefixReferenceIdentification.lean 7 declarations
- PrescribedPhaseRealization.lean 5 declarations
- PrescribedSamplingStage.lean 2 declarations
- ProductCharacters.lean 18 declarations
- ProductIdealSamplingKernel.lean 6 declarations
- ProductIdealSamplingLimit.lean 12 declarations
- ProductIdealSamplingOrder.lean 7 declarations
- ProductIdealSamplingProduct.lean 10 declarations
- ProductIdealSamplingRectangles.lean 4 declarations
- ProductIdealSamplingScales.lean 2 declarations
- ProductInfiniteSamplingMoments.lean 9 declarations
- ProductPhaseRange.lean 3 declarations
- ProductPrefixApproximation.lean 19 declarations
- ProductPrefixCircle.lean 7 declarations
- ProductPrefixConditioning.lean 2 declarations
- ProductPrefixDomination.lean 10 declarations
- ProductPrefixWeakConvergence.lean 1 declarations
- ProductSampling.lean 17 declarations
- ProductSamplingAbsoluteContinuity.lean 1 declarations
- ProductSamplingAsymptotics.lean 11 declarations
- ProductSamplingCanonicalBudget.lean 3 declarations
- ProductSamplingCoordinateScales.lean 4 declarations
- ProductSamplingCylinderWeights.lean 11 declarations
- ProductSamplingEstimates.lean 6 declarations
- ProductSamplingEventualMarginals.lean 3 declarations
- ProductSamplingExpectedTransport.lean 9 declarations
- ProductSamplingIdealBounds.lean 21 declarations
- ProductSamplingJointMeasurable.lean 8 declarations
- ProductSamplingMoments.lean 9 declarations
- ProductSamplingNumericalBudget.lean 5 declarations
- ProductSamplingNumericalMajorant.lean 8 declarations
- ProductSamplingPhaseMoments.lean 22 declarations
- ProductSamplingPhaseScale.lean 2 declarations
- ProductSamplingRealMoments.lean 3 declarations
- ProductSamplingRestriction.lean 6 declarations
- ProductSamplingScaleTrimming.lean 4 declarations
- ProductSamplingSourceAlmostSure.lean 2 declarations
- ProductSamplingSourceWeak.lean 4 declarations
- ProductSamplingTailReindex.lean 3 declarations
- ProductSamplingTestAlmostSure.lean 4 declarations
- ProductSamplingTestCongruence.lean 8 declarations
- ProductSamplingTestIntegrability.lean 11 declarations
- ProductSamplingTrimming.lean 5 declarations
- ProductSamplingUniformL2.lean 6 declarations
- ProductSamplingUnitTests.lean 5 declarations
- ProductSamplingWeakConvergence.lean 21 declarations
- ProductSamplingWeightAssembly.lean 6 declarations
- ProductSamplingWeightMeasurability.lean 6 declarations
- ProductSamplingWeightScalarBridge.lean 3 declarations
- ProductSamplingWeightTests.lean 16 declarations
- ProductSamplingWeights.lean 19 declarations
- ProductScaleSampling.lean 3 declarations
- ProductSourceSamplingAssembly.lean 1 declarations
- ProductSourceSamplingEnergy.lean 3 declarations
- ProductSourceSamplingFinal.lean 1 declarations
- ProductSourceSamplingL2.lean 4 declarations
- ProductStrictPhaseBounds.lean 3 declarations
- RationalGraphSampling.lean 5 declarations
- RealizedSamplingStage.lean 2 declarations
- SampleMapConditioning.lean 6 declarations
- SamplingAlmostSure.lean 5 declarations
- SamplingAsymptotics.lean 19 declarations
- SamplingCylinderError.lean 6 declarations
- SamplingCylinderWeak.lean 22 declarations
- SamplingErrorSummability.lean 3 declarations
- SamplingHorizon.lean 17 declarations
- SamplingMeanSquare.lean 7 declarations
- SamplingMomentBounds.lean 10 declarations
- SamplingOrbitExpectedWeak.lean 2 declarations
- SamplingOrbitWeak.lean 6 declarations
- SamplingTestContinuity.lean 12 declarations
- SamplingTestLimit.lean 4 declarations
- SamplingTestTrialBridge.lean 8 declarations
- ScalarSampling.lean 27 declarations
- ScalarSamplingContinuity.lean 11 declarations
- ScalarSamplingEndpointVariation.lean 21 declarations
- ScalarSamplingEstimates.lean 6 declarations
- ScalarSamplingFull.lean 4 declarations
- ScalarSamplingJensen.lean 6 declarations
- ScalarSamplingMarginalTransfer.lean 5 declarations
- ScalarSamplingMomentConsequences.lean 11 declarations
- ScalarSamplingNumerics.lean 3 declarations
- ScalarSamplingPairMoments.lean 17 declarations
- ScalarSamplingSeparated.lean 3 declarations
- ScalarSamplingShear.lean 9 declarations
- ScalarSamplingTestVariation.lean 13 declarations
- ScalarSamplingVariation.lean 17 declarations
- SeparatedCharacterFrequencies.lean 8 declarations
- StageSampling.lean 1 declarations
- StrictCharacterSpread.lean 2 declarations
- StrictPhaseStability.lean 7 declarations
- StrictPhaseTrials.lean 9 declarations
- SyndeticSampling.lean 7 declarations
- TestedSamplingMoments.lean 12 declarations
- TrialSamplingActualMoments.lean 7 declarations
- TrialSamplingIdeal.lean 3 declarations
- TrialSamplingIdealMoments.lean 5 declarations
- TrialSamplingMoments.lean 10 declarations
- TrialSamplingPowers.lean 2 declarations
- TrialSamplingScalar.lean 4 declarations
- TrialSamplingSelection.lean 13 declarations
- TrimmedCircleSamplingGraph.lean 9 declarations
- UniformIntervalPhase.lean 24 declarations