OAI/Analysis/IrrationalRotation/Product/
514 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- CoordinateSwap.lean 7 declarations
- FiniteProductAbsoluteContinuity.lean 4 declarations
- FloorProducts.lean 8 declarations
- IndependentAngles.lean 14 declarations
- IndependentCoordinateConditioning.lean 11 declarations
- IndependentKernelProduct.lean 8 declarations
- IndependentMissBounds.lean 4 declarations
- IndependentRotation.lean 8 declarations
- OneCoordinateCrossing.lean 17 declarations
- OneCoordinateDensity.lean 27 declarations
- ProductAlgebraDimension.lean 5 declarations
- ProductBaseDynamics.lean 6 declarations
- ProductBlockCost.lean 4 declarations
- ProductBlockTailBounds.lean 13 declarations
- ProductCircleConditioning.lean 10 declarations
- ProductCircleThresholds.lean 5 declarations
- ProductCocycle.lean 18 declarations
- ProductCocycleInterchange.lean 5 declarations
- ProductCocycleWindow.lean 3 declarations
- ProductConvolutionIdentity.lean 5 declarations
- ProductCoordinateSplit.lean 1 declarations
- ProductCovariance.lean 9 declarations
- ProductDenseRange.lean 7 declarations
- ProductDiffuse.lean 7 declarations
- ProductErgodicity.lean 5 declarations
- ProductFactorComplete.lean 1 declarations
- ProductFactorCovariance.lean 5 declarations
- ProductFactorSource.lean 2 declarations
- ProductFieldConverse.lean 2 declarations
- ProductFieldDiagonals.lean 12 declarations
- ProductFieldRepresentation.lean 3 declarations
- ProductFields.lean 7 declarations
- ProductFloorIntegral.lean 5 declarations
- ProductGaugeFourier.lean 9 declarations
- ProductHilbert.lean 5 declarations
- ProductIdealCylinderLimit.lean 10 declarations
- ProductInvariantProjectionObstruction.lean 1 declarations
- ProductLogIntegral.lean 5 declarations
- ProductMultiplierFunctionalCalculus.lean 14 declarations
- ProductNorm.lean 14 declarations
- ProductObstructionConstant.lean 3 declarations
- ProductOrbitFiberNull.lean 6 declarations
- ProductOrbitL2Marginals.lean 1 declarations
- ProductOrbitMarginals.lean 12 declarations
- ProductOrbitPair.lean 8 declarations
- ProductOrbitTests.lean 8 declarations
- ProductPairRatios.lean 4 declarations
- ProductPairSanity.lean 7 declarations
- ProductPairTransfer.lean 2 declarations
- ProductPositiveDiagonal.lean 2 declarations
- ProductPowerIdentity.lean 6 declarations
- ProductPowerOrbit.lean 4 declarations
- ProductProjectionFields.lean 3 declarations
- ProductRealizationAssembly.lean 1 declarations
- ProductScalarity.lean 2 declarations
- ProductScaleAnalyticRealization.lean 1 declarations
- ProductScaleCocycleWindow.lean 5 declarations
- ProductScaleConsequences.lean 20 declarations
- ProductScaleConstruction.lean 13 declarations
- ProductScaleRealization.lean 1 declarations
- ProductScaleTagAttenuation.lean 1 declarations
- ProductScaleTail.lean 6 declarations
- ProductScaleTailAssignment.lean 2 declarations
- ProductScaleTailAttenuation.lean 2 declarations
- ProductSourceAngleLaw.lean 4 declarations
- ProductSourceCircleAttenuation.lean 1 declarations
- ProductSourceCocycleAttenuation.lean 2 declarations
- ProductSourceTagAttenuation.lean 2 declarations
- ProductSupport.lean 1 declarations
- ProductTailDensity.lean 5 declarations
- ProductTailScaleCover.lean 1 declarations
- ProductTailTrimming.lean 19 declarations
- ProductTestedExpectationSummability.lean 4 declarations
- ProductTestedKernelMoments.lean 8 declarations
- ProductThresholdIndependence.lean 2 declarations
- ProductTraceNormality.lean 3 declarations
- ProductTracialInputs.lean 10 declarations
- ProductTracialVector.lean 4 declarations
- ProductWeightBridge.lean 13 declarations
- ProductWeightNonconstant.lean 6 declarations
- SourceProductTailAttenuation.lean 1 declarations
- SourceProductTailRealization.lean 2 declarations