OAI/Analysis/IrrationalRotation/Model/
587 declarations, 0 contain sorry, 0 declared as axioms; 114 files
Files
- AffiliatedTransport.lean 3 declarations
- Analytic.lean 7 declarations
- BackgroundData.lean 4 declarations
- BiasedTailDensity.lean 1 declarations
- BlockProductCoupling.lean 3 declarations
- BlockedProductCoupling.lean 14 declarations
- BlockedSourceEvent.lean 10 declarations
- CharacterLaw.lean 6 declarations
- CharacterSampling.lean 4 declarations
- CircleConditionalLabels.lean 1 declarations
- CircleCoupling.lean 10 declarations
- CircleDigitCoupling.lean 15 declarations
- CircleDigitMarginals.lean 7 declarations
- CircleOrderedCoupling.lean 3 declarations
- CircleParameters.lean 24 declarations
- CircleRationalGraphs.lean 4 declarations
- CircleSamplingGraph.lean 4 declarations
- CircleSamplingStage.lean 2 declarations
- CircleSmoothing.lean 3 declarations
- CircleTailAttenuation.lean 3 declarations
- CircleTruncation.lean 5 declarations
- CircleTruncationEvent.lean 1 declarations
- CircleWeights.lean 7 declarations
- ColumnOperator.lean 2 declarations
- Commutant.lean 7 declarations
- CompactTransfer.lean 4 declarations
- ConcreteSpectral.lean 8 declarations
- ConditionalConvolution.lean 7 declarations
- Conjugation.lean 1 declarations
- ConjugationDefect.lean 5 declarations
- ContinuityCoboundary.lean 5 declarations
- ContinuousConstruction.lean 4 declarations
- ContinuousCounterexample.lean 1 declarations
- ContinuousExtendedCost.lean 1 declarations
- CouplingMarginalBounds.lean 5 declarations
- CouplingMixture.lean 4 declarations
- Diagonal.lean 4 declarations
- DiagonalGauge.lean 6 declarations
- ExponentialWeight.lean 1 declarations
- Fejer.lean 5 declarations
- FejerApproximation.lean 2 declarations
- FieldDiagonal.lean 7 declarations
- FieldOperator.lean 6 declarations
- FieldUnboundedMultiplier.lean 3 declarations
- FieldWeightedShift.lean 2 declarations
- FiniteConvolution.lean 4 declarations
- FiniteKernelMixture.lean 3 declarations
- GeneratedVonNeumann.lean 1 declarations
- Hyperfinite.lean 1 declarations
- IndependentKernelProduct.lean 2 declarations
- JointEigenspace.lean 3 declarations
- LaurentConvolution.lean 2 declarations
- MixedRadix.lean 11 declarations
- MixedRadixCircle.lean 2 declarations
- MixedRadixProbability.lean 1 declarations
- NormalAffiliation.lean 3 declarations
- OneCoordinateConditional.lean 2 declarations
- OneCoordinateCoupling.lean 12 declarations
- OperatorProperties.lean 10 declarations
- OrbitMeasurable.lean 1 declarations
- ParameterCircleOperator.lean 3 declarations
- ParameterCircleWeights.lean 5 declarations
- ParameterSmoothing.lean 6 declarations
- PhaseBlocks.lean 1 declarations
- PhaseFailure.lean 7 declarations
- PositiveDiagonalModel.lean 19 declarations
- PrefixDomination.lean 4 declarations
- PrefixHybrid.lean 3 declarations
- PrefixPatternLaw.lean 5 declarations
- Product.lean 15 declarations
- ProductBase.lean 14 declarations
- ProductCharacters.lean 3 declarations
- ProductCocycle.lean 5 declarations
- ProductCoupling.lean 12 declarations
- ProductCouplingCircle.lean 6 declarations
- ProductFactorStructure.lean 2 declarations
- ProductIdealSampling.lean 6 declarations
- ProductPairIdentity.lean 3 declarations
- ProductPowers.lean 3 declarations
- ProductPrefixDomination.lean 11 declarations
- ProductSampling.lean 12 declarations
- ProductScaleSampling.lean 1 declarations
- ProductScales.lean 9 declarations
- ProductTailDensity.lean 7 declarations
- ProductTailTrimming.lean 6 declarations
- RationalGraphTrimming.lean 4 declarations
- RealTriangularLaw.lean 4 declarations
- Rotation.lean 15 declarations
- RotationLInfinity.lean 7 declarations
- RotationMeasurable.lean 2 declarations
- RotationProducts.lean 1 declarations
- RotationTransfer.lean 1 declarations
- SamplingTests.lean 4 declarations
- SawtoothSmoothing.lean 3 declarations
- ScalarEndpointDensity.lean 5 declarations
- ScalarKernelEstimates.lean 1 declarations
- ScalarMultiplier.lean 1 declarations
- ScalarSampling.lean 6 declarations
- ScalarSamplingEstimates.lean 11 declarations
- ShiftedPullback.lean 1 declarations
- SourceCouplingMarginals.lean 2 declarations
- SourceProductTail.lean 1 declarations
- Spectral.lean 5 declarations
- SpectralCutoff.lean 14 declarations
- StrictPhase.lean 3 declarations
- TailSubspace.lean 1 declarations
- TrialSampling.lean 7 declarations
- TrimmedCircleSamplingGraph.lean 1 declarations
- UnboundedMultiplier.lean 4 declarations
- UniformIntervalPhase.lean 7 declarations
- UniformQuantization.lean 2 declarations
- UnrestrictedDiagonal.lean 1 declarations
- VectorTraceState.lean 5 declarations
- WeightedShift.lean 11 declarations