OAI/NumberTheory/DirichletL/Energy/
798 declarations, 0 contain sorry, 0 declared as axioms; 208 files
Files
- ActiveChildRestoration.lean 2 declarations
- AllocatedBound.lean 1 declarations
- AllocatedChildren.lean 7 declarations
- AllocatedClipped.lean 6 declarations
- AllocatedHomogeneous.lean 1 declarations
- AllocatedPaid.lean 1 declarations
- AllocatedProfiles.lean 2 declarations
- AllocatedZero.lean 3 declarations
- AmplifiedChildWidth.lean 16 declarations
- AmplifiedRayDictionary.lean 25 declarations
- AmplifierFamilyAdmission.lean 3 declarations
- BackwardSourceRanges.lean 13 declarations
- BandMonotonicity.lean 7 declarations
- BandSubtypeTransport.lean 2 declarations
- Bands.lean 6 declarations
- CanonicalAmplifiedColumn.lean 3 declarations
- CanonicalAmplifiedUniform.lean 2 declarations
- CanonicalAnnularLower.lean 7 declarations
- CanonicalAnnularPower.lean 1 declarations
- CanonicalChildBound.lean 1 declarations
- CanonicalCommonPaid.lean 1 declarations
- CanonicalErrorAdmitted.lean 1 declarations
- CanonicalErrorGaussian.lean 1 declarations
- CanonicalErrorHomogeneous.lean 1 declarations
- CanonicalErrorPaid.lean 10 declarations
- CanonicalErrorPower.lean 1 declarations
- CanonicalErrorSubsets.lean 1 declarations
- CanonicalErrorUniform.lean 1 declarations
- CanonicalHighColumn.lean 1 declarations
- CanonicalHighPhysical.lean 1 declarations
- CanonicalHighSource.lean 1 declarations
- CanonicalLiveBound.lean 3 declarations
- CanonicalLiveCapacity.lean 2 declarations
- CanonicalLowColumn.lean 3 declarations
- CanonicalLowPhysical.lean 1 declarations
- CanonicalLowSource.lean 1 declarations
- CanonicalMainGaussian.lean 1 declarations
- CanonicalMainHomogeneous.lean 1 declarations
- CanonicalMainPaid.lean 2 declarations
- CanonicalMainSeparated.lean 1 declarations
- CanonicalMainSeparatedPower.lean 1 declarations
- CanonicalMainSubsets.lean 1 declarations
- CanonicalMainUniform.lean 1 declarations
- CanonicalNestedReference.lean 1 declarations
- CanonicalPaidSource.lean 1 declarations
- CanonicalReferencePaid.lean 1 declarations
- CanonicalRightSourceColumn.lean 2 declarations
- CanonicalUniformReference.lean 1 declarations
- CapacityRemoval.lean 9 declarations
- CappedAnalyticSuccessor.lean 1 declarations
- CappedBandTransport.lean 1 declarations
- CappedLowStage.lean 1 declarations
- CappedRadialTransport.lean 2 declarations
- CappedRequests.lean 8 declarations
- CappedSuccessorPacking.lean 1 declarations
- CappedWidthInduction.lean 9 declarations
- CertifiedExistence.lean 2 declarations
- ChildEnvelopeFitting.lean 5 declarations
- ChildState.lean 9 declarations
- DeletedChildCapacity.lean 16 declarations
- DeletedRobustGeometry.lean 1 declarations
- FirstActualFrequencyBudget.lean 3 declarations
- FirstAnnularAdmission.lean 9 declarations
- FirstColumnPairing.lean 3 declarations
- FirstDeclaredCapacityLossBudget.lean 2 declarations
- FirstGaussianCoefficients.lean 7 declarations
- FirstGaussianProfileWeights.lean 4 declarations
- FirstHighExceptionalPowers.lean 2 declarations
- FirstHighFourCoefficients.lean 3 declarations
- FirstHighGaussianUniformPowers.lean 3 declarations
- FirstHighNormalizedGaussianPowers.lean 1 declarations
- FirstLiveAdmission.lean 19 declarations
- FirstLowHomogeneousPowers.lean 1 declarations
- FirstNormalizedGaussianPowers.lean 1 declarations
- FirstPhysicalNormalization.lean 15 declarations
- FirstRawScaleAdmission.lean 6 declarations
- FirstRightAdmission.lean 4 declarations
- FirstSourceParameters.lean 8 declarations
- FirstStageLossBudget.lean 3 declarations
- FirstTwoSeedAdmission.lean 2 declarations
- FixedRadialEntry.lean 2 declarations
- FixedRadialReduction.lean 1 declarations
- FixedRadialSource.lean 4 declarations
- Floor.lean 1 declarations
- InputParentCapacity.lean 10 declarations
- LiveClippingDefect.lean 23 declarations
- LowBandEmpty.lean 1 declarations
- LowBandSubtype.lean 2 declarations
- LowFixedRadialEntry.lean 4 declarations
- NaturalHighStage.lean 1 declarations
- NaturalInputMatches.lean 22 declarations
- NaturalLowPhysical.lean 1 declarations
- NaturalLowSourceBound.lean 4 declarations
- NaturalLowStage.lean 1 declarations
- NaturalSourceAdmission.lean 17 declarations
- NaturalZeroStage.lean 1 declarations
- OriginalHighReflectionBounded.lean 1 declarations
- OriginalHighReflectionDeleted.lean 1 declarations
- OriginalHighReflectionGeometry.lean 3 declarations
- OriginalHighReflectionOriginal.lean 1 declarations
- OriginalHighReflectionPower.lean 1 declarations
- OriginalHighReflectionSymmetric.lean 3 declarations
- OriginalHighReflectionSymmetricBounded.lean 1 declarations
- OriginalProfileControl.lean 10 declarations
- OriginalSource.lean 11 declarations
- PaidBands.lean 1 declarations
- PaidRemoval.lean 1 declarations
- PhysicalEntry.lean 3 declarations
- PositiveBalancedAdmission.lean 6 declarations
- PositiveHighAssembly.lean 2 declarations
- PositiveHighAssemblyBounded.lean 1 declarations
- PositiveHighBound.lean 1 declarations
- PositiveHighParameters.lean 6 declarations
- PositiveHighPhysical.lean 1 declarations
- PositiveHighSource.lean 5 declarations
- PositiveHighSourceBound.lean 4 declarations
- PositiveHighSourceBounded.lean 1 declarations
- PositiveLowBandSource.lean 2 declarations
- PositiveLowSourceControlled.lean 1 declarations
- Profiles.lean 17 declarations
- ReferenceChild.lean 5 declarations
- ReferenceChildProfiles.lean 5 declarations
- ReferenceDeletionBudget.lean 8 declarations
- ReferenceDeletionCapacity.lean 6 declarations
- ReferenceDeletionClipped.lean 2 declarations
- ReferenceDeletionEnergy.lean 1 declarations
- ReferenceDivisors.lean 4 declarations
- ReferenceHomogeneous.lean 1 declarations
- ReferenceHomogeneousError.lean 2 declarations
- ReferenceLiveBounded.lean 1 declarations
- ReferenceLivePower.lean 1 declarations
- ReferenceLowBands.lean 2 declarations
- ReferenceLowBranchGeometry.lean 5 declarations
- ReferenceLowChild.lean 2 declarations
- ReferenceLowControl.lean 2 declarations
- ReferenceLowDeletedGeometry.lean 1 declarations
- ReferenceLowDirect.lean 1 declarations
- ReferenceLowEmpty.lean 1 declarations
- ReferenceLowError.lean 1 declarations
- ReferenceLowMoments.lean 1 declarations
- ReferenceLowReflection.lean 1 declarations
- ReferenceLowReflectionError.lean 1 declarations
- ReferenceLowWindow.lean 2 declarations
- ReferenceProfileBudget.lean 2 declarations
- ReferenceReflection.lean 2 declarations
- ReferenceRobustBounded.lean 1 declarations
- ReferenceRobustDeletedEnergy.lean 1 declarations
- ReferenceRobustOriginal.lean 1 declarations
- ReferenceRobustPower.lean 1 declarations
- ReferenceScalarBounds.lean 6 declarations
- ReferenceScalarReserve.lean 2 declarations
- ReferenceSource.lean 3 declarations
- ReferenceState.lean 13 declarations
- ReferenceWeightedEnergy.lean 2 declarations
- Reindex.lean 3 declarations
- SlotHeight.lean 5 declarations
- SourceCapSchedule.lean 4 declarations
- SourceInputReindexGates.lean 27 declarations
- StageMargins.lean 5 declarations
- StageMonotonicity.lean 4 declarations
- StageReserve.lean 2 declarations
- StageReserveBounded.lean 1 declarations
- StageReserveSchedule.lean 6 declarations
- State.lean 8 declarations
- WidthFloor.lean 2 declarations
- WidthInduction.lean 9 declarations
- WidthRanges.lean 14 declarations
- WidthSchedule.lean 19 declarations
- ZeroBalancedAdmission.lean 6 declarations
- ZeroBalancedDictionary.lean 10 declarations
- ZeroComparison.lean 11 declarations
- ZeroGrowth.lean 4 declarations
- ZeroGrowthBounded.lean 1 declarations
- ZeroGrowthBounds.lean 2 declarations
- ZeroGrowthChild.lean 2 declarations
- ZeroGrowthConclusion.lean 4 declarations
- ZeroGrowthContourBounded.lean 3 declarations
- ZeroGrowthHighBound.lean 2 declarations
- ZeroGrowthMoments.lean 2 declarations
- ZeroGrowthOriginal.lean 4 declarations
- ZeroGrowthPhysical.lean 1 declarations
- ZeroGrowthPhysicalReindex.lean 5 declarations
- ZeroGrowthReflection.lean 1 declarations
- ZeroGrowthReserve.lean 2 declarations
- ZeroGrowthSource.lean 2 declarations
- ZeroGrowthSourceControlled.lean 1 declarations
- ZeroGrowthWindow.lean 1 declarations
- ZeroReferenceBounded.lean 1 declarations
- ZeroReferenceChild.lean 3 declarations
- ZeroReferenceDeleted.lean 1 declarations
- ZeroReferenceError.lean 1 declarations
- ZeroReferenceGeometry.lean 2 declarations
- ZeroReferenceLive.lean 1 declarations
- ZeroReferenceLiveBounded.lean 1 declarations
- ZeroReferenceMoments.lean 1 declarations
- ZeroReferenceOriginal.lean 1 declarations
- ZeroReferencePhysical.lean 3 declarations
- ZeroReferencePhysicalBounded.lean 1 declarations
- ZeroReferencePower.lean 1 declarations
- ZeroReferenceReflection.lean 1 declarations
- ZeroReflectionSupport.lean 11 declarations
- ZeroRetainedError.lean 6 declarations
- ZeroUnbalancedDeletedGeometry.lean 1 declarations
- ZeroUnbalancedOriginal.lean 1 declarations
- ZeroUnbalancedOriginalDeleted.lean 1 declarations
- ZeroUnbalancedOriginalGates.lean 2 declarations
- ZeroUnbalancedOriginalPower.lean 1 declarations
- ZeroUnbalancedOriginalSource.lean 1 declarations