OAI/Combinatorics/Progressions/Nilpotent/
1595 declarations, 0 contain sorry, 0 declared as axioms; 139 files
Files
- AdaptedBasisNilmanifold.lean 4 declarations
- AllocatedCandidateHistoryLocalNiltests.lean 1 declarations
- AllocatedExternalCandidateQuotientNiltests.lean 1 declarations
- AllocatedKeptCommonCurrentGradeLocalNiltest.lean 13 declarations
- AllocatedNiltestNativeDetection.lean 1 declarations
- AllocatedNiltestSourceSelection.lean 12 declarations
- AllocatedNiltestSupportedSlicedDetection.lean 3 declarations
- AllocatedOriginalDegreeQuotientBinNiltest.lean 9 declarations
- AllocatedPathwiseFrozenNiltestMajorWitness.lean 1 declarations
- AmbientBracketCorrectionPolynomials.lean 7 declarations
- AntisymmetricPairNiltest.lean 5 declarations
- BCHChartCutoffSmooth.lean 45 declarations
- BCHConjugationLinear.lean 90 declarations
- BCHDenominatorBudget.lean 9 declarations
- BCHLatticeImageGap.lean 40 declarations
- BCHNonlinearRemainder.lean 62 declarations
- BCHOrderedReduction.lean 4 declarations
- BCHOuterGridChangeBasis.lean 18 declarations
- BCHPairCoordinateMetric.lean 3 declarations
- BCHQuotientChart.lean 2 declarations
- BCHQuotientLocalIsometry.lean 49 declarations
- BCHSmoothChartPartition.lean 3 declarations
- BCHSmoothPartitionBudget.lean 36 declarations
- BCHSubgroupGridExistence.lean 49 declarations
- BCHSubmoduleRemainder.lean 4 declarations
- BCHUniformQuotientCharts.lean 35 declarations
- BlockLayerBracket.lean 4 declarations
- BoxNiltestDetection.lean 7 declarations
- BracketArrayEquation.lean 4 declarations
- BracketStepBudget.lean 7 declarations
- CanonicalReducedMajorTwistedNiltest.lean 20 declarations
- CellwiseNiltestDiscretization.lean 1 declarations
- ChosenBCHGrids.lean 2 declarations
- CommonProductNiltestFamily.lean 1 declarations
- CommonVariableDimensionNiltests.lean 12 declarations
- ComparisonLayerBracket.lean 4 declarations
- ControlledBracketToCurrentLayer.lean 8 declarations
- CoordinateNiltestSplitting.lean 1 declarations
- CoveredAnchoredSquareNiltests.lean 2 declarations
- CubicPairNiltest.lean 5 declarations
- CubicPrimitiveNiltest.lean 2 declarations
- CurrentBracketInductionStep.lean 14 declarations
- CyclicNiltestApproximation.lean 50 declarations
- CyclicNiltestDetection.lean 7 declarations
- CyclicPairNiltestDetection.lean 1 declarations
- DegreeRankBCH.lean 13 declarations
- DegreeRankLieBrackets.lean 5 declarations
- DiagramExternalNetMaskedNiltests.lean 2 declarations
- DiagramExternalPhysicalNiltests.lean 1 declarations
- DualBCHDifferential.lean 20 declarations
- FactorwiseBCHCovers.lean 14 declarations
- FilteredAdjointFirstBracket.lean 29 declarations
- FixedPatchNiltestFamily.lean 1 declarations
- FormalMarkedNiltestRestoration.lean 1 declarations
- FreeDegreeRankNilmanifold.lean 11 declarations
- FreeNilpotentLieAlgebra.lean 14 declarations
- FreeNilpotentSourceBounds.lean 30 declarations
- FreeWeightedNilpotentLieAlgebra.lean 12 declarations
- FrozenComplexNiltest.lean 4 declarations
- IdealInvariantNiltestBudget.lean 29 declarations
- IntegralCentralNiltest.lean 1 declarations
- LieBCHContinuity.lean 128 declarations
- LinearBCHAbelian.lean 3 declarations
- LocalMajorDenseSliceNiltest.lean 58 declarations
- LocalNiltestFixedNativePartners.lean 15 declarations
- MajorTranslationPartnerNiltest.lean 2 declarations
- MajorTranslationRationalLiftNiltest.lean 4 declarations
- MatchedFlatNiltest.lean 1 declarations
- MissingCoordinateNiltestApproximation.lean 2 declarations
- MixedPrimitiveNiltest.lean 2 declarations
- NativeAnchoredSquareNiltests.lean 2 declarations
- NativeCoverNiltest.lean 18 declarations
- NativeFrozenMultidegreeNiltest.lean 1 declarations
- NativeIntegerChartNiltest.lean 15 declarations
- NativeMixedPairNiltest.lean 5 declarations
- NativeMultidegreeNiltest.lean 5 declarations
- NativeNilsequenceExpansion.lean 7 declarations
- NativeNiltestPartition.lean 1 declarations
- NativeRankZeroNiltest.lean 19 declarations
- NativeResetBracketGeometry.lean 6 declarations
- NativeResidueNiltests.lean 7 declarations
- NativeSquareNiltest.lean 9 declarations
- NilpotentBilinearExponential.lean 1 declarations
- NiltestAffineProjection.lean 38 declarations
- NiltestBasepointNormalization.lean 62 declarations
- NiltestComplement.lean 29 declarations
- NiltestOrbitOne.lean 5 declarations
- NiltestProbabilityProjection.lean 13 declarations
- NiltestScalarTransfer.lean 11 declarations
- NiltestVerticalBounds.lean 10 declarations
- PolarizedVerticalNiltest.lean 6 declarations
- PolynomialBCHRemoval.lean 6 declarations
- PolynomialPatchWeightedChartNiltest.lean 16 declarations
- PolynomialPotentialBCHHom.lean 5 declarations
- PolynomialShearBCH.lean 7 declarations
- PolynomialShearBCHOver.lean 6 declarations
- PolynomialShearNilmanifold.lean 8 declarations
- PositiveNiltestDiscretization.lean 1 declarations
- PositivePolynomialFactorNiltests.lean 5 declarations
- PositiveShiftTestingNiltests.lean 4 declarations
- PreparedAdditionNiltest.lean 2 declarations
- PreparedDilationNiltest.lean 1 declarations
- PreparedFiniteScheduleAllNilmanifoldMaskProductiveGood.lean 1 declarations
- PreparedFiniteScheduleAllNilmanifoldModel.lean 1 declarations
- QuadraticPrimitiveNiltest.lean 1 declarations
- QuarticPairNiltest.lean 5 declarations
- QuarticPrimitiveNiltest.lean 2 declarations
- QuotientSectionNiltests.lean 1 declarations
- RankAdaptedNiltest.lean 13 declarations
- RankBracketFactorizationMonotone.lean 10 declarations
- RankInvariantNiltestBudget.lean 2 declarations
- RationalBCHProducts.lean 7 declarations
- RealBCHOrderedReduction.lean 4 declarations
- RealFunctionalBCH.lean 3 declarations
- RealPolynomialBCH.lean 18 declarations
- RealifiedBCHFiniteAtlas.lean 23 declarations
- RealifiedBCHProductEquiv.lean 3 declarations
- RealifiedBCHSmoothPartition.lean 4 declarations
- RealizedDualBCH.lean 1 declarations
- RelativeScalarNiltestConclusion.lean 4 declarations
- SimultaneousNiltestFactorization.lean 3 declarations
- SquarefreeBracketCoefficients.lean 5 declarations
- SquarefreeBracketHeight.lean 15 declarations
- SquarefreeSupportBracket.lean 1 declarations
- StepOneGradedNiltestSplitting.lean 5 declarations
- SumNilmanifoldFactors.lean 9 declarations
- TopInvariantNiltestBudget.lean 2 declarations
- TotalDegreeNiltestSplitting.lean 1 declarations
- UnconditionedArbitraryNiltestBase.lean 1 declarations
- UnconditionedScalarScaleNiltestBase.lean 7 declarations
- UniformControlledBracketStage.lean 10 declarations
- UnitComparisonNiltest.lean 3 declarations
- VectorPolynomialSupportBracket.lean 1 declarations
- WeightedTranslationNilmanifold.lean 5 declarations
- WeightedTranslationRealBCHCoordinates.lean 15 declarations
- WeightedTranslationResidueNilmanifold.lean 3 declarations
- WeightedTranslationTwistedNiltest.lean 8 declarations
- WordTruncationBracket.lean 5 declarations
- ZeroLayerPhysicalNiltestBudget.lean 2 declarations