OAI/NumberTheory/DirichletL/Moments/

Files

• AbsoluteEnergy.lean 7 declarations
• Active.lean 11 declarations
• ActiveAllocation.lean 6 declarations
• ActiveCanonicalSource.lean 8 declarations
• ActiveDivisorShell.lean 8 declarations
• ActiveSmoothedSource.lean 1 declarations
• ActiveSource.lean 12 declarations
• ActiveSourceRetained.lean 1 declarations
• ActualLiveSlotRemoval.lean 1 declarations
• AddedZero.lean 37 declarations
• AddedZeroUniform.lean 24 declarations
• AllocatedCenteredCapped.lean 4 declarations
• AllocatedChildCapacity.lean 26 declarations
• AllocatedDetectorAmplitude.lean 6 declarations
• AllocatedDetectorCapped.lean 1 declarations
• AllocatedNaturalRadial.lean 18 declarations
• AllocatedNaturalSource.lean 29 declarations
• AllocatedRayDictionary.lean 21 declarations
• AllocationCost.lean 2 declarations
• Amplification.lean 5 declarations
• AmplificationActiveFactor.lean 6 declarations
• AmplificationActiveFamily.lean 2 declarations
• AmplificationAllocation.lean 7 declarations
• AmplificationAllocationCost.lean 6 declarations
• AmplificationAllocationScale.lean 6 declarations
• AmplificationChildEnergy.lean 1 declarations
• AmplificationChildInput.lean 26 declarations
• AmplificationChildSourceCaps.lean 35 declarations
• AmplificationCount.lean 5 declarations
• AmplificationEligibility.lean 8 declarations
• AmplificationEnergy.lean 7 declarations
• AmplificationErrorEnergy.lean 4 declarations
• AmplificationErrorPool.lean 2 declarations
• AmplificationFamily.lean 7 declarations
• AmplificationFamilyEnergy.lean 2 declarations
• AmplificationGlobal.lean 11 declarations
• AmplificationLiveEnergy.lean 2 declarations
• AmplificationLiveMask.lean 4 declarations
• AmplificationLocal.lean 9 declarations
• AmplificationMask.lean 2 declarations
• AmplificationOriginalErrors.lean 1 declarations
• AmplificationRadicalChoice.lean 4 declarations
• AmplificationRadicalFamily.lean 8 declarations
• AmplificationRectangle.lean 3 declarations
• AmplificationShortening.lean 16 declarations
• AmplificationSlotGap.lean 5 declarations
• AmplificationSource.lean 3 declarations
• AmplificationSourceDomain.lean 10 declarations
• AmplificationSourceError.lean 3 declarations
• AmplificationSourcePolynomial.lean 3 declarations
• AmplificationSourcePool.lean 2 declarations
• AmplifiedChildWidth.lean 28 declarations
• AmplifiedRetainedRadius.lean 24 declarations
• Basic.lean 25 declarations
• BottomStage.lean 4 declarations
• Bridge.lean 8 declarations
• CRT.lean 6 declarations
• Cancellation.lean 6 declarations
• Canonical.lean 11 declarations
• CanonicalFirst.lean 31 declarations
• CanonicalRetainedSource.lean 10 declarations
• Cauchy.lean 6 declarations
• ChildAssembly.lean 6 declarations
• ChildEnergy.lean 3 declarations
• ChildRows.lean 10 declarations
• CommonAllocation.lean 6 declarations
• CommonAllocationBox.lean 5 declarations
• CommonAllocationSum.lean 8 declarations
• CommonAllowance.lean 6 declarations
• CommonExceptionalCanonical.lean 1 declarations
• CommonExceptionalCanonicalWindow.lean 1 declarations
• CommonExceptionalCost.lean 5 declarations
• CommonExceptionalGates.lean 6 declarations
• CommonExceptionalMass.lean 3 declarations
• CommonExceptionalSource.lean 1 declarations
• CommonExceptionalSymmetry.lean 2 declarations
• CommonExceptionalWindow.lean 1 declarations
• CommonHarmonicMass.lean 17 declarations
• CommonHeightEnvelope.lean 3 declarations
• CommonLinearNormalization.lean 5 declarations
• CommonLinearSource.lean 4 declarations
• CommonLiveFrozen.lean 3 declarations
• CommonLiveHeight.lean 1 declarations
• CommonMaskChildCapacity.lean 5 declarations
• CommonMaskEnergy.lean 17 declarations
• CommonMaskExpansion.lean 31 declarations
• CommonMaskRadialEnergy.lean 3 declarations
• CommonPairedSource.lean 4 declarations
• CommonPrimeSlots.lean 6 declarations
• CommonProfile.lean 8 declarations
• CommonPuncture.lean 4 declarations
• CommonRadialCost.lean 3 declarations
• CommonRadialData.lean 8 declarations
• CommonRadialPointwise.lean 3 declarations
• CommonRadialSource.lean 5 declarations
• CommonRadicalHarmonicMass.lean 12 declarations
• CommonRadiusSaving.lean 20 declarations
• CommonRawCost.lean 1 declarations
• CommonRawScale.lean 13 declarations
• CommonSectorColumn.lean 1 declarations
• CommonSectorWindow.lean 3 declarations
• CommonSectors.lean 6 declarations
• CommonSupport.lean 17 declarations
• CommonWindowColumn.lean 6 declarations
• ComparisonReflection.lean 9 declarations
• CompleteCommon.lean 45 declarations
• ConjugateWindow.lean 4 declarations
• CoreFloor.lean 7 declarations
• Correlation.lean 24 declarations
• Counting.lean 4 declarations
• DescentLedger.lean 10 declarations
• DetectorDictionary.lean 5 declarations
• DetectorDictionaryFiber.lean 3 declarations
• DetectorDictionaryProfiles.lean 4 declarations
• DetectorDictionaryRelativeSlots.lean 4 declarations
• DetectorDictionaryRows.lean 2 declarations
• DetectorDictionarySlots.lean 4 declarations
• DetectorDictionarySource.lean 4 declarations
• DetectorDictionarySupport.lean 3 declarations
• DetectorDictionaryUniform.lean 3 declarations
• DetectorDictionaryUniformHeight.lean 1 declarations
• DetectorDictionaryUniformLog.lean 7 declarations
• DetectorDictionaryUniformTests.lean 6 declarations
• DetectorEnergyInitialState.lean 10 declarations
• DetectorPlainCapacity.lean 3 declarations
• DetectorPlainExceptional.lean 5 declarations
• DetectorPlainFiberSource.lean 14 declarations
• DetectorPlainMarkedState.lean 9 declarations
• DetectorPlainMomentParameters.lean 14 declarations
• DetectorPlainProfileControl.lean 2 declarations
• DetectorPlainRelativeClass.lean 4 declarations
• DetectorPlainSlotProfile.lean 12 declarations
• DetectorPlainSource.lean 6 declarations
• DetectorPlainStateDictionary.lean 3 declarations
• DetectorPlainUnmarkedState.lean 7 declarations
• DivisorActualBoundary.lean 3 declarations
• DivisorAllocation.lean 10 declarations
• DivisorBoundary.lean 12 declarations
• DivisorEnergy.lean 4 declarations
• DivisorExtraction.lean 8 declarations
• DivisorFullMask.lean 5 declarations
• DivisorRaw.lean 11 declarations
• DivisorRawEnergy.lean 3 declarations
• DivisorRectangle.lean 6 declarations
• DivisorRetained.lean 3 declarations
• DivisorRowEnergy.lean 2 declarations
• DivisorRows.lean 3 declarations
• DivisorSlots.lean 4 declarations
• DivisorTensor.lean 6 declarations
• DivisorWitness.lean 7 declarations
• DyadicCount.lean 14 declarations
• EligibleEnergy.lean 13 declarations
• ExceptionalAllocationShell.lean 7 declarations
• ExceptionalAmplitudePair.lean 9 declarations
• ExceptionalAsymmetricCanonical.lean 1 declarations
• ExceptionalAsymmetricSource.lean 6 declarations
• ExceptionalCanonicalShell.lean 1 declarations
• ExceptionalCappedAmplitude.lean 8 declarations
• ExceptionalHeight.lean 6 declarations
• ExceptionalIndexedWindow.lean 1 declarations
• ExceptionalKernel.lean 3 declarations
• ExceptionalMaskedSource.lean 6 declarations
• ExceptionalPair.lean 7 declarations
• ExceptionalReflection.lean 6 declarations
• ExceptionalSourceShell.lean 3 declarations
• ExceptionalWholeSource.lean 3 declarations
• ExceptionalWholeWindow.lean 2 declarations
• ExceptionalWindowHeight.lean 2 declarations
• ExceptionalWindowPair.lean 2 declarations
• Extraction.lean 8 declarations
• FinalStageLedger.lean 4 declarations
• FiniteProfileExceptionalAllocated.lean 1 declarations
• FiniteProfileExceptionalAmplitude.lean 1 declarations
• FiniteProfileExceptionalCapped.lean 1 declarations
• FiniteProfileExceptionalCommonAsymmetric.lean 6 declarations
• FiniteProfileExceptionalCommonCanonical.lean 1 declarations
• FiniteProfileExceptionalCommonGates.lean 1 declarations
• FiniteProfileExceptionalCommonHeight.lean 3 declarations
• FiniteProfileExceptionalCommonMass.lean 2 declarations
• FiniteProfileExceptionalCommonSource.lean 1 declarations
• FiniteProfileExceptionalCommonSymmetry.lean 1 declarations
• FiniteProfileExceptionalCommonWindow.lean 1 declarations
• FiniteProfileExceptionalControl.lean 2 declarations
• FiniteProfileExceptionalFixedQBlock.lean 1 declarations
• FiniteProfileExceptionalFixedQCanonical.lean 1 declarations
• FiniteProfileExceptionalFixedQDyadic.lean 1 declarations
• FiniteProfileExceptionalFixedQPair.lean 1 declarations
• FiniteProfileExceptionalFixedQRows.lean 1 declarations
• FiniteProfileExceptionalFixedQSaved.lean 1 declarations
• FiniteProfileExceptionalFixedQUniform.lean 1 declarations
• FiniteProfileExceptionalFixedQWindow.lean 1 declarations
• FiniteProfileExceptionalNormalize.lean 9 declarations
• FiniteProfileExceptionalPair.lean 5 declarations
• FiniteProfileExceptionalPhysicalBlock.lean 3 declarations
• FiniteProfileExceptionalPhysicalBudget.lean 6 declarations
• FiniteProfileExceptionalPhysicalDyadic.lean 1 declarations
• FiniteProfileExceptionalPhysicalHeight.lean 2 declarations
• FiniteProfileExceptionalPhysicalPair.lean 1 declarations
• FiniteProfileExceptionalPhysicalRows.lean 1 declarations
• FiniteProfileExceptionalPhysicalSaved.lean 1 declarations
• FiniteProfileExceptionalPhysicalSaving.lean 1 declarations
• FiniteProfileExceptionalPhysicalUniform.lean 1 declarations
• FiniteProfileExceptionalRectangle.lean 1 declarations
• FiniteProfileExceptionalRow.lean 1 declarations
• FiniteProfileExceptionalSlots.lean 1 declarations
• FiniteProfileExceptionalStability.lean 11 declarations
• FiniteProfileExceptionalUnit.lean 1 declarations
• FiniteProfileExceptionalVolume.lean 2 declarations
• FirstActiveFourier.lean 3 declarations
• FirstActiveRadicalBudget.lean 6 declarations
• FirstAllocationGaussEnergy.lean 20 declarations
• FirstAmplificationChoice.lean 71 declarations
• FirstAmplifiedActiveAffine.lean 3 declarations
• FirstAmplifiedActiveCapacitySource.lean 3 declarations
• FirstAmplifiedCapacityCommon.lean 7 declarations
• FirstAmplifiedCapacityRadius.lean 4 declarations
• FirstAmplifiedCapacitySource.lean 4 declarations
• FirstAmplifiedFourCoefficients.lean 24 declarations
• FirstAmplifiedPaidAdmission.lean 7 declarations
• FirstAmplifiedPaidReserve.lean 5 declarations
• FirstAmplifiedPowerBudget.lean 2 declarations
• FirstAmplifiedRadiusLower.lean 5 declarations
• FirstAnnularActiveInput.lean 4 declarations
• FirstAnnularAmplification.lean 1 declarations
• FirstAnnularEnergy.lean 4 declarations
• FirstAnnularGeometry.lean 6 declarations
• FirstAnnularInput.lean 2 declarations
• FirstAnnularInputAmplification.lean 1 declarations
• FirstAnnularMajorant.lean 18 declarations
• FirstAssembly.lean 5 declarations
• FirstCanonicalAllowance.lean 9 declarations
• FirstCanonicalFamily.lean 8 declarations
• FirstChildBound.lean 4 declarations
• FirstChildLower.lean 4 declarations
• FirstChildProfile.lean 2 declarations
• FirstChildProfileControl.lean 12 declarations
• FirstColumns.lean 9 declarations
• FirstCommonFourierTransport.lean 8 declarations
• FirstCommonReferencePower.lean 4 declarations
• FirstCommonSourceBudget.lean 3 declarations
• FirstCommonSourcePowerBudget.lean 2 declarations
• FirstCommonTransport.lean 16 declarations
• FirstDiscarded.lean 2 declarations
• FirstDiscardedEnergy.lean 11 declarations
• FirstDivisorCommonBound.lean 8 declarations
• FirstDivisorSupport.lean 8 declarations
• FirstEnergy.lean 1 declarations
• FirstErrorAllocationPower.lean 6 declarations
• FirstExceptionalChildPaid.lean 6 declarations
• FirstExceptionalPaidScales.lean 9 declarations
• FirstExceptionalPrefactor.lean 5 declarations
• FirstExceptionalPrefactorActual.lean 4 declarations
• FirstExtractedLedger.lean 1 declarations
• FirstFamily.lean 3 declarations
• FirstFrequency.lean 3 declarations
• FirstIdealFamily.lean 3 declarations
• FirstInactiveRadicalMass.lean 5 declarations
• FirstLocalization.lean 12 declarations
• FirstMaskedFamily.lean 27 declarations
• FirstMaskedInput.lean 8 declarations
• FirstMixed.lean 2 declarations
• FirstMixedAllowance.lean 7 declarations
• FirstMixedChild.lean 2 declarations
• FirstMixedCommonRadius.lean 4 declarations
• FirstMixedDiagonal.lean 3 declarations
• FirstMixedExceptionalCap.lean 4 declarations
• FirstMixedExceptionalDeclared.lean 2 declarations
• FirstMixedExceptionalLow.lean 4 declarations
• FirstMixedMainError.lean 2 declarations
• FirstMixedNormalization.lean 2 declarations
• FirstMixedNormalizationActual.lean 3 declarations
• FirstMixedRightTransport.lean 12 declarations
• FirstMixedRoot.lean 6 declarations
• FirstMixedWindow.lean 1 declarations
• FirstNestedSeededGaussianPower.lean 7 declarations
• FirstNonexceptionalFixedWeightSum.lean 2 declarations
• FirstNonexceptionalLocalWeightSum.lean 2 declarations
• FirstNonexceptionalPrefactor.lean 5 declarations
• FirstNonexceptionalWeightSum.lean 6 declarations
• FirstNormalization.lean 2 declarations
• FirstPhysicalActiveDictionary.lean 18 declarations
• FirstPhysicalAnnularCommonBound.lean 1 declarations
• FirstPhysicalDyadicAssembly.lean 19 declarations
• FirstPhysicalDyadicCount.lean 4 declarations
• FirstPhysicalDyadicCountSource.lean 5 declarations
• FirstPhysicalDyadicRows.lean 9 declarations
• FirstPhysicalLedger.lean 5 declarations
• FirstPhysicalOriginalMask.lean 5 declarations
• FirstPhysicalSource.lean 13 declarations
• FirstPhysicalSourceAllocatedInput.lean 7 declarations
• FirstPhysicalSourceAllocationControl.lean 4 declarations
• FirstPhysicalSourceBound.lean 1 declarations
• FirstPhysicalSourceCanonicalData.lean 4 declarations
• FirstPhysicalSourceCommonBound.lean 1 declarations
• FirstPhysicalSourceDyadicWindowEnergy.lean 2 declarations
• FirstPhysicalSourceFixedEnergy.lean 5 declarations
• FirstPhysicalSourceFixedFamily.lean 6 declarations
• FirstPhysicalSourceFixedSource.lean 5 declarations
• FirstPhysicalSourceNormalization.lean 1 declarations
• FirstPhysicalSourceOriginalColumn.lean 4 declarations
• FirstPhysicalSourceOriginalData.lean 6 declarations
• FirstPhysicalSourcePool.lean 2 declarations
• FirstPhysicalSourcePresentation.lean 4 declarations
• FirstPhysicalSourceSupport.lean 7 declarations
• FirstPhysicalSourceWindow.lean 4 declarations
• FirstPhysicalSourceWindowCanonical.lean 3 declarations
• FirstPhysicalSourceWindowColumns.lean 4 declarations
• FirstPhysicalSourceWindowEnergy.lean 5 declarations
• FirstPhysicalZeroRadius.lean 5 declarations
• FirstPoisson.lean 6 declarations
• FirstReduced.lean 10 declarations
• FirstReferenceBlock.lean 1 declarations
• FirstReferenceEnergy.lean 7 declarations
• FirstReferenceSource.lean 6 declarations
• FirstRetainedActive.lean 2 declarations
• FirstRetainedAssembly.lean 4 declarations
• FirstRetainedBlock.lean 5 declarations
• FirstRetainedNorm.lean 5 declarations
• FirstRetainedPhysical.lean 3 declarations
• FirstRetainedSector.lean 7 declarations
• FirstScale.lean 7 declarations
• FirstSecondActiveErrorGates.lean 4 declarations
• FirstSecondCapacityDefect.lean 5 declarations
• FirstSecondCapacityLedger.lean 7 declarations
• FirstSecondCapacityShift.lean 5 declarations
• FirstSecondCommonGates.lean 2 declarations
• FirstSecondInputGates.lean 4 declarations
• FirstSecondLossParameters.lean 4 declarations
• FirstSecondPaidLedger.lean 3 declarations
• FirstSectorEnergy.lean 6 declarations
• FirstSectorLocalization.lean 6 declarations
• FirstSectorTransform.lean 8 declarations
• FirstSectors.lean 10 declarations
• FirstSeededGaussianPower.lean 4 declarations
• FirstSourceConductorCaps.lean 8 declarations
• FirstSourceReduction.lean 2 declarations
• FirstTailAggregate.lean 3 declarations
• FirstWholeAssembly.lean 1 declarations
• FirstWholeKernel.lean 2 declarations
• FirstWindowBudgets.lean 4 declarations
• FixedQForcingCount.lean 17 declarations
• FixedRay.lean 16 declarations
• FixedRayInducingTransport.lean 10 declarations
• FixedRowMask.lean 2 declarations
• Forcing.lean 16 declarations
• Fourier.lean 9 declarations
• FrequencyScaleSupremum.lean 8 declarations
• FullCorrelation.lean 12 declarations
• GaussEnergy.lean 9 declarations
• GaussNormalization.lean 5 declarations
• HeckeCancellation.lean 6 declarations
• HeckeColumnWindow.lean 12 declarations
• HeckeExceptionalEnergy.lean 2 declarations
• HeckeExpansion.lean 7 declarations
• HeckeHeight.lean 5 declarations
• HeckeSlots.lean 6 declarations
• HeckeTwist.lean 7 declarations
• HeckeVolume.lean 20 declarations
• HeckeWindowEnergy.lean 7 declarations
• Height.lean 3 declarations
• HeterogeneousCRT.lean 2 declarations
• InductionEnergy.lean 4 declarations
• Initial.lean 7 declarations
• Lattice.lean 8 declarations
• LiveCapacity.lean 3 declarations
• LiveDomain.lean 8 declarations
• LiveSupport.lean 4 declarations
• Local.lean 6 declarations
• LogDyadic.lean 8 declarations
• Mask.lean 6 declarations
• MaskedVolume.lean 1 declarations
• MobiusHarmonicMass.lean 3 declarations
• MobiusRegroup.lean 4 declarations
• NaturalCoreFloor.lean 1 declarations
• NaturalFixedRaySourceAllocatedErrorMass.lean 8 declarations
• NaturalFixedRaySourceAllocatedProfile.lean 7 declarations
• NaturalFixedRaySourceBatch.lean 2 declarations
• NaturalFixedRaySourceCapacity.lean 4 declarations
• NaturalFixedRaySourceCharacters.lean 9 declarations
• NaturalFixedRaySourceDegree.lean 4 declarations
• NaturalFixedRaySourceDetectorCancellation.lean 3 declarations
• NaturalFixedRaySourceDetectorCapped.lean 2 declarations
• NaturalFixedRaySourceDetectorProfile.lean 6 declarations
• NaturalFixedRaySourceDetectorSlots.lean 2 declarations
• NaturalFixedRaySourceFiber.lean 7 declarations
• NaturalFixedRaySourceFixedIdeal.lean 8 declarations
• NaturalFixedRaySourceFreeExceptional.lean 5 declarations
• NaturalFixedRaySourceInternal.lean 9 declarations
• NaturalFixedRaySourceNaturalPrime.lean 3 declarations
• NaturalFixedRaySourcePhysical.lean 2 declarations
• NaturalFixedRaySourcePrimeBound.lean 1 declarations
• NaturalFixedRaySourcePrimeGate.lean 4 declarations
• NaturalFixedRaySourceProduct.lean 5 declarations
• NaturalFixedRaySourceRayPrime.lean 1 declarations
• NaturalFixedRaySourceSlots.lean 3 declarations
• NaturalFixedRaySourceSupport.lean 5 declarations
• NaturalMaskedFloor.lean 3 declarations
• NaturalPrimitive.lean 17 declarations
• NaturalRadialCutoff.lean 3 declarations
• NaturalReflection.lean 5 declarations
• NaturalRetainedEnergy.lean 1 declarations
• NaturalRowSourceDictionary.lean 4 declarations
• NaturalRowSourceFamily.lean 11 declarations
• NaturalRowSourceMask.lean 6 declarations
• NonprincipalGate.lean 7 declarations
• OneReflectionEnergy.lean 3 declarations
• OneReflectionScaleEnergy.lean 4 declarations
• OriginalChildEnergy.lean 3 declarations
• OriginalCommonHarmonic.lean 6 declarations
• OriginalComparisonEnergy.lean 1 declarations
• OriginalRadialComparison.lean 4 declarations
• OriginalRadialTail.lean 6 declarations
• OriginalReflectionApproximation.lean 5 declarations
• OriginalReflectionEnergy.lean 2 declarations
• OriginalReflectionErrorMass.lean 15 declarations
• PairedEligibleEnergy.lean 2 declarations
• Partition.lean 10 declarations
• PartitionNorm.lean 7 declarations
• PlainChildEnergy.lean 3 declarations
• PlainEnergy.lean 3 declarations
• PlainGlobalActual.lean 1 declarations
• PlainGlobalBound.lean 2 declarations
• PlainGlobalEnergy.lean 4 declarations
• PlainPositiveEnergy.lean 1 declarations
• PlainPositiveScale.lean 2 declarations
• PlainWindowEnergy.lean 6 declarations
• Poisson.lean 3 declarations
• PositiveSummability.lean 6 declarations
• Primary.lean 12 declarations
• PrimaryCharacter.lean 12 declarations
• PrimeElements.lean 9 declarations
• PrimeGlobal.lean 2 declarations
• PrimeHeight.lean 4 declarations
• PrimePool.lean 6 declarations
• PrimePower.lean 9 declarations
• PrimeSlot.lean 6 declarations
• PrimeSlotBound.lean 1 declarations
• PrimeSlotExternal.lean 1 declarations
• PrimeSlotShift.lean 3 declarations
• PrimeSlotUniform.lean 1 declarations
• Primitive.lean 6 declarations
• ProductCRT.lean 14 declarations
• RadialCenteredEnergy.lean 7 declarations
• RadialEligibleEnergy.lean 12 declarations
• RadialPointwiseEnergy.lean 2 declarations
• RadialPointwiseUniform.lean 3 declarations
• RadialPolynomialEnergy.lean 3 declarations
• RadialSourceDictionary.lean 1 declarations
• RadicalFamily.lean 5 declarations
• Rankin.lean 6 declarations
• RankinCount.lean 6 declarations
• RankinLabels.lean 2 declarations
• RankinRadical.lean 6 declarations
• RankinScale.lean 1 declarations
• RankinSubset.lean 2 declarations
• RayMaskedFloor.lean 1 declarations
• RayMaskedFloorCoefficients.lean 1 declarations
• RayMaskedFloorNatural.lean 1 declarations
• RayMaskedFloorShared.lean 1 declarations
• RayMaskedFloorSlots.lean 2 declarations
• RayMaskedFloorSource.lean 1 declarations
• RayMaskedFloorState.lean 1 declarations
• RayNonprincipal.lean 4 declarations
• Rectangle.lean 5 declarations
• ReflectedAnnuli.lean 29 declarations
• ReflectedChild.lean 2 declarations
• ReflectedChoiceEnergy.lean 2 declarations
• ReflectedNormalization.lean 4 declarations
• ReflectedPairEnergy.lean 3 declarations
• ReflectedProfileMeasure.lean 8 declarations
• ReflectedSeries.lean 6 declarations
• ReflectedSource.lean 8 declarations
• ReflectedTruncation.lean 5 declarations
• ReflectedUniformPair.lean 10 declarations
• ReflectionDeletion.lean 52 declarations
• ReflectionLength.lean 3 declarations
• ReflectionMass.lean 31 declarations
• ReflectionNegligible.lean 3 declarations
• ReflectionRetainedLength.lean 4 declarations
• ReflectionTailMass.lean 5 declarations
• ReflectionTails.lean 7 declarations
• ReflectionWeightedEnergy.lean 24 declarations
• RelativeCapacityRemoval.lean 2 declarations
• RemainingBox.lean 8 declarations
• RestrictedDomain.lean 3 declarations
• RestrictedEnergy.lean 8 declarations
• RestrictedSource.lean 4 declarations
• RestrictedSourceNormalization.lean 3 declarations
• RestrictedWindow.lean 4 declarations
• RetainedComparisonEnergy.lean 1 declarations
• RetainedEnergy.lean 7 declarations
• RetainedProfile.lean 34 declarations
• RetainedReflection.lean 5 declarations
• RetainedWeightedSource.lean 9 declarations
• RowNorm.lean 10 declarations
• Scale.lean 4 declarations
• ScaleSupremum.lean 9 declarations
• SecondActiveCount.lean 5 declarations
• SecondActiveDyadic.lean 6 declarations
• SecondActivePhysicalDictionary.lean 6 declarations
• SecondActualWidth.lean 3 declarations
• SecondBlockAggregate.lean 8 declarations
• SecondBlockCount.lean 12 declarations
• SecondBlockHarmonicMass.lean 13 declarations
• SecondBlockRadicalHarmonicMass.lean 7 declarations
• SecondBlockSupport.lean 3 declarations
• SecondCanonical.lean 12 declarations
• SecondCanonicalFrequency.lean 7 declarations
• SecondCanonicalLedger.lean 6 declarations
• SecondCanonicalNonunit.lean 8 declarations
• SecondCanonicalScalar.lean 5 declarations
• SecondCapacitySourceShift.lean 8 declarations
• SecondChildPowerBudget.lean 11 declarations
• SecondChildProfile.lean 3 declarations
• SecondChildRadialWidth.lean 10 declarations
• SecondDescent.lean 4 declarations
• SecondDiagonal.lean 11 declarations
• SecondDivisorSupport.lean 4 declarations
• SecondDyadicPartition.lean 3 declarations
• SecondDyadicRowSupport.lean 9 declarations
• SecondEnergySplit.lean 8 declarations
• SecondExceptionalAggregate.lean 3 declarations
• SecondExceptionalBudget.lean 6 declarations
• SecondExceptionalCanonicalPair.lean 1 declarations
• SecondExceptionalCommonSaving.lean 1 declarations
• SecondExceptionalCount.lean 5 declarations
• SecondExceptionalEnergy.lean 1 declarations
• SecondExceptionalFamily.lean 22 declarations
• SecondExceptionalFamilyUniform.lean 7 declarations
• SecondExceptionalFixedQChosenBlock.lean 1 declarations
• SecondExceptionalFixedQSource.lean 1 declarations
• SecondExceptionalKernel.lean 5 declarations
• SecondExceptionalOriginalBlock.lean 3 declarations
• SecondExceptionalPairBound.lean 3 declarations
• SecondExceptionalPairDictionary.lean 2 declarations
• SecondExceptionalPhysicalSaving.lean 5 declarations
• SecondExceptionalSourceCaps.lean 1 declarations
• SecondExceptionalSourceFamily.lean 4 declarations
• SecondExceptionalUniformSource.lean 1 declarations
• SecondFamilyTransport.lean 5 declarations
• SecondFrozenChosen.lean 2 declarations
• SecondFrozenLiveDescent.lean 1 declarations
• SecondFrozenLiveSource.lean 1 declarations
• SecondFrozenPhysical.lean 1 declarations
• SecondFrozenPowerDescent.lean 1 declarations
• SecondFrozenRatioCost.lean 1 declarations
• SecondFrozenReferenceSeededPowerDescent.lean 1 declarations
• SecondFrozenSeededPowerDescent.lean 1 declarations
• SecondFrozenSupported.lean 1 declarations
• SecondFrozenUniformSubset.lean 1 declarations
• SecondHarmonicBudget.lean 2 declarations
• SecondHeightFamily.lean 6 declarations
• SecondIdealBlockBound.lean 2 declarations
• SecondInputCapacitySource.lean 8 declarations
• SecondLedger.lean 12 declarations
• SecondLiveBlock.lean 9 declarations
• SecondLiveEnergy.lean 2 declarations
• SecondLiveFamily.lean 1 declarations
• SecondLiveSourceDescent.lean 1 declarations
• SecondLocalization.lean 4 declarations
• SecondMaskedWindow.lean 3 declarations
• SecondMovingSupport.lean 5 declarations
• SecondNonexceptional.lean 1 declarations
• SecondNonexceptionalAggregate.lean 3 declarations
• SecondNonexceptionalChosenBlock.lean 3 declarations
• SecondNonexceptionalCost.lean 1 declarations
• SecondNonexceptionalLiveSource.lean 1 declarations
• SecondNonexceptionalPhysical.lean 3 declarations
• SecondNonexceptionalScalar.lean 8 declarations
• SecondOriginalChildren.lean 4 declarations
• SecondPhysicalBlock.lean 5 declarations
• SecondPhysicalCost.lean 3 declarations
• SecondPhysicalLedger.lean 13 declarations
• SecondPhysicalWindow.lean 2 declarations
• SecondRadicalBlock.lean 1 declarations
• SecondRadicalBudget.lean 9 declarations
• SecondRadicalColumns.lean 3 declarations
• SecondRadicalFamily.lean 2 declarations
• SecondReducedEnergy.lean 2 declarations
• SecondReducedPredicate.lean 3 declarations
• SecondReferenceNormalization.lean 5 declarations
• SecondRetainedAggregate.lean 2 declarations
• SecondRetainedPair.lean 2 declarations
• SecondRetainedRatioCost.lean 1 declarations
• SecondRetainedRatioScalar.lean 5 declarations
• SecondRetainedRows.lean 5 declarations
• SecondRetainedWidth.lean 6 declarations
• SecondScaled.lean 6 declarations
• SecondSectorChildren.lean 1 declarations
• SecondSectorColumns.lean 9 declarations
• SecondSectorEnergy.lean 4 declarations
• SecondSectorFrequency.lean 6 declarations
• SecondSectorRetained.lean 3 declarations
• SecondSixthReduction.lean 8 declarations
• SecondSixthSource.lean 9 declarations
• SecondSourceCost.lean 1 declarations
• SecondSourceDiagonal.lean 1 declarations
• SecondSourceEnergy.lean 4 declarations
• SecondSourceFrequency.lean 2 declarations
• SecondSourceMask.lean 3 declarations
• SecondSourcePoisson.lean 2 declarations
• SecondSourcePowerDescent.lean 3 declarations
• SecondSourceRemainder.lean 1 declarations
• SecondSourceRetained.lean 5 declarations
• SecondSourceSeededPowerDescent.lean 2 declarations
• SecondSquarefreeBlock.lean 1 declarations
• SecondSummedBlock.lean 1 declarations
• SecondSupportedChildren.lean 4 declarations
• SecondTail.lean 3 declarations
• SecondUniformSubsetSource.lean 8 declarations
• SecondWholeKernel.lean 6 declarations
• SecondWidthDrop.lean 5 declarations
• SecondWindowBudget.lean 9 declarations
• SecondWindowSource.lean 4 declarations
• SectorLocalization.lean 80 declarations
• SlotClassTransport.lean 4 declarations
• SlotNormalization.lean 2 declarations
• SlotRatios.lean 5 declarations
• SlotRemoval.lean 3 declarations
• Smooth.lean 13 declarations
• SmoothedRetainedSource.lean 1 declarations
• SmoothedWindowEnergy.lean 4 declarations
• SourceAbsoluteEnvelope.lean 1 declarations
• SourceAllocationEnergy.lean 3 declarations
• SourceBlockWindows.lean 2 declarations
• SourceCommonMask.lean 3 declarations
• SourceDyadicShell.lean 2 declarations
• SourceInputFirstRemainder.lean 1 declarations
• SourceInputFirstSectorTailAggregate.lean 2 declarations
• SourceInputFirstSectorTailNatural.lean 1 declarations
• SourceInputFirstSectorTailPair.lean 2 declarations
• SourceInputFirstSectorTailUniform.lean 1 declarations
• SourceInputFirstTailScale.lean 2 declarations
• SourceInputFirstTailUniform.lean 2 declarations
• SourceInputReindex.lean 19 declarations
• SourceInputTailSeed.lean 3 declarations
• SourceInputTailUniform.lean 9 declarations
• SourceInputZeroUniform.lean 3 declarations
• SourceLiveAllocation.lean 4 declarations
• SourceLiveColumn.lean 5 declarations
• SourceLowerSupport.lean 3 declarations
• SourceMass.lean 50 declarations
• SourceProfileMass.lean 5 declarations
• SourceProfileMassUniform.lean 2 declarations
• SourceRectangle.lean 27 declarations
• SourceRectangleEnergy.lean 2 declarations
• SourceRectangleMask.lean 4 declarations
• SourceRetainedEnergy.lean 1 declarations
• SourceRow.lean 10 declarations
• SourceSecondZeroEnergy.lean 14 declarations
• SourceSmoothedAllocation.lean 2 declarations
• SourceSupportedTailUniform.lean 2 declarations
• SourceZeroEnergy.lean 6 declarations
• SuccessorPaidParameters.lean 10 declarations
• Support.lean 24 declarations
• SupportedCorrelation.lean 14 declarations
• SupportedTailAggregate.lean 4 declarations
• SupportedZeroEnergy.lean 11 declarations
• Tail.lean 10 declarations
• TerminalEnergy.lean 1 declarations
• Twist.lean 9 declarations
• TwistedReflection.lean 2 declarations
• UncenteredTerminal.lean 8 declarations
• Unequal.lean 14 declarations
• UniformDivisorShell.lean 6 declarations
• UniformEligibleEnergy.lean 3 declarations
• UniformNaturalRetained.lean 1 declarations
• UniformOriginalComparison.lean 1 declarations
• UniformOriginalEnergy.lean 1 declarations
• UniformRadialComparison.lean 1 declarations
• UniformReflectionApproximation.lean 12 declarations
• UniformReflectionChoices.lean 1 declarations
• UniformReflectionProfile.lean 9 declarations
• UniformReflectionScale.lean 1 declarations
• UniformRetainedEnergy.lean 4 declarations
• WholeDivisorShell.lean 28 declarations
• WholeSlotDeletion.lean 5 declarations
• ZeroMeanBridge.lean 23 declarations
• ZeroMode.lean 27 declarations