OAI/Analysis/IrrationalRotation/Rotation/
1039 declarations, 0 contain sorry, 0 declared as axioms; 147 files
Files
- ActualRotationCentrality.lean 2 declarations
- AnalyticWeightBridge.lean 10 declarations
- BlockedCircleEvent.lean 6 declarations
- CanonicalCircleCoefficients.lean 3 declarations
- CanonicalCircleFiniteLower.lean 5 declarations
- ChoKoLeeCircleReduction.lean 1 declarations
- CircleBackgroundBumps.lean 3 declarations
- CircleBackgroundCost.lean 9 declarations
- CircleCocycle.lean 12 declarations
- CircleCocycleSupport.lean 5 declarations
- CircleCocycleWindow.lean 10 declarations
- CircleCoefficientBounds.lean 11 declarations
- CircleCurrentBlockEvent.lean 5 declarations
- CircleErgodicity.lean 3 declarations
- CircleFiberDecay.lean 5 declarations
- CircleFieldDecay.lean 4 declarations
- CircleFlattenedCosts.lean 2 declarations
- CircleFutureBudget.lean 9 declarations
- CircleFutureEndpointLoss.lean 12 declarations
- CircleKernelConvolution.lean 21 declarations
- CircleMarginalBudget.lean 5 declarations
- CircleMarginalDensity.lean 1 declarations
- CircleMeasurableObstruction.lean 1 declarations
- CircleObstruction.lean 4 declarations
- CircleOrderedHaarRigidity.lean 5 declarations
- CircleOrderedSharpness.lean 10 declarations
- CircleOrderedTransfer.lean 14 declarations
- CircleParameterBlocks.lean 11 declarations
- CircleParameterConsequences.lean 6 declarations
- CircleParameterRecursion.lean 34 declarations
- CircleParametersExistence.lean 1 declarations
- CircleProjectionEndpointLoss.lean 1 declarations
- CircleQuantizedMarginals.lean 11 declarations
- CircleRationalGraphApproximants.lean 12 declarations
- CircleRationalGraphCaps.lean 3 declarations
- CircleRationalGraphFields.lean 2 declarations
- CircleRationalGraphTransfer.lean 4 declarations
- CircleRawTagEvent.lean 5 declarations
- CircleRepresentative.lean 2 declarations
- CircleSmoothing.lean 18 declarations
- CircleTailAttenuation.lean 4 declarations
- CircleTailExceptionalFamilies.lean 1 declarations
- CircleTruncationBound.lean 2 declarations
- CircleTruncationEvent.lean 2 declarations
- CircleTruncationIntegral.lean 2 declarations
- CircleTruncationMass.lean 6 declarations
- CircleWeightDecay.lean 9 declarations
- CircleWeightSupport.lean 6 declarations
- CocycleSupport.lean 5 declarations
- CocycleWindow.lean 4 imports, no declarations
- CocycleWindowBounds.lean 15 declarations
- ContinuousCircleImage.lean 4 declarations
- ContinuousCircleRepresentation.lean 4 declarations
- ContinuousWeightAssembly.lean 12 declarations
- ContinuousWeightOperatorBridge.lean 6 declarations
- ContinuousWeightParameterBridge.lean 2 declarations
- CountableWeightRange.lean 6 declarations
- DiagonalAdjoint.lean 6 declarations
- DiagonalContinuity.lean 8 declarations
- DiagonalGauge.lean 27 declarations
- DiagonalJointEigenspace.lean 1 declarations
- ExponentialWeight.lean 6 declarations
- ExponentialWeightIntegral.lean 9 declarations
- FieldDiagonal.lean 16 declarations
- FieldDiagonalConvergence.lean 3 declarations
- FieldDiagonalPositive.lean 2 declarations
- FieldKoopmanDiagonal.lean 4 declarations
- FieldWeightedShiftHalfline.lean 12 declarations
- FieldWeightedShiftPowers.lean 7 declarations
- FiniteFloorCocycle.lean 3 declarations
- FiniteSupportCocycle.lean 6 declarations
- FiniteSupportWeights.lean 19 declarations
- FloorCocycle.lean 10 declarations
- GaugeFourierDiagonal.lean 18 declarations
- MeasurableRotationDenseRange.lean 6 declarations
- ParameterCircleCocycle.lean 14 declarations
- ParameterCircleReindex.lean 3 declarations
- ParameterPositiveDiagonal.lean 3 declarations
- PositiveDiagonal.lean 4 declarations
- PositiveDiagonalAlgebra.lean 1 declarations
- PositiveDiagonalFields.lean 2 declarations
- PositiveDiagonalRepresentatives.lean 2 declarations
- ProjectionCocycleWindow.lean 9 declarations
- ProjectionDiagonal.lean 7 declarations
- ProjectionDiagonalPropagation.lean 13 declarations
- RealWeightedPositiveDiagonal.lean 7 declarations
- RepresentedPositiveDiagonal.lean 4 declarations
- Rotation.lean 30 declarations
- RotationAlgebra.lean 6 declarations
- RotationCenter.lean 3 declarations
- RotationCyclicity.lean 7 declarations
- RotationDecay.lean 9 declarations
- RotationDenseRange.lean 6 declarations
- RotationDiagonalState.lean 2 declarations
- RotationDiffuse.lean 7 declarations
- RotationFactorStructure.lean 1 declarations
- RotationFieldExistence.lean 1 declarations
- RotationFieldRepresentation.lean 1 declarations
- RotationFields.lean 5 declarations
- RotationFiniteReturnTowers.lean 3 declarations
- RotationFourierDensity.lean 4 declarations
- RotationHalfline.lean 5 declarations
- RotationHilbert.lean 5 declarations
- RotationHyperfinite.lean 1 declarations
- RotationHyperfiniteCriterion.lean 3 declarations
- RotationInjective.lean 5 declarations
- RotationLInfinity.lean 19 declarations
- RotationLInfinityConvergence.lean 1 declarations
- RotationLInfinityIsometry.lean 5 declarations
- RotationMeasurable.lean 13 declarations
- RotationMeasurableLaws.lean 7 declarations
- RotationMoments.lean 18 declarations
- RotationNonzero.lean 7 declarations
- RotationPositiveDiagonal.lean 2 declarations
- RotationPowerNorm.lean 8 declarations
- RotationProjectionTransport.lean 4 declarations
- RotationRecursiveTowerAssembly.lean 4 declarations
- RotationReturnTowers.lean 15 declarations
- RotationScalarity.lean 4 declarations
- RotationSeparating.lean 3 declarations
- RotationSetProjectionSmallSupport.lean 4 declarations
- RotationSetProjections.lean 22 declarations
- RotationShrinkingBases.lean 6 declarations
- RotationSmallSupport.lean 8 declarations
- RotationSmallSupportBounds.lean 3 declarations
- RotationTowerAlgebras.lean 14 declarations
- RotationTowerApproximation.lean 2 declarations
- RotationTowerCyclicApproximation.lean 7 declarations
- RotationTowerHyperfiniteAssembly.lean 2 declarations
- RotationTrace.lean 5 declarations
- RotationTraceNormality.lean 3 declarations
- RotationTransfer.lean 8 declarations
- RotationTransferIntertwining.lean 3 declarations
- RotationTransferInverse.lean 9 declarations
- RotationTransferTrace.lean 6 declarations
- TowerDiagonalApproximation.lean 14 declarations
- UniformRotationAverage.lean 22 declarations
- UnrestrictedDiagonal.lean 4 declarations
- WeightedGraphMarginals.lean 6 declarations
- WeightedOrbitInvariance.lean 14 declarations
- WeightedShiftAlgebra.lean 15 declarations
- WeightedShiftCentrality.lean 4 declarations
- WeightedShiftDiagonal.lean 9 declarations
- WeightedShiftHalfline.lean 9 declarations
- WeightedShiftMeasurability.lean 4 declarations
- WeightedShiftPowers.lean 13 declarations
- WeightedShiftTransport.lean 3 declarations