`OAI/NumberTheory/DukePrimeDegree/Dynamics/`

1102 declarations, 0 contain sorry, 0 declared as axioms; 240 files

Files

ActiveBlockProjection.lean 7 declarations
AlmostInvariantComponents.lean 1 declarations
BlockDiagonalAlgebra.lean 12 declarations
BlockEliminationSchedule.lean 13 declarations
BlockGroupNormalizer.lean 5 declarations
BlockIncidentComponents.lean 2 declarations
BlockIncidentMautner.lean 4 declarations
BlockMatrixProjection.lean 7 declarations
BlockNormalizer.lean 9 declarations
BlockNormalizerFiniteIndex.lean 13 declarations
BlockOrbit.lean 5 declarations
BlockOrbitMass.lean 4 declarations
BlockRootGroup.lean 11 declarations
BlockTransverseDiagonal.lean 11 declarations
BlockTransverseElimination.lean 7 declarations
BoundedGenericSet.lean 5 declarations
BoundedReturnCompactSupport.lean 2 declarations
CanonicalSubgroupComponents.lean 1 declarations
CentralOrbitCover.lean 2 declarations
CentralizerContraction.lean 4 declarations
CentralizerFlow.lean 9 declarations
CentralizerWeights.lean 6 declarations
CompactFamilyGeneric.lean 6 declarations
CompactFlowReturns.lean 4 declarations
CompactShearingSequence.lean 1 declarations
CompactStabilizerSeparation.lean 4 declarations
ConjugationOrbit.lean 20 declarations
ConnectedBlockContainment.lean 4 declarations
CorrectedGenericPairs.lean 3 declarations
CountableOrbitSection.lean 1 declarations
DenseActionAverages.lean 12 declarations
DenseInvariantFunctions.lean 1 declarations
DiagonalFlowMaximal.lean 2 declarations
DiagonalProjectiveRecurrence.lean 4 declarations
DiagonalRecurrence.lean 6 declarations
DominatedAverages.lean 2 declarations
EqualLeafReturnWindows.lean 1 declarations
EqualLeafReturns.lean 2 declarations
ErgodicAverageMean.lean 9 declarations
ErgodicL2Averages.lean 1 declarations
ErgodicReturnLevels.lean 2 declarations
EuclideanVelocityProjection.lean 12 declarations
ExactInvariantFunctions.lean 9 declarations
ExactInvariantSets.lean 6 declarations
ExceptionalReturns.lean 4 declarations
ExponentialReturnRefinement.lean 2 declarations
ExtremalRootFlow.lean 5 declarations
FiniteDiagonalVelocity.lean 5 declarations
FiniteFlowGenericSets.lean 2 declarations
FiniteKoopmanAverages.lean 7 declarations
FiniteOrbitDensity.lean 3 declarations
FixedTerminalShearing.lean 3 declarations
FlowMaximal.lean 3 declarations
FlowOccupation.lean 10 declarations
FlowSmoothedL2.lean 4 declarations
FlowWindowAverages.lean 6 declarations
ForwardOrbitSection.lean 1 declarations
FrameSubspaceRecurrence.lean 2 declarations
GenericBlockOrbit.lean 4 declarations
GenericLatticeStabilizer.lean 1 declarations
GenericMatrixPairs.lean 3 declarations
GenericMeanOscillation.lean 4 declarations
GenericRootCommutant.lean 10 declarations
HaarFromHomogeneousComponent.lean 2 declarations
HomogeneousComponents.lean 2 declarations
HopfContracting.lean 2 declarations
HopfMaximal.lean 7 declarations
HopfMeanBound.lean 2 declarations
HopfPairs.lean 5 declarations
HopfTranslationOrbits.lean 2 declarations
HorosphereIsolatingFlow.lean 9 declarations
IntegrableCoboundary.lean 6 declarations
IntrinsicShearingCollision.lean 1 declarations
InvariantMeanGenericSet.lean 6 declarations
InvariantMeanLimit.lean 2 declarations
InvariantMeasureGroup.lean 4 declarations
InvariantRootExistence.lean 1 declarations
InvariantVersion.lean 1 declarations
KernelStabilizerMeasurable.lean 4 declarations
KernelVelocityDistance.lean 1 declarations
KernelVelocityFrames.lean 10 declarations
KernelVelocityRecurrence.lean 5 declarations
L2ToL1Averages.lean 4 declarations
LatticeCentralizer.lean 8 declarations
LatticeInvariantVersions.lean 1 declarations
LeafFlowCovariance.lean 7 declarations
LeafReturnCovariance.lean 2 declarations
LocalOrbitIsolation.lean 4 declarations
LusinFlowReturns.lean 1 declarations
MatrixExponentialVelocity.lean 4 declarations
MatrixVelocitySpace.lean 11 declarations
MautnerBlock.lean 3 declarations
MautnerBlockL2.lean 1 declarations
MautnerLatticeL2.lean 4 declarations
MautnerMetric.lean 3 declarations
MautnerRootPair.lean 5 declarations
MaximalOccupation.lean 6 declarations
MeasureStabilizerCovariance.lean 4 declarations
NeutralBlockLocalInvariance.lean 2 declarations
NeutralBlockVelocity.lean 4 declarations
NeutralLeafFlow.lean 2 declarations
NoCentralizerOrbit.lean 1 declarations
NoFixedVectorOrbit.lean 4 declarations
NoInvariantRootGraph.lean 2 declarations
NoncentralReturns.lean 3 declarations
NormalizedDenseSubgroup.lean 3 declarations
NormalizerErgodicComponents.lean 1 declarations
NormalizerInvariantSigma.lean 4 declarations
NormalizerOrbitReduction.lean 4 declarations
OneSidedCoboundary.lean 4 declarations
OpenSubgroupOrbit.lean 6 declarations
OrbitAverageFunctions.lean 5 declarations
OrbitBasepoint.lean 4 declarations
OrbitCoboundary.lean 5 declarations
OrbitConcentration.lean 1 declarations
OrbitGenericity.lean 7 declarations
OrbitMeasureTransfer.lean 7 declarations
OrbitRationality.lean 10 declarations
OrbitRecurrence.lean 2 declarations
OrbitSupport.lean 2 declarations
OrbitWindowMeasures.lean 6 declarations
PairedBlockOrbit.lean 3 declarations
PairedOrbitSupport.lean 4 declarations
PairedRootCentralizer.lean 6 declarations
PositiveOrbitRestriction.lean 1 declarations
PrimeBlockEndpoint.lean 3 declarations
PrimeBlockRationality.lean 28 declarations
PrimeSingleBlockHaar.lean 4 declarations
PublishedEKL.lean 8 declarations
QuantitativeCutAverage.lean 1 declarations
QuotientReturn.lean 1 declarations
RationalCentralizer.lean 9 declarations
RealFlowWindows.lean 5 declarations
ReturnLiftAlignment.lean 2 declarations
ReturnTowerCoverage.lean 1 declarations
ReturnTowerLevels.lean 6 declarations
ReturnTowerMass.lean 2 declarations
ReverseRootFlow.lean 4 declarations
RootBlocks.lean 9 declarations
RootCentralizer.lean 6 declarations
RootFlowGeneric.lean 2 declarations
RootHopf.lean 1 declarations
RootInvariantLeaves.lean 5 declarations
RootInvariantNonatomic.lean 2 declarations
RootLeafHopf.lean 5 declarations
RootOrbitConcentration.lean 1 declarations
RootOrbitRationality.lean 4 declarations
RootOrbitRebase.lean 4 declarations
RootOrbitSeparation.lean 1 declarations
RootPairErgodicity.lean 6 declarations
RootShearing.lean 6 declarations
RootVelocityRecovery.lean 6 declarations
ScalarOrbitCommutant.lean 4 declarations
SeparatedOrbitCover.lean 8 declarations
ShearingAnnulus.lean 4 declarations
ShearingBoundedLimit.lean 1 declarations
ShearingCandidateWindows.lean 1 declarations
ShearingCentralizer.lean 5 declarations
ShearingCoefficientBounds.lean 8 declarations
ShearingCollision.lean 5 declarations
ShearingCompactness.lean 4 declarations
ShearingDiagonal.lean 14 declarations
ShearingFourWindows.lean 3 declarations
ShearingHorosphere.lean 5 declarations
ShearingKappa.lean 12 declarations
ShearingLimits.lean 4 declarations
ShearingLogTime.lean 6 declarations
ShearingMeasureLimits.lean 4 declarations
ShearingNormalizedProfile.lean 5 declarations
ShearingProfile.lean 2 declarations
ShearingRegimes.lean 2 declarations
ShearingReturnGeometry.lean 2 declarations
ShearingScale.lean 7 declarations
ShearingSelectedConvergence.lean 1 declarations
ShearingSelection.lean 2 declarations
ShearingSelectionData.lean 2 declarations
ShearingSignedCentralizer.lean 4 declarations
ShearingSignedCollision.lean 2 declarations
ShearingSignedLimit.lean 1 declarations
ShearingTimeCovariance.lean 3 declarations
ShearingTimeSelection.lean 1 declarations
ShearingTwoAnnuli.lean 2 declarations
ShearingTwoScales.lean 1 declarations
ShearingWindow.lean 4 declarations
ShearingWindowControl.lean 2 declarations
SingleBlockClosure.lean 4 declarations
SingleBlockComponents.lean 1 declarations
SingleBlockCorrectedPairs.lean 2 declarations
SingleBlockErgodicity.lean 6 declarations
SingleBlockGenericSet.lean 1 declarations
SingleBlockLocalStabilizer.lean 3 declarations
SingleBlockNoncentral.lean 3 declarations
SingleBlockNormalization.lean 15 declarations
SingleBlockOrbitExistence.lean 3 declarations
SingleBlockProjection.lean 3 declarations
SingleBlockShearingContradiction.lean 1 declarations
SingleBlockShearingLimit.lean 2 declarations
SingleBlockShell.lean 9 declarations
SingleBlockTransverse.lean 6 declarations
SingularCentralizer.lean 3 declarations
SmallCentralizer.lean 12 declarations
SmallFineReturnRefinement.lean 2 declarations
SmallOrbitSection.lean 3 declarations
SmallReturnRefinement.lean 3 declarations
SmallReturns.lean 3 declarations
StabilizerClosedGraph.lean 3 declarations
StrongReturnExclusion.lean 2 declarations
StrongReturns.lean 4 declarations
StrongStableConjugates.lean 1 declarations
SubgroupInduction.lean 3 declarations
SynchronizedReturns.lean 1 declarations
TemperedOrbitWindows.lean 5 declarations
TerminalGenericWindows.lean 3 declarations
TransferredVelocity.lean 5 declarations
TranslationInvariantProduct.lean 4 declarations
TranslationInvariantSlices.lean 6 declarations
TransverseReturnCoordinates.lean 2 declarations
TransverseStabilizerLimit.lean 8 declarations
TriangularStabilizer.lean 8 declarations
TwoAnnularEqualReturns.lean 1 declarations
TwoAnnularReturns.lean 1 declarations
TwoBlockGauss.lean 11 declarations
TwoBlockGaussChart.lean 11 declarations
TwoBlockGroups.lean 12 declarations
TwoBlockIndexTransport.lean 7 declarations
TwoBlockInvariantChart.lean 10 declarations
TwoBlockLocalNeutralMeasure.lean 12 declarations
TwoBlockNeutralAction.lean 11 declarations
TwoBlockParabolicChart.lean 12 declarations
UnboundedReturnSection.lean 2 declarations
UniformShearingWindow.lean 3 declarations
UnipotentFreeness.lean 2 declarations
UnitFlowSmoothing.lean 7 declarations
VectorAvoidance.lean 2 declarations
VelocityClosedGraph.lean 4 declarations
VelocityCommutant.lean 3 declarations
VelocityMembershipMeasurable.lean 4 declarations
VelocityRootProjection.lean 5 declarations
VelocityTransportRank.lean 3 declarations
WeylAtomicRoots.lean 2 declarations