OAI/NumberTheory/Ostmann/Tree/
1209 declarations, 0 contain sorry, 0 declared as axioms; 198 files
Files
- AffineEnergy.lean 8 declarations
- AffineFibers.lean 12 declarations
- AffineFourier.lean 7 declarations
- AffineHilbertSchmidt.lean 6 declarations
- AffinePairAlgebra.lean 5 declarations
- AffinePairIdentity.lean 4 declarations
- AffineSelfBound.lean 2 declarations
- AffineUnitEnergy.lean 6 declarations
- ArrangementGraph.lean 10 declarations
- ArrangementReindex.lean 4 declarations
- ArrangementTreeComparison.lean 2 declarations
- Autocorrelation.lean 5 declarations
- BadArrangementCount.lean 4 declarations
- BadArrangementFraction.lean 2 declarations
- BadConvolution.lean 3 declarations
- BadNonprincipalConvolution.lean 1 declarations
- BadPartitionCounts.lean 9 declarations
- BadPrincipalConvolution.lean 5 declarations
- BottomPairCoordinates.lean 6 declarations
- CellGroupExponentialCost.lean 2 declarations
- CellGroupPigeonhole.lean 7 declarations
- CellListPigeonhole.lean 5 declarations
- CharacterFourth.lean 5 declarations
- CharacterFourthNonprincipal.lean 3 declarations
- ComponentFactorial.lean 4 declarations
- ComponentFibers.lean 7 declarations
- ConstrainedCharacterSum.lean 2 declarations
- CoordinateAverages.lean 11 declarations
- CorrelationSymmetry.lean 5 declarations
- CoupledDiagramCorrelation.lean 5 declarations
- CoupledHaar.lean 10 declarations
- CrossMajorantBounds.lean 4 declarations
- CrossPairHeldAverage.lean 3 declarations
- CrossPairMajorant.lean 6 declarations
- CrossQuartetFiber.lean 10 declarations
- CrossedMoments.lean 1 declarations
- CutFiberAverage.lean 5 declarations
- CycleCut.lean 5 declarations
- CycleExistence.lean 4 declarations
- CycleFiberProjection.lean 7 declarations
- CycleLocalMajorantsBasic.lean 13 declarations
- CycleLocalMajorantsCoefficients.lean 11 declarations
- CycleLocalMajorantsFrames.lean 3 declarations
- CycleProducts.lean 4 declarations
- CycleProjection.lean 8 declarations
- CycleQuartetActions.lean 10 declarations
- CycleQuartetActionsClassification.lean 15 declarations
- CycleQuartetActionsCoordinates.lean 9 declarations
- CycleQuartetActionsSelected.lean 14 declarations
- CycleQuartets.lean 4 declarations
- CycleSelection.lean 12 declarations
- CycleSigned.lean 17 declarations
- CycleWalk.lean 5 declarations
- DeletedPairEnergy.lean 7 declarations
- DensityAlgebra.lean 6 declarations
- DensityCut.lean 13 declarations
- DensityDomination.lean 7 declarations
- DensityFibers.lean 5 declarations
- DensityHorizontal.lean 7 declarations
- DensityL2.lean 5 declarations
- DensityReconstruction.lean 16 declarations
- DensitySplit.lean 4 declarations
- DensityValues.lean 9 declarations
- DiagonalMellin.lean 2 declarations
- Diagram.lean 15 declarations
- DifferenceConvolution.lean 6 declarations
- DoubleMellinEnergy.lean 3 declarations
- FiberProjection.lean 7 declarations
- FiniteActionAverage.lean 8 declarations
- Fourier.lean 12 declarations
- FriendlyConvolution.lean 1 declarations
- FriendlyQuartet.lean 2 declarations
- FriendlyRightConvolution.lean 1 declarations
- HorizontalProjectionBound.lean 6 declarations
- IncidenceCirculation.lean 13 declarations
- IncidenceCycle.lean 4 declarations
- IncidenceCycleSigns.lean 8 declarations
- IndependentCoordinate.lean 2 declarations
- IndependentMajorants.lean 5 declarations
- IndependentUniformBound.lean 1 declarations
- MeanInner.lean 12 declarations
- Mellin.lean 8 declarations
- MellinSquare.lean 6 declarations
- MellinTransform.lean 3 declarations
- NonnegativeDifference.lean 5 declarations
- OmittedCoordinate.lean 2 declarations
- PairCoefficientMeans.lean 4 declarations
- PairCoordinates.lean 7 declarations
- PairEnergy.lean 6 declarations
- PairFourierMass.lean 10 declarations
- PairMellin.lean 5 declarations
- PairMellinVariables.lean 9 declarations
- PairMobius.lean 6 declarations
- PairMoment.lean 4 declarations
- PairOrientationValue.lean 4 declarations
- PairPopulationFibers.lean 6 declarations
- PairSecondMoment.lean 7 declarations
- PairSpectrum.lean 14 declarations
- PairSquareMoment.lean 7 declarations
- PairTotalMass.lean 1 declarations
- PairedFrequencyProjection.lean 3 declarations
- PairedPartitions.lean 5 declarations
- PairedRationalReduction.lean 3 declarations
- ParallelCycle.lean 7 declarations
- Parseval.lean 2 declarations
- PartitionMatching.lean 8 declarations
- PartitionProducts.lean 6 declarations
- PreorderNodePaths.lean 8 declarations
- PrincipalSpectrum.lean 5 declarations
- ProductFibers.lean 6 declarations
- QuarterPowerBound.lean 2 declarations
- QuartetActions.lean 19 declarations
- QuartetAverage.lean 4 declarations
- QuartetBlockFamily.lean 12 declarations
- QuartetBlockMoments.lean 7 declarations
- QuartetBlockRoot.lean 6 declarations
- QuartetCoefficient.lean 2 declarations
- QuartetCoordinates.lean 25 declarations
- QuartetCrossAction.lean 5 declarations
- QuartetCrossBound.lean 6 declarations
- QuartetDiagram.lean 11 declarations
- QuartetFactorRatios.lean 14 declarations
- QuartetFactorization.lean 10 declarations
- QuartetFactorizationArguments.lean 4 declarations
- QuartetFactorizationFibers.lean 1 declarations
- QuartetFactorizationFrames.lean 9 declarations
- QuartetFactorizationLeaves.lean 12 declarations
- QuartetFactorizationValidity.lean 2 declarations
- QuartetFamily.lean 15 declarations
- QuartetFamilyParameters.lean 7 declarations
- QuartetFamilyPullback.lean 5 declarations
- QuartetFamilyValue.lean 7 declarations
- QuartetFiberIndependence.lean 3 declarations
- QuartetHeld.lean 12 declarations
- QuartetLocal.lean 9 declarations
- QuartetMellinPullback.lean 2 declarations
- QuartetMobiusMellin.lean 2 declarations
- QuartetPairMajorant.lean 7 declarations
- QuartetPairMeasure.lean 6 declarations
- QuartetPairValues.lean 8 declarations
- QuartetProductFiber.lean 7 declarations
- QuartetRatioConvolution.lean 2 declarations
- QuartetRemainingMeans.lean 8 declarations
- QuartetSameBound.lean 7 declarations
- QuartetSquareMeasure.lean 6 declarations
- QuartetUniformMeans.lean 12 declarations
- QuartetZero.lean 8 declarations
- QuarticCollision.lean 3 declarations
- QuarticWeighted.lean 8 declarations
- RatioOrthogonality.lean 7 declarations
- RationalPairValue.lean 1 declarations
- RationalProfileLeaves.lean 3 declarations
- RationalQuartetCut.lean 15 declarations
- RationalQuartetValue.lean 6 declarations
- RationalTree.lean 11 declarations
- RationalTreeLeaves.lean 7 declarations
- RationalTreeProfile.lean 5 declarations
- ReciprocalCoordinates.lean 4 declarations
- ReciprocalDiagonal.lean 2 declarations
- ReciprocalPair.lean 3 declarations
- ReciprocalTwist.lean 7 declarations
- SamePairFiber.lean 10 declarations
- SamePairHeldAverage.lean 2 declarations
- SamePairMajorant.lean 8 declarations
- SamePairMeanBounds.lean 2 declarations
- SampleEqualityPatterns.lean 6 declarations
- SignedCycleBound.lean 3 declarations
- SmallDepthMatchingCount.lean 5 declarations
- SpectralFourth.lean 2 declarations
- SpectralGaussBound.lean 3 declarations
- SpectralParts.lean 8 declarations
- SquareMajorant.lean 4 declarations
- TensorActionMajorization.lean 2 declarations
- TensorActionProjection.lean 5 declarations
- TensorCharacters.lean 6 declarations
- TensorParseval.lean 3 declarations
- TensorProjection.lean 11 declarations
- TreeComparison.lean 5 declarations
- TreeComparisonSquared.lean 3 declarations
- TreeFiberMajorization.lean 1 declarations
- TreeMajorant.lean 5 declarations
- TreeProjectionBound.lean 1 declarations
- TruncatedModePairing.lean 6 declarations
- TwistedPairSpectrum.lean 5 declarations
- TwoPairBare.lean 4 declarations
- TwoPairConvolution.lean 3 declarations
- TwoPairMellin.lean 1 declarations
- TwoPairModeBounds.lean 3 declarations
- TwoPairRatioEnergy.lean 4 declarations
- TwoVertexReindex.lean 8 declarations
- UniformCoordinateAverage.lean 1 declarations
- UniformGroupReduction.lean 4 declarations
- UniformMellin.lean 1 declarations
- UnitSums.lean 3 declarations
- UntouchedQuartetBound.lean 3 declarations
- WeightedAffine.lean 8 declarations
- WeightedAffineBound.lean 1 declarations
- WeightedFourierGauss.lean 2 declarations