`OAI/NumberTheory/OrdinaryCorrelations/HighTrace/`

2105 declarations, 0 contain sorry, 0 declared as axioms; 269 files

Files

AbsPrimeMeanLe.lean 3 declarations
ActiveComponents.lean 11 declarations
ActiveReachable.lean 3 declarations
ActivityGapIndices.lean 2 declarations
ActivityResidue.lean 5 declarations
AffineResidueEquiv.lean 6 declarations
AllCoreLit.lean 6 declarations
AllForward.lean 2 declarations
AllSlotMasses.lean 2 declarations
AmplitudeGeOne.lean 16 declarations
Append.lean 2 declarations
ArithmeticClause.lean 6 declarations
ArithmeticSum.lean 4 declarations
AttachedMetadata.lean 12 declarations
Avg.lean 14 declarations
AvgAdd.lean 6 declarations
AvgFintypeChange.lean 9 declarations
AvoidEdgeSuffix.lean 1 declarations
BelowChain.lean 14 declarations
BetaZ.lean 15 declarations
BinWeight.lean 6 declarations
BitWeight.lean 23 declarations
Block.lean 8 declarations
BlockActiveCapacity.lean 1 declarations
BlockEdges.lean 7 declarations
BlockGateExists.lean 2 declarations
BoundedLists.lean 10 declarations
BoundedMultiplicity.lean 6 declarations
CardPrimesLe.lean 3 declarations
CardTreeVerticesLe.lean 18 declarations
CenterMassTendsto.lean 4 declarations
ChargeKappaPos.lean 5 declarations
ChargePivotAbsorption.lean 6 declarations
ChargedCorrectionSum.lean 4 declarations
ClosedLine.lean 12 declarations
CodeEntropyMass.lean 8 declarations
CoefficientEqSingle.lean 2 declarations
CoefficientZeroOfNotSupport.lean 8 declarations
ComponentBoundAfterGap.lean 3 declarations
ConnectedLitComponent.lean 3 declarations
ConnectedSet.lean 12 declarations
ConnectedSetPath.lean 9 declarations
Constant.lean 4 declarations
CoordinateEquiv.lean 9 declarations
CoreTupleBins.lean 2 declarations
CorruptWitness.lean 3 declarations
Cylinder.lean 19 declarations
CylinderBudget.lean 5 declarations
DataInjective.lean 6 declarations
DensitySizeLeTestSize.lean 6 declarations
Directed.lean 8 declarations
DisconnectedCertificate.lean 10 declarations
DisconnectedErrorSum.lean 4 declarations
DisconnectedWitness.lean 9 declarations
DisjointIntervals.lean 1 declarations
DivisorFamily.lean 16 declarations
DivisorPath.lean 12 declarations
DivisorPathFilling.lean 14 declarations
DivisorPathTemplate.lean 18 declarations
EarlierTuple.lean 3 declarations
EdgeAt.lean 12 declarations
EdgeGraph.lean 17 declarations
EdgeGraphMono.lean 3 declarations
EdgeInjective.lean 4 declarations
Edges.lean 9 declarations
Enum.lean 7 declarations
Epsilon.lean 28 declarations
EventuallyConstPowLeExp.lean 6 declarations
ExceptionalBudget.lean 10 declarations
ExceptionalCodeSlot.lean 12 declarations
ExistsNewPrime.lean 5 declarations
ExistsTreePathWithSupport.lean 1 declarations
Expression.lean 5 declarations
ExtFields.lean 9 declarations
FactorialTotal.lean 8 declarations
FactorsAppendSubset.lean 1 declarations
FarBlockPair.lean 4 declarations
FarCorrupted.lean 6 declarations
FarFilling.lean 16 declarations
FarTemplate.lean 14 declarations
FarTestSizePolynomial.lean 9 declarations
Fiber.lean 8 declarations
FiniteSumInstanceTransfer.lean 8 declarations
FirstEdges.lean 10 declarations
FirstSlot.lean 18 declarations
FixedCharges.lean 10 declarations
FixedDisconnected.lean 8 declarations
FixedIsTagged.lean 19 declarations
FlatCode.lean 11 declarations
FlatSlot.lean 6 declarations
ForestCuts.lean 1 declarations
ForwardSegment.lean 8 declarations
FreePieceWeight.lean 8 declarations
FreeResidues.lean 19 declarations
FreeSplit.lean 14 declarations
FullArithmeticTrace.lean 3 declarations
GapEmpty.lean 4 declarations
GapFilling.lean 10 declarations
GapPathCode.lean 8 declarations
GapShapes.lean 4 declarations
GapTemplate.lean 10 declarations
GateAncestor.lean 3 declarations
GateSelection.lean 2 declarations
GeometryGoodEdges.lean 4 declarations
GeometryRetained.lean 2 declarations
GlobalRecord.lean 13 declarations
GoodGapTemplate.lean 5 declarations
GrowsSingleton.lean 9 declarations
HarmonicCongruenceBound.lean 3 declarations
IndependentTests.lean 1 declarations
Index.lean 15 declarations
IndexedWitnessFilling.lean 10 declarations
IntegerResidues.lean 9 declarations
IntegerResiduesAdd.lean 6 declarations
IntersectionEqBotOfSupport.lean 16 declarations
IntervalOverlap.lean 1 declarations
KappaPos.lean 8 declarations
LabelPrimeSet.lean 12 declarations
LabelPrimeSetEraseProduct.lean 11 declarations
LastEdge.lean 10 declarations
LineList.lean 14 declarations
LinePrimeCode.lean 7 declarations
LinePrimeMemFullUsed.lean 12 declarations
LinearCoeffZeroOfNot.lean 1 declarations
ListLocalLeOne.lean 5 declarations
ListSupport.lean 5 declarations
LitEdgesEmptyOfNo.lean 5 declarations
LitEdgesSubsetTree.lean 5 declarations
LocalIndicator.lean 11 declarations
LocalToken.lean 14 declarations
LocalUnlitCount.lean 5 declarations
LocalWithList.lean 13 declarations
Main.lean 48 imports, no declarations
MemSupport.lean 18 declarations
MemTakeIndex.lean 7 declarations
ModifiedWeightSameBand.lean 11 declarations
NoFixedQualifyingPath.lean 1 declarations
Nonempty.lean 10 declarations
NormalizedFiberWeight.lean 3 declarations
NumericalLine.lean 11 declarations
OfRelabel.lean 2 declarations
OffsetAbsLe.lean 4 declarations
Ordered.lean 10 declarations
OrderedSelection.lean 12 declarations
OrientedSubpathRefl.lean 5 declarations
PackedGapPrefactor.lean 4 declarations
PackedGapPrefactorMonoPath.lean 6 declarations
PackedGapSum.lean 4 declarations
PaddedGroupWeight.lean 7 declarations
PaddedWeightIdentity.lean 2 declarations
PathTop.lean 5 declarations
PivotEdges.lean 11 declarations
PostGapErrorSum.lean 3 declarations
Precedes.lean 8 declarations
PrefixCoefficientNondvd.lean 2 declarations
PrimeChargeProduct.lean 6 declarations
PrimeFactorsCardLeLog.lean 8 declarations
PrimeIndex.lean 14 declarations
PrimeOccurrenceInterval.lean 2 declarations
PrimeSystem.lean 38 declarations
PrivateFamily.lean 16 declarations
PrivateMono.lean 2 declarations
ProductCode.lean 1 declarations
RankBot.lean 8 declarations
Realizable.lean 5 declarations
RecordPacket.lean 9 declarations
RecordUntaggedSingleton.lean 8 declarations
RecordedTopOutgoing.lean 4 declarations
RecordedTops.lean 6 declarations
RelabelAppend.lean 3 declarations
RepeatedCenterUnlitCount.lean 6 declarations
RepeatedUnlitTotalEqFixed.lean 4 declarations
ResidualRankPrivateFamily.lean 1 declarations
Restrict.lean 12 declarations
RetainedKernel.lean 6 declarations
ReturnCountLe.lean 6 declarations
ReverseSegment.lean 6 declarations
RootCode.lean 14 declarations
RootNotDestination.lean 18 declarations
RowFactors.lean 4 declarations
SegmentEdges.lean 5 declarations
SelectedUsed.lean 10 declarations
Shape.lean 14 declarations
ShapeFromGrows.lean 3 declarations
ShapePivotBins.lean 2 declarations
SignedAssignedSum.lean 3 declarations
SingleEdgeWeight.lean 15 declarations
SizedSet.lean 36 declarations
SlotEdgeProduct.lean 3 declarations
SlotWeight.lean 5 declarations
SourceCoreEquiv.lean 9 declarations
SourceCylinderTruncation.lean 1 declarations
SourceDisconnectedCertificatesSmall.lean 3 declarations
SourceFullTraceRaw.lean 3 declarations
SourceLengthGe.lean 5 declarations
SourceListSlotBudget.lean 4 declarations
SourceManyWitnessTests.lean 2 declarations
SourcePivotAbsorb.lean 4 declarations
SourcePivotFactor.lean 7 declarations
SourcePolyDivTendsto.lean 4 declarations
SourcePrimeUpper.lean 3 declarations
SourcePrimitiveCoefficientInputs.lean 1 declarations
SourceReturnFactor.lean 2 declarations
SourceSystem.lean 16 declarations
SourceWitnessBasicScales.lean 3 declarations
SourceWitnessDelta.lean 4 declarations
SourceWitnessError.lean 6 declarations
SourceWitnessErrorBelowTrace.lean 8 declarations
SourceWitnessMajorant.lean 4 declarations
Spec.lean 10 declarations
SpecPrimeSlot.lean 18 declarations
SpecSegment.lean 6 declarations
SpecificationPrefactor.lean 6 declarations
SpecificationSlotCount.lean 15 declarations
SpecificationTemplate.lean 16 declarations
Splice.lean 15 declarations
SquarefreeExpression.lean 12 declarations
StepFactor.lean 8 declarations
Subpath.lean 3 declarations
SubtreeUnionWeightNonneg.lean 12 declarations
SumEquiv.lean 4 declarations
SumPeriodBlocks.lean 3 declarations
Support.lean 7 declarations
SupportEqUsed.lean 11 declarations
SupportIffExtraOrLabel.lean 7 declarations
Symbolic.lean 8 declarations
TaggedEdgeProduct.lean 7 declarations
TaggedShape.lean 8 declarations
TaggedShapeMap.lean 11 declarations
Test.lean 13 declarations
TestVacuous.lean 11 declarations
TiltedListLocalMean.lean 2 declarations
TokenSlot.lean 23 declarations
Topology.lean 12 declarations
TopologyTreeSteps.lean 11 declarations
TotalCodeMass.lean 1 declarations
TotalUnlitCountEqSubtype.lean 3 declarations
TreeBlocksWithEdges.lean 2 declarations
TreeDestinationInjective.lean 11 declarations
TreeEdge.lean 4 declarations
TreeEdgeInjective.lean 4 declarations
TreeOccurrences.lean 16 declarations
TreeOccurrencesEmptyOfFree.lean 12 declarations
TreePrimeSupport.lean 11 declarations
TreeVertices.lean 12 declarations
TwoBlockRerooting.lean 1 declarations
TwoTermBinomial.lean 8 declarations
UncutTreeEdges.lean 12 declarations
UnlitPolynomialBound.lean 3 declarations
Unselected.lean 10 declarations
UnselectedCard.lean 1 declarations
UntaggedEdgeCode.lean 7 declarations
UntaggedReferenceWeight.lean 10 declarations
UsedPrimeReciprocal.lean 10 declarations
VertexAt.lean 8 declarations
VertexIndex.lean 19 declarations
VertexWeight.lean 6 declarations
VerticesInBlock.lean 3 declarations
WalkBetweenSupport.lean 1 declarations
WalkSupportConnected.lean 1 declarations
WalkVertices.lean 2 declarations
Witness.lean 8 declarations
WitnessBaseDoublePath.lean 4 declarations
WitnessConfiguration.lean 12 declarations
WitnessEntropyBase.lean 4 declarations
WitnessSlotCount.lean 6 declarations
WitnessTestDescriptor.lean 15 declarations
WitnessTestShape.lean 9 declarations
ZeroExpression.lean 14 declarations