OAI/NumberTheory/DukePrimeDegree/Geometry/

Files

• AdjacentFirstProduct.lean 3 declarations
• AdjacentFirstRoot.lean 6 declarations
• AffineTimeSelection.lean 5 declarations
• AtomicNeutralPatch.lean 1 declarations
• AtomicRootLimits.lean 1 declarations
• AtomicRootPositivity.lean 2 declarations
• AtomlessDiagonalMeasure.lean 2 declarations
• BilateralNeutralLifts.lean 2 declarations
• BoundedPhysicalRectangles.lean 2 declarations
• CanonicalRootBasic.lean 7 declarations
• CanonicalRootCoefficients.lean 4 declarations
• CommutatorInvariance.lean 2 declarations
• CompactAction.lean 2 declarations
• CompactCorrectionPatches.lean 2 declarations
• CompactLimitData.lean 1 declarations
• CompactNeutralFibers.lean 4 declarations
• CompactPhysicalRectangles.lean 1 declarations
• ComponentRootConstancy.lean 6 declarations
• ComponentRootPattern.lean 5 declarations
• ConjugationRadius.lean 6 declarations
• ConjugationReference.lean 3 declarations
• ConjugationRestrictions.lean 2 declarations
• ConjugationTransport.lean 3 declarations
• ControlledDistanceCuts.lean 1 declarations
• ControlledRadialHeight.lean 1 declarations
• Convergence.lean 1 declarations
• CorrectedPairLimits.lean 2 declarations
• CountableCutNeighborhoods.lean 1 declarations
• CountableRootPrefixAtoms.lean 2 declarations
• CountableWeakKernel.lean 10 declarations
• CountableWeakTests.lean 4 declarations
• CutFamilyCode.lean 4 declarations
• DenseDiagonalGenerators.lean 9 declarations
• DiagonalCommutatorCurve.lean 12 declarations
• DiagonalPeriodicity.lean 1 declarations
• DiagonalRootTubes.lean 10 declarations
• DiagonalTwoTargets.lean 2 declarations
• DiracFiberGraph.lean 4 declarations
• DiscreteMaximal.lean 2 declarations
• DistanceCutBounds.lean 3 declarations
• DyadicBoundaryCuts.lean 3 declarations
• EliminationChain.lean 15 declarations
• EliminationFirstRootSlice.lean 7 declarations
• EliminationMatrixCoordinates.lean 2 declarations
• EliminationRootChart.lean 7 declarations
• EliminationRootOrder.lean 7 declarations
• EliminationWordEntries.lean 3 declarations
• EmbeddingMatrix.lean 7 declarations
• ExponentialCutBoundary.lean 1 declarations
• ExponentialCutFamily.lean 1 declarations
• ExponentialCutSize.lean 1 declarations
• ExponentialLevelBudget.lean 3 declarations
• ExtremalConjugationEntries.lean 1 declarations
• ExtremalRemainingEntries.lean 4 declarations
• ExtremalRootQuotient.lean 4 declarations
• FactorAtSample.lean 1 declarations
• FactorPivotCylinder.lean 2 declarations
• FactorSliceFreeness.lean 1 declarations
• FineTransverseConjugates.lean 2 declarations
• FiniteCoordinateIndependence.lean 2 declarations
• FiniteKernelEquality.lean 1 declarations
• FiniteLinearShear.lean 5 declarations
• FiniteNormalizedRectangle.lean 2 declarations
• FiniteOrderSpectrum.lean 4 declarations
• FiniteProductShear.lean 5 declarations
• FiniteProjectionFrames.lean 23 declarations
• FiniteRealProductKernel.lean 2 declarations
• FiniteTransverseCode.lean 1 declarations
• FirstCoverCode.lean 8 declarations
• FirstCoverLocalPacking.lean 2 declarations
• FrameChangeOfBasis.lean 2 declarations
• FrameWeightRigidity.lean 8 declarations
• FullFrameMinors.lean 1 declarations
• GoodSetFiberCorrection.lean 8 declarations
• HeightBoundaryCount.lean 7 declarations
• HorosphereAtomicSupport.lean 1 declarations
• HorosphereChart.lean 10 declarations
• HorosphereCollision.lean 1 declarations
• HorosphereCoordinates.lean 12 declarations
• HorosphereDiagonal.lean 3 declarations
• HorosphereFreeness.lean 4 declarations
• HorosphereIsolatedLimit.lean 3 declarations
• HorosphereRootExtraction.lean 1 declarations
• HorosphereSeparation.lean 1 declarations
• IncidentRootObstruction.lean 3 declarations
• IndependentCoordinateKernel.lean 7 declarations
• IndependentGraphSlice.lean 2 declarations
• IndependentNestedKernel.lean 2 declarations
• IndexedLinearShear.lean 6 declarations
• IndexedRootShear.lean 1 declarations
• IntegratedCoverCost.lean 2 declarations
• IteratedRootShear.lean 4 declarations
• KernelTransport.lean 5 declarations
• LargePhysicalRectangles.lean 2 declarations
• LatticeGroupDecomposition.lean 9 declarations
• LatticeSpace.lean 20 declarations
• LeafBoundedMaximal.lean 1 declarations
• LeafBoxMaximal.lean 1 declarations
• LeafBoxSeparation.lean 2 declarations
• LeafClosedRadius.lean 1 declarations
• LeafCompactMaximal.lean 1 declarations
• LeafGoodSet.lean 1 declarations
• LeafLusin.lean 7 declarations
• LeafLusinGoodSet.lean 1 declarations
• LeafMaximal.lean 3 declarations
• LeafMaximalDisintegration.lean 2 declarations
• LeafMaximalIntrinsic.lean 5 declarations
• LeafMaximalScaling.lean 4 declarations
• LeafMeasurableBad.lean 7 declarations
• LeafNormalizationInjectivity.lean 3 declarations
• LeafNullClosure.lean 2 declarations
• LeafPairSelection.lean 2 declarations
• LeafRationalRadii.lean 2 declarations
• LeafRegularSet.lean 1 declarations
• LeafScaleComposition.lean 4 declarations
• LeafShortMaximal.lean 1 declarations
• LeafSmallRadius.lean 3 declarations
• LexicographicRootWeights.lean 6 declarations
• LocalInjectivityHeight.lean 5 declarations
• LocalMoment.lean 5 declarations
• LocalProduct.lean 2 declarations
• LocalProjection.lean 2 declarations
• LocalQuotientPacking.lean 4 declarations
• MatrixConjugationDensity.lean 11 declarations
• MatrixCoordinateFrames.lean 10 declarations
• MatrixLogLength.lean 13 declarations
• MatrixPowerApproximation.lean 3 declarations
• MeasureConjugation.lean 3 declarations
• NestedRectangleRestriction.lean 1 declarations
• NeutralAction.lean 5 declarations
• NeutralAtomicPatch.lean 3 declarations
• NeutralCoordinateMeasure.lean 10 declarations
• NeutralDiagonal.lean 6 declarations
• NeutralGraphLifts.lean 2 declarations
• NeutralHaarProduct.lean 1 declarations
• NeutralLeafVersion.lean 2 declarations
• NeutralPatchCover.lean 5 declarations
• NeutralPatchNull.lean 6 declarations
• NeutralPrefixMap.lean 8 declarations
• NeutralSmallRectangles.lean 1 declarations
• NeutralTransverseCoordinates.lean 20 declarations
• NeutralUpperRootChart.lean 5 declarations
• NeutralUpperRootHomeomorph.lean 7 declarations
• NeutralWeightSpace.lean 3 declarations
• NextGroupConjugation.lean 6 declarations
• NextGroupCoordinates.lean 5 declarations
• NextProductChain.lean 3 declarations
• NextProductHolonomy.lean 1 declarations
• NextProductRegularity.lean 1 declarations
• NextProductTranslations.lean 3 declarations
• NormalizedFactorProduct.lean 2 declarations
• NormalizedFrame.lean 7 declarations
• NormalizedIntersections.lean 2 declarations
• NormalizedLattice.lean 11 declarations
• NormalizedPiMeasures.lean 3 declarations
• NormalizedProductRectangle.lean 2 declarations
• NormalizedRestrictionLimit.lean 3 declarations
• NormalizerKernelCovariance.lean 2 declarations
• OpenRegionEmbedding.lean 1 declarations
• OrderedEliminationChain.lean 8 declarations
• OrderedRootElimination.lean 8 declarations
• OwnLeafSeparation.lean 2 declarations
• PairedCoordinateAlgebra.lean 9 declarations
• PhysicalIndependentBoxes.lean 1 declarations
• PhysicalLeafInduction.lean 1 declarations
• PhysicalPointFactor.lean 1 declarations
• PhysicalPrefixBox.lean 3 declarations
• PhysicalPrefixCoordinates.lean 7 declarations
• PhysicalPrefixMeasure.lean 8 declarations
• PhysicalPrefixRealMarginal.lean 1 declarations
• PhysicalPrefixWindows.lean 4 declarations
• PhysicalProductRebase.lean 1 declarations
• PhysicalRectangleFactor.lean 1 declarations
• PhysicalRectangleKernel.lean 3 declarations
• PhysicalRootEmbeddings.lean 5 declarations
• PhysicalRootMarginal.lean 1 declarations
• PhysicalRootRectangles.lean 6 declarations
• PhysicalWindowAtlas.lean 6 declarations
• PhysicalWindowIntrinsic.lean 1 declarations
• PhysicalWindowProduct.lean 1 declarations
• PhysicalWindowRebase.lean 4 declarations
• PluckerCovariance.lean 4 declarations
• PositiveRootCoordinates.lean 6 declarations
• PositiveRootFactorization.lean 6 declarations
• PositiveRootHolonomy.lean 3 declarations
• PositiveRootPattern.lean 8 declarations
• PrefixBoundedRegions.lean 4 declarations
• PrefixExchangeMeasures.lean 6 declarations
• PrefixExchangeRegions.lean 8 declarations
• PrefixFactorIdentification.lean 1 declarations
• PrefixRectangleCandidates.lean 1 declarations
• PrefixRegionAmbientCandidates.lean 1 declarations
• PrefixRegionFibers.lean 4 declarations
• PrefixTimeExchange.lean 5 declarations
• PrefixWindowProportionality.lean 1 declarations
• ProjectionFromDistances.lean 4 declarations
• ProjectiveLeafEquality.lean 5 declarations
• ProportionalWindowMeasures.lean 3 declarations
• QuantitativeDistanceNet.lean 3 declarations
• QuantitativeQuotientCover.lean 1 declarations
• QuotientLiftInvariance.lean 1 declarations
• QuotientLiftMeasure.lean 7 declarations
• QuotientLogDistance.lean 12 declarations
• QuotientLogProper.lean 4 declarations
• QuotientLogTopology.lean 3 declarations
• QuotientMeasurableSection.lean 1 declarations
• QuotientNeighborhoods.lean 5 declarations
• QuotientSeparatingCuts.lean 8 declarations
• RadialHeightContinuity.lean 4 declarations
• RadialLocalInjectivity.lean 1 declarations
• RationalFixedVectors.lean 10 declarations
• RealLeafDensity.lean 1 declarations
• RealWindowRebase.lean 2 declarations
• RectangleReferences.lean 1 declarations
• Reduction.lean 5 declarations
• RegularLusinSets.lean 2 declarations
• RegularRootInvariance.lean 5 declarations
• RegularRootSymmetry.lean 6 declarations
• RemainingAtomicProduct.lean 5 declarations
• RemainingChainExistence.lean 2 declarations
• RemainingEuclideanCoordinates.lean 6 declarations
• RemainingFactorRebase.lean 5 declarations
• RemainingGroupCenter.lean 4 declarations
• RemainingIntrinsicProduct.lean 5 declarations
• RemainingLeafProduct.lean 1 declarations
• RemainingProductBase.lean 1 declarations
• RemainingProductCoordinates.lean 8 declarations
• RemainingProductDiagonal.lean 4 declarations
• RemainingProductFactor.lean 2 declarations
• RemainingProductKernel.lean 3 declarations
• RemainingProductMass.lean 4 declarations
• RemainingProductReorder.lean 8 declarations
• RemainingProductSupport.lean 6 declarations
• RemainingProjectiveEquality.lean 6 declarations
• RemainingRebase.lean 12 declarations
• RemainingRootCoordinates.lean 9 declarations
• RemainingRootHolonomy.lean 14 declarations
• RemainingRootProductBoxes.lean 11 declarations
• RepeatedRoot.lean 5 declarations
• RestrictedCoordinateMap.lean 1 declarations
• RestrictedLeafProduct.lean 2 declarations
• RightHaarProduct.lean 3 declarations
• RightObservableUniformity.lean 4 declarations
• RootAtomicTransversal.lean 2 declarations
• RootBalanceSymmetry.lean 2 declarations
• RootBoxMargins.lean 3 declarations
• RootCoefficientReduction.lean 11 declarations
• RootCommutator.lean 2 declarations
• RootCompactTransversals.lean 1 declarations
• RootContraction.lean 5 declarations
• RootCoordinateRestrictions.lean 1 declarations
• RootCurveExtraction.lean 9 declarations
• RootFactorHolonomy.lean 2 declarations
• RootFactorTransversal.lean 2 declarations
• RootFiberConstancy.lean 2 declarations
• RootFiberReference.lean 4 declarations
• RootFiberReferenceCovariance.lean 1 declarations
• RootHolonomy.lean 1 declarations
• RootHorosphereGroup.lean 8 declarations
• RootInductionStep.lean 3 declarations
• RootLeafLowerBound.lean 6 declarations
• RootMatrixDensity.lean 5 declarations
• RootOrderCoordinates.lean 3 declarations
• RootPairCoordinates.lean 2 declarations
• RootPairSourceSet.lean 1 declarations
• RootPairTimeSelection.lean 3 declarations
• RootPrefixAmbientGood.lean 2 declarations
• RootPrefixAmbientStationarity.lean 1 declarations
• RootPrefixBasedMeasure.lean 7 declarations
• RootPrefixBoxes.lean 15 declarations
• RootPrefixCompatibility.lean 13 declarations
• RootPrefixCoordinates.lean 9 declarations
• RootPrefixCountableAtlas.lean 1 declarations
• RootPrefixFactorChart.lean 11 declarations
• RootPrefixGroupLeaves.lean 5 declarations
• RootPrefixIntrinsicCandidates.lean 2 declarations
• RootPrefixLeafKernel.lean 4 declarations
• RootPrefixLeafMeasure.lean 2 declarations
• RootPrefixLeafSupport.lean 2 declarations
• RootPrefixLift.lean 4 declarations
• RootPrefixLocalRestriction.lean 2 declarations
• RootPrefixLongBoxes.lean 3 declarations
• RootPrefixNormalizedLeaves.lean 8 declarations
• RootPrefixNullAmbient.lean 1 declarations
• RootPrefixNullStationarity.lean 2 declarations
• RootPrefixPositiveAtoms.lean 2 declarations
• RootPrefixProductKernel.lean 5 declarations
• RootPrefixRegionCandidates.lean 3 declarations
• RootPrefixRegularKernel.lean 11 declarations
• RootPrefixReorder.lean 5 declarations
• RootPrefixRestrictions.lean 2 declarations
• RootPrefixStationaryImages.lean 3 declarations
• RootPrefixSupport.lean 4 declarations
• RootPrefixTransverseProduct.lean 2 declarations
• RootPrefixWindows.lean 9 declarations
• RootProductCovariance.lean 2 declarations
• RootProductReorder.lean 6 declarations
• RootProductShear.lean 4 declarations
• RootRectangleInclusion.lean 3 declarations
• RootRectangleMeasures.lean 4 declarations
• RootRowProduct.lean 2 declarations
• RootRowShear.lean 9 declarations
• RootSourceOrder.lean 1 declarations
• RootStableHolonomy.lean 3 declarations
• RootTranslateBox.lean 5 declarations
• RootTranslateLeaves.lean 5 declarations
• RootTransverseRectangles.lean 4 declarations
• RootVectorDensity.lean 8 declarations
• RootWeights.lean 3 declarations
• RowCubes.lean 7 declarations
• RowIndependentCoordinates.lean 6 declarations
• RowLeafConstancy.lean 5 declarations
• RowLeafProduct.lean 3 declarations
• RowLongBoxes.lean 5 declarations
• RowReducedChart.lean 2 declarations
• RowRootBox.lean 16 declarations
• RowRootChart.lean 17 declarations
• RowSingleBox.lean 7 declarations
• RowSingleMeasure.lean 4 declarations
• RowTimeSplit.lean 8 declarations
• SampledFactorIdentification.lean 1 declarations
• ScaledMatrixBalls.lean 2 declarations
• SeparatedControlledCuts.lean 1 declarations
• SeparatedCutFamily.lean 3 declarations
• SeparatedQuotientNet.lean 2 declarations
• ShiftedRealWindow.lean 1 declarations
• ShiftedRootLeafHolonomy.lean 2 declarations
• ShiftedRootProduct.lean 1 declarations
• ShiftedRootPullback.lean 6 declarations
• ShiftedRootWindowLeaf.lean 3 declarations
• SmallCommutingCorrections.lean 3 declarations
• SmallCompactHeight.lean 1 declarations
• SmallMatrixLength.lean 3 declarations
• SmallPositiveSection.lean 2 declarations
• SmallUpperRootAtlas.lean 3 declarations
• SparseUpperRootComparison.lean 4 declarations
• SpectralMoments.lean 3 declarations
• SpectralPerturbation.lean 6 declarations
• SpectralSeparation.lean 7 declarations
• StationaryRestrictions.lean 10 declarations
• SublinearHeight.lean 3 declarations
• SynchronizedAnnuli.lean 1 declarations
• TemperedChartRadius.lean 4 declarations
• TemperedCutBoundary.lean 1 declarations
• TerminalNeutralPairs.lean 3 declarations
• TerminalPairComparison.lean 4 declarations
• TranslatedNeutralProduct.lean 2 declarations
• TransverseDiagonalData.lean 9 declarations
• TransverseDiagonalFactorization.lean 3 declarations
• TransverseRootFibers.lean 3 declarations
• Tubes.lean 6 declarations
• UpperRootBasedMeasure.lean 10 declarations
• UpperRootChart.lean 17 declarations
• UpperRootContraction.lean 6 declarations
• UpperRootCoordinatesMeasure.lean 5 declarations
• UpperRootDiagonalCharts.lean 11 declarations
• UpperRootDilation.lean 4 declarations
• UpperRootDisintegration.lean 20 declarations
• UpperRootEuclideanCoordinates.lean 10 declarations
• UpperRootGlobalCoordinates.lean 10 declarations
• UpperRootGroupLeaves.lean 6 declarations
• UpperRootLeafDiagonal.lean 4 declarations
• UpperRootLeafKernel.lean 4 declarations
• UpperRootLeafMeasure.lean 4 declarations
• UpperRootLeafSupport.lean 2 declarations
• UpperRootLogContraction.lean 5 declarations
• UpperRootLongBoxes.lean 7 declarations
• UpperRootMeasureCovariance.lean 16 declarations
• UpperRootNormalizedLeaves.lean 8 declarations
• UpperRootRebase.lean 7 declarations
• UpperRootRegularKernel.lean 11 declarations
• UpperRootRestrictions.lean 13 declarations
• UpperRootUniformContraction.lean 2 declarations
• UpperRootWindows.lean 19 declarations
• VaryingCutBoundary.lean 1 declarations
• WeakLimits.lean 4 declarations
• WeakStableFactorization.lean 2 declarations
• WeylDiagonalAction.lean 6 declarations
• WeylReindex.lean 8 declarations
• WeylRootBoxes.lean 8 declarations
• WeylRootLeaves.lean 5 declarations