OAI/NumberTheory/Ostmann/Conclusion/
286 declarations, 0 contain sorry, 0 declared as axioms; 71 files
Files
- ActualAmplitudeNorm.lean 7 declarations
- ActualComparisonConsumer.lean 1 declarations
- ActualComparisonContradiction.lean 1 declarations
- ActualComparisonObstruction.lean 1 declarations
- ActualComparisonObstructionInterface.lean 1 declarations
- ActualComparisonProviders.lean 4 declarations
- ActualComparisonSourceDefs.lean 2 declarations
- ActualComparisonSpectator.lean 4 declarations
- ActualCovariance.lean 4 declarations
- ActualCovarianceComplex.lean 3 declarations
- ActualDiagonalGoodComparison.lean 1 declarations
- ActualDiagonalGoodComparisonAssembly.lean 1 declarations
- ActualDiagonalGoodComparisonPoint.lean 1 declarations
- ActualDiagonalGoodComparisonPrincipal.lean 1 declarations
- ActualDiagonalGoodComparisonScalar.lean 1 declarations
- ActualFinalUpper.lean 1 declarations
- ActualFinalUpperRegular.lean 1 declarations
- ActualFourComparisonConsumer.lean 2 declarations
- ActualGoodCovarianceComparison.lean 1 declarations
- ActualGoodCovarianceComparisonAssembly.lean 1 declarations
- ActualGoodCovarianceComparisonBasic.lean 1 declarations
- ActualGoodCovarianceComparisonPrincipal.lean 1 declarations
- ActualNoDecomposition.lean 1 declarations
- ActualParameterChoice.lean 2 declarations
- ActualSymmetrization.lean 5 declarations
- ActualTransferLower.lean 1 declarations
- BadArrangementCount.lean 5 declarations
- BadFraction.lean 4 declarations
- BadPairAverages.lean 4 declarations
- BulkPermutation.lean 8 declarations
- BulkPositionPermutation.lean 9 declarations
- BulkPositionShape.lean 8 declarations
- BulkPositionShapeBasic.lean 14 declarations
- BulkPositionShapeOrder.lean 9 declarations
- ComponentFactorials.lean 4 declarations
- FinalRateAbsorption.lean 2 declarations
- FinalRateAbsorptionBasic.lean 4 declarations
- FinalRateAbsorptionScales.lean 3 declarations
- HistorySelectedCovarianceCauchy.lean 2 declarations
- HistorySelectedCovarianceCauchyActual.lean 2 declarations
- HistorySelectedCovarianceCauchyBasic.lean 3 declarations
- LowLevelBadPairs.lean 7 declarations
- MaskedPermutation.lean 5 declarations
- OverlapComponents.lean 15 declarations
- ParameterChoice.lean 2 declarations
- PartitionPermutations.lean 8 declarations
- PermutationSymmetrization.lean 12 declarations
- PriorSymmetrization.lean 4 declarations
- RegularNorm.lean 10 declarations
- RegularNormAP.lean 2 declarations
- RegularNormActual.lean 1 declarations
- RegularNormCell.lean 1 declarations
- RegularNormCellBounds.lean 3 declarations
- RegularNormCellEstimate.lean 1 declarations
- RegularNormGeneral.lean 5 declarations
- RegularNormPointwise.lean 4 declarations
- RegularNormPriors.lean 5 declarations
- RegularNormProduct.lean 3 declarations
- RegularNormResidue.lean 6 declarations
- RegularNormScale.lean 1 declarations
- RegularNormSourceRanges.lean 1 declarations
- RegularNormTestAP.lean 1 declarations
- RegularNormTuple.lean 2 declarations
- RegularNormTupleScale.lean 1 declarations
- ScaleReserves.lean 7 declarations
- Scales.lean 16 declarations
- SelectedCovarianceComplex.lean 4 declarations
- SelectedPermutation.lean 5 declarations
- SourcePermutation.lean 9 declarations
- SymmetrizedNorm.lean 5 declarations
- TransferRecurrence.lean 9 declarations