`OAI/NumberTheory/DirichletL/Reflection/`

819 declarations, 0 contain sorry, 0 declared as axioms; 266 files

Files

ActiveDictionary.lean 6 declarations
ActiveProducts.lean 3 declarations
Actual.lean 2 declarations
ActualBounds.lean 3 declarations
ActualExponent.lean 1 declarations
ActualExtractedEnergy.lean 1 declarations
ActualSelected.lean 1 declarations
ActualSizeCaps.lean 4 declarations
ActualSizeCapsUniformDegree.lean 1 declarations
ActualWeightedEnergy.lean 2 declarations
AnnularExponent.lean 1 declarations
AnnularNormalization.lean 3 declarations
BoundedTemplates.lean 5 declarations
Brackets.lean 3 declarations
Branch.lean 4 declarations
BranchCount.lean 3 declarations
Canonical.lean 14 declarations
CanonicalCaps.lean 2 declarations
CanonicalCellArithmetic.lean 4 declarations
CanonicalChoiceEnergy.lean 1 declarations
CanonicalChoiceEnergyUniformDegree.lean 1 declarations
CanonicalDyads.lean 1 declarations
CanonicalDyadsUniformDegree.lean 1 declarations
CanonicalEnergy.lean 1 declarations
CanonicalEnergyUniformDegree.lean 1 declarations
CanonicalFrozenEnergy.lean 1 declarations
CanonicalFrozenEnergyUniformDegree.lean 1 declarations
CanonicalInactiveEnergy.lean 2 declarations
CanonicalInactiveEnergyUniformDegree.lean 1 declarations
CanonicalParameters.lean 2 declarations
CanonicalPool.lean 13 declarations
CanonicalWidth.lean 1 declarations
CellArithmetic.lean 3 declarations
ChoiceTransport.lean 8 declarations
Coefficient.lean 5 declarations
Cofactor.lean 4 declarations
Columns.lean 8 declarations
Common.lean 2 declarations
CommonMeasure.lean 1 declarations
CompletedAggregation.lean 1 declarations
CompletedCanonicalEnergy.lean 3 declarations
CompletedCanonicalEnergyUniformDegree.lean 1 declarations
CompletedFiberSource.lean 3 declarations
CompletedRowsEnergy.lean 1 declarations
CompletedRowsEnergyUniformDegree.lean 1 declarations
CoprimeSource.lean 3 declarations
CountBudget.lean 4 declarations
Cross.lean 2 declarations
CrudeCoefficient.lean 3 declarations
CubeCompletedEnergy.lean 1 declarations
CubeCompletedEnergyUniformDegree.lean 1 declarations
CubeSlotBounds.lean 5 declarations
CubeSlotChoices.lean 9 declarations
CubeSlotEnergy.lean 1 declarations
CubeSlotSource.lean 6 declarations
CubeSlots.lean 5 declarations
Denominator.lean 6 declarations
DyadBudget.lean 2 declarations
DyadCompletionEnergy.lean 3 declarations
DyadReassembly.lean 5 declarations
DyadSelection.lean 4 declarations
DyadicBox.lean 6 declarations
DyadicTail.lean 5 declarations
Energy.lean 4 declarations
ExtractedEnergy.lean 2 declarations
ExtractedKernel.lean 8 declarations
ExtractedRow.lean 3 declarations
Extraction.lean 3 declarations
Family.lean 4 declarations
FamilyFactorization.lean 1 declarations
FamilyTail.lean 6 declarations
FamilyTailUniformDegree.lean 1 declarations
FilteredEnergy.lean 1 declarations
FilteredMeasure.lean 1 declarations
FixedLevel.lean 8 declarations
FixedTuples.lean 6 declarations
Frozen.lean 6 declarations
FrozenNorms.lean 5 declarations
FrozenSplit.lean 5 declarations
FullBudget.lean 1 declarations
FullBudgetUniformDegree.lean 1 declarations
FullDyadic.lean 3 declarations
FullEnergyBasic.lean 2 declarations
FullRaw.lean 8 declarations
Functions.lean 4 declarations
GlobalBudget.lean 1 declarations
GlobalBudgetUniformDegree.lean 1 declarations
GlobalEnergy.lean 2 declarations
HeightTail.lean 1 declarations
IdealBridge.lean 5 declarations
InactiveAggregation.lean 3 declarations
InactiveBudget.lean 3 declarations
InactiveEnergy.lean 3 declarations
InactiveRows.lean 3 declarations
InactiveSource.lean 2 declarations
Independent.lean 9 declarations
KernelActual.lean 6 declarations
KernelActualSource.lean 1 declarations
KernelAdmissible.lean 4 declarations
KernelBaseline.lean 1 declarations
KernelGeometry.lean 10 declarations
KernelIntegral.lean 3 declarations
KernelSeparation.lean 7 declarations
KernelSource.lean 1 declarations
KernelWeights.lean 11 declarations
LiteralNormalized.lean 1 declarations
LiteralNormalizedUniformDegree.lean 1 declarations
Local.lean 3 declarations
LowBranchSum.lean 1 declarations
LowCaps.lean 2 declarations
LowChoiceEnergy.lean 1 declarations
LowCompletedFiber.lean 1 declarations
LowCompletedRows.lean 1 declarations
LowDyads.lean 1 declarations
LowExponent.lean 1 declarations
LowFixedMember.lean 1 declarations
LowFrozenEnergy.lean 1 declarations
LowFull.lean 1 declarations
LowFullBudget.lean 1 declarations
LowGlobalBudget.lean 1 declarations
LowInactiveEnergy.lean 1 declarations
LowMemberBudget.lean 1 declarations
LowMemberGeometry.lean 1 declarations
LowOriginalEnergy.lean 1 declarations
LowPunctureLists.lean 4 declarations
LowRetained.lean 1 declarations
LowRetainedBudget.lean 1 declarations
LowSector.lean 1 declarations
LowWidth.lean 4 declarations
MarkedActiveSets.lean 4 declarations
MarkedActualSource.lean 5 declarations
MarkedChosenDual.lean 2 declarations
MarkedChosenSource.lean 1 declarations
MarkedDualSource.lean 2 declarations
MarkedFiber.lean 3 declarations
MarkedInactive.lean 4 declarations
MarkedJoined.lean 3 declarations
MarkedLevel.lean 4 declarations
MarkedOverlap.lean 4 declarations
MarkedRestriction.lean 5 declarations
MarkedRow.lean 7 declarations
MarkedSource.lean 5 declarations
MarkedTuples.lean 2 declarations
Matrices.lean 2 declarations
MemberBudget.lean 1 declarations
MemberBudgetUniformDegree.lean 1 declarations
MemberChoiceTransport.lean 4 declarations
MemberGeometry.lean 1 declarations
MemberGeometryUniformDegree.lean 1 declarations
Moving.lean 9 declarations
NormalizedColumns.lean 7 declarations
NormalizedEnergy.lean 1 declarations
NormalizedPhysical.lean 1 declarations
Norms.lean 6 declarations
OptionalWidth.lean 1 declarations
OriginalActiveReflection.lean 1 declarations
OriginalAggregation.lean 2 declarations
OriginalBranchSum.lean 1 declarations
OriginalCellBounds.lean 4 declarations
OriginalChoiceControl.lean 3 declarations
OriginalChoicePhysical.lean 2 declarations
OriginalChosen.lean 2 declarations
OriginalCompletedEnergy.lean 1 declarations
OriginalCompletedEnergyUniformDegree.lean 1 declarations
OriginalDictionary.lean 5 declarations
OriginalExponent.lean 1 declarations
OriginalFiber.lean 1 declarations
OriginalFull.lean 1 declarations
OriginalFullUniformDegree.lean 2 declarations
OriginalMask.lean 2 declarations
OriginalRetained.lean 1 declarations
OriginalRetainedSlots.lean 4 declarations
OriginalRetainedUniformDegree.lean 1 declarations
OriginalSaving.lean 1 declarations
OriginalSector.lean 1 declarations
OriginalSectorUniformDegree.lean 1 declarations
OriginalSlotSupport.lean 5 declarations
OriginalSplitReflection.lean 1 declarations
OriginalTransport.lean 5 declarations
OriginalWeights.lean 4 declarations
Partition.lean 1 declarations
PhysicalBranchMeasure.lean 1 declarations
PhysicalEnergy.lean 1 declarations
PhysicalIntegral.lean 3 declarations
PoolArithmetic.lean 7 declarations
PowerfulBudget.lean 3 declarations
Projections.lean 4 declarations
Pullback.lean 4 declarations
PunctureAbsorption.lean 4 declarations
PunctureLists.lean 5 declarations
PuncturedMarks.lean 2 declarations
Ramified.lean 3 declarations
RamifiedWidth.lean 5 declarations
RawCoefficient.lean 3 declarations
RawTail.lean 6 declarations
Reindex.lean 6 declarations
ReindexReflection.lean 7 declarations
RetainedBudget.lean 1 declarations
RetainedBudgetUniformDegree.lean 1 declarations
RetainedCaps.lean 4 declarations
RetainedWidth.lean 2 declarations
RowReindex.lean 5 declarations
RowTail.lean 3 declarations
RowTailUniformDegree.lean 1 declarations
Rows.lean 11 declarations
Sector.lean 5 declarations
SectorAggregation.lean 4 declarations
SectorCover.lean 2 declarations
SectorData.lean 2 declarations
SectorIndependence.lean 8 declarations
SectorNormalized.lean 1 declarations
SectorNormalizedUniformDegree.lean 1 declarations
SelectedExpansion.lean 3 declarations
Shape.lean 5 declarations
ShapeWeights.lean 6 declarations
ShellDomains.lean 7 declarations
ShellRows.lean 2 declarations
ShellSource.lean 3 declarations
SlotChoices.lean 6 declarations
SlotCoefficients.lean 5 declarations
SlotMass.lean 3 declarations
SourceBudget.lean 1 declarations
SourceCost.lean 2 declarations
SourceFamily.lean 3 declarations
SourcePhysical.lean 2 declarations
SourceScaleCaps.lean 3 declarations
SourceSectors.lean 1 declarations
SourceSelection.lean 4 declarations
SourceSum.lean 3 declarations
Split.lean 3 declarations
Static.lean 2 declarations
SumEnergy.lean 1 declarations
SumMeasure.lean 1 declarations
SupportedChoices.lean 4 declarations
Surviving.lean 8 declarations
SurvivingEnergy.lean 1 declarations
SurvivingGate.lean 1 declarations
TailAbsorption.lean 4 declarations
TailEnergyBudget.lean 1 declarations
TailEnergyBudgetUniformDegree.lean 1 declarations
TerminalThreshold.lean 2 declarations
ThreeBlocks.lean 4 declarations
ThresholdError.lean 3 declarations
Transport.lean 6 declarations
TruncatedSource.lean 6 declarations
TupleDyads.lean 7 declarations
TupleFamily.lean 8 declarations
TupleMasks.lean 5 declarations
TupleMembers.lean 6 declarations
TupleSectors.lean 3 declarations
UniformFiltered.lean 2 declarations
UniformMeasure.lean 3 declarations
UniformNormalized.lean 2 declarations
UniformNormalizedUniformDegree.lean 1 declarations
UniformPhysical.lean 2 declarations
UniformPhysicalUniformDegree.lean 1 declarations
UniformSieve.lean 4 declarations
UniformTail.lean 3 declarations
UpperThreshold.lean 1 declarations
WeightedEnergy.lean 2 declarations
WeightedMeasurable.lean 1 declarations
WeightedSourceSum.lean 2 declarations
WholePair.lean 4 declarations
WholeRow.lean 3 declarations
WholeTail.lean 1 declarations
WholeTailUniformDegree.lean 1 declarations