`OAI/Analysis/LipschitzHilbert/Packets/`

1141 declarations, 0 contain sorry, 0 declared as axioms; 346 files

Files

AnalyzedGlobalNeighborhood.lean 1 declarations
AnalyzedLineFamily.lean 4 declarations
AnalyzedLineMoments.lean 1 declarations
AnalyzedNeighborhood.lean 1 declarations
AnalyzedReplacement.lean 2 declarations
AnalyzingBilinear.lean 1 declarations
AnalyzingCoefficientNorm.lean 1 declarations
AnalyzingCoefficients.lean 5 declarations
AnalyzingProfileNormalization.lean 6 declarations
AnnularEnlargedFrame.lean 4 declarations
AnnularLowerFrame.lean 8 declarations
AnnularPacketGeometry.lean 9 declarations
BoxPacketVariation.lean 1 declarations
ConvolutionPacketProfile.lean 3 declarations
ConvolutionPacketSchwartz.lean 6 declarations
ConvolutionPacketSpectrum.lean 4 declarations
FactoredMultiplierPackets.lean 7 declarations
FiniteNormalizedPacketLattice.lean 6 declarations
FinitePacketSites.lean 9 declarations
HilbertPacketLinearity.lean 2 declarations
HilbertPacketSums.lean 3 declarations
JointPacketAverage.lean 1 declarations
JointVectorPacketAverage.lean 1 declarations
LineConvolutionFrame.lean 3 declarations
LinePacketFamily.lean 14 declarations
LinePacketReplacement.lean 2 declarations
NormalizedPacketKernelForm.lean 1 declarations
NormalizedPacketLattice.lean 5 declarations
NormalizedPacketProfiles.lean 7 declarations
NormalizedPacketSpectrum.lean 5 declarations
PacketBinAnnulus.lean 3 declarations
PacketBoxes.lean 8 declarations
PacketConvolution.lean 12 declarations
PacketDataActualPacketRecovery.lean 1 declarations
PacketDataActualReferenceArea.lean 1 declarations
PacketDataActualReferenceCentral.lean 1 declarations
PacketDataActualReferenceEvents.lean 7 declarations
PacketDataAdjoint.lean 7 declarations
PacketDataAdjointEnergy.lean 1 declarations
PacketDataAdjointPairingBound.lean 1 declarations
PacketDataAdjointPolarization.lean 2 declarations
PacketDataAssignedBoundaryError.lean 1 declarations
PacketDataAssignedBoundaryGain.lean 1 declarations
PacketDataAssignedBoundaryPrefix.lean 5 declarations
PacketDataAssignedLabelCount.lean 1 declarations
PacketDataAssignedLabelCountAt.lean 1 declarations
PacketDataAssignedLinearEnvelope.lean 1 declarations
PacketDataAssignedMarkedPath.lean 1 declarations
PacketDataAssignedMaskRemoval.lean 1 declarations
PacketDataAssignedMaskSums.lean 3 declarations
PacketDataAssignedModelInterval.lean 1 declarations
PacketDataAssignedParentCentralGain.lean 1 declarations
PacketDataAssignedParentCentralInputs.lean 1 declarations
PacketDataAssignedParentMarkedBound.lean 2 declarations
PacketDataAssignedParentPhysicalPlane.lean 1 declarations
PacketDataAssignedParentVertexIntegral.lean 1 declarations
PacketDataAssignedPathIntegral.lean 8 declarations
PacketDataAssignedPhysical.lean 6 declarations
PacketDataAssignedPlaneIntegral.lean 1 declarations
PacketDataAssignedReference.lean 5 declarations
PacketDataAssignedSelectorCentralGoodSet.lean 1 declarations
PacketDataAssignedSelectorControlledGoodSet.lean 1 declarations
PacketDataAssignedSelectorGoodSet.lean 1 declarations
PacketDataAssignedSelectorJointGoodSet.lean 1 declarations
PacketDataAssignedStoppedBound.lean 3 declarations
PacketDataAssignedSupportedGeometry.lean 1 declarations
PacketDataAssignedSupportedPath.lean 1 declarations
PacketDataAssignedTopAlternate.lean 3 declarations
PacketDataAssignedTopBands.lean 4 declarations
PacketDataAssignedTopEnvelope.lean 3 declarations
PacketDataAssignedTopFamily.lean 9 declarations
PacketDataAssignedTopReference.lean 1 declarations
PacketDataAssignedTopSelector.lean 22 declarations
PacketDataAssignedTubeEnvelope.lean 1 declarations
PacketDataAssignedVertexPath.lean 2 declarations
PacketDataBasicPairing.lean 1 declarations
PacketDataCappedRemovalStep.lean 1 declarations
PacketDataCoefficient.lean 3 declarations
PacketDataConeSingleScale.lean 1 declarations
PacketDataCrossForm.lean 1 declarations
PacketDataCrossPairingBound.lean 1 declarations
PacketDataCrossProductForm.lean 1 declarations
PacketDataCrossValue.lean 3 declarations
PacketDataDeletionForest.lean 10 declarations
PacketDataDeletionTreeEstimate.lean 1 declarations
PacketDataDensity.lean 6 declarations
PacketDataDensityCentralGoodSet.lean 1 declarations
PacketDataDensityForest.lean 4 declarations
PacketDataDensityForestIntegral.lean 1 declarations
PacketDataDensityGeometry.lean 1 declarations
PacketDataDensityGoodRecovery.lean 1 declarations
PacketDataDensityJetNormalization.lean 5 declarations
PacketDataDensityPopularRecovery.lean 1 declarations
PacketDataDensityRemovalIntegral.lean 1 declarations
PacketDataDensitySelectorGoodSet.lean 2 declarations
PacketDataDropDensity.lean 5 declarations
PacketDataDropPackets.lean 4 declarations
PacketDataDropSize.lean 4 declarations
PacketDataDropTreeTransport.lean 3 declarations
PacketDataEnclosingScale.lean 1 declarations
PacketDataFiniteSizeBound.lean 2 declarations
PacketDataHighDensityEnergyRecovery.lean 1 declarations
PacketDataHighDensityPopularRecovery.lean 1 declarations
PacketDataInteractionGeometry.lean 5 declarations
PacketDataIntrinsicCrossEnergy.lean 1 declarations
PacketDataIntrinsicDensityPairing.lean 1 declarations
PacketDataIntrinsicReverse.lean 1 declarations
PacketDataJetBudget.lean 4 declarations
PacketDataJetControl.lean 3 declarations
PacketDataKernelForm.lean 1 declarations
PacketDataLabelScaleEnergy.lean 2 declarations
PacketDataLatticeSites.lean 1 declarations
PacketDataMaskedBand.lean 2 declarations
PacketDataMaskedValue.lean 3 declarations
PacketDataModelBilinearRecovery.lean 1 declarations
PacketDataModelBound.lean 3 declarations
PacketDataModelConfig.lean 6 declarations
PacketDataModelCostPolynomial.lean 11 declarations
PacketDataModelDegenerateCases.lean 2 declarations
PacketDataModelEstimate.lean 2 declarations
PacketDataModelRestriction.lean 1 declarations
PacketDataNormalizedRemovalStep.lean 1 declarations
PacketDataOrdinaryDensityForest.lean 3 declarations
PacketDataOrdinaryRemovalStep.lean 1 declarations
PacketDataOriginalIntegrability.lean 2 declarations
PacketDataOriginalParentMarkedPath.lean 2 declarations
PacketDataPackedPairing.lean 1 declarations
PacketDataPacketGram.lean 3 declarations
PacketDataPacketRecovery.lean 1 declarations
PacketDataPacketScaleCount.lean 3 declarations
PacketDataParentFullResidual.lean 1 declarations
PacketDataParentReference.lean 6 declarations
PacketDataParentResidualReference.lean 1 declarations
PacketDataParentResidualSquare.lean 1 declarations
PacketDataParentStoppedBound.lean 2 declarations
PacketDataPartial.lean 5 declarations
PacketDataPathRegularity.lean 2 declarations
PacketDataPhysicalPropagatedTail.lean 1 declarations
PacketDataPhysicalResidualNorm.lean 3 declarations
PacketDataPhysicalUnaryEndpoint.lean 1 declarations
PacketDataPolarization.lean 4 declarations
PacketDataRecenteredBoundedSize.lean 1 declarations
PacketDataRecenteredReferenceConditions.lean 1 declarations
PacketDataRecenteredSelector.lean 8 declarations
PacketDataRecordedEnergy.lean 4 declarations
PacketDataReferenceBand.lean 1 declarations
PacketDataReferenceConditions.lean 4 declarations
PacketDataReferenceCross.lean 4 declarations
PacketDataReferenceEnvelope.lean 1 declarations
PacketDataReferenceMasked.lean 4 declarations
PacketDataReferenceProperties.lean 7 declarations
PacketDataReferenceSelectedVariation.lean 2 declarations
PacketDataReverseCost.lean 5 declarations
PacketDataRootedTree.lean 1 declarations
PacketDataScaleGeometry.lean 4 declarations
PacketDataScaleRestriction.lean 5 declarations
PacketDataScaleRestrictionSums.lean 4 declarations
PacketDataSelectedArea.lean 1 declarations
PacketDataSelectedBoxSeparation.lean 3 declarations
PacketDataSelectedCoefficientBound.lean 1 declarations
PacketDataSelectedConstants.lean 2 declarations
PacketDataSelectedDuality.lean 2 declarations
PacketDataSelectedGeometry.lean 5 declarations
PacketDataSelectedGram.lean 4 declarations
PacketDataSelectedPackets.lean 2 declarations
PacketDataSelectedPartial.lean 3 declarations
PacketDataSelectedPrefix.lean 7 declarations
PacketDataSelectedQuadratic.lean 2 declarations
PacketDataSelectedRecordSums.lean 2 declarations
PacketDataSelectedReference.lean 14 declarations
PacketDataSelectedScale.lean 4 declarations
PacketDataSelectedSum.lean 8 declarations
PacketDataSelectedTree.lean 1 declarations
PacketDataSignedBoxSeparation.lean 4 declarations
PacketDataSignedSelectedArea.lean 1 declarations
PacketDataSignedSelectedSynthesis.lean 1 declarations
PacketDataSignedSizeTest.lean 9 declarations
PacketDataSignedTopGeometry.lean 1 declarations
PacketDataSizeOnePacket.lean 3 declarations
PacketDataSizeRemovalIntegral.lean 1 declarations
PacketDataSizeStopping.lean 7 declarations
PacketDataSizeTest.lean 2 declarations
PacketDataSpatialTree.lean 1 declarations
PacketDataStoppingPrefix.lean 1 declarations
PacketDataSupportedAssignedConcentration.lean 1 declarations
PacketDataTopEstimate.lean 1 declarations
PacketDataTopReferenceGeometry.lean 2 declarations
PacketDataTreeSize.lean 4 declarations
PacketDataTrimInteractions.lean 1 declarations
PacketDataTwoSidedRemovedIntegral.lean 1 declarations
PacketDataTwoSidedSizeArea.lean 1 declarations
PacketDataUniformBoundedSize.lean 1 declarations
PacketDataUniformCappedStep.lean 3 declarations
PacketDataUniformCrossEnergy.lean 1 declarations
PacketDataUniformCrossReverse.lean 1 declarations
PacketDataUniformReverseDisparity.lean 1 declarations
PacketDataUniformReverseModel.lean 4 declarations
PacketDataUniversalAdjointEnergy.lean 1 declarations
PacketDataUniversalBound.lean 1 declarations
PacketDataUniversalEstimate.lean 4 declarations
PacketDataUniversalNormalizedStep.lean 1 declarations
PacketDataVectorEnvelope.lean 3 declarations
PacketDataWeightedMaximal.lean 1 declarations
PacketDataZeroDensity.lean 2 declarations
PacketFrequencyInputL1.lean 5 declarations
PacketIntervalNeighborhood.lean 1 declarations
PacketLatticeAverage.lean 2 declarations
PacketLatticeData.lean 14 declarations
PacketLatticeRestriction.lean 12 declarations
PacketLineConcentration.lean 5 declarations
PacketPolarization.lean 2 declarations
PacketReferenceSpectrum.lean 5 declarations
PacketVectorDerivative.lean 7 declarations
ParityPackets.lean 5 declarations
PhysicalPacketSpectrum.lean 3 declarations
PhysicalPlanarPacket.lean 5 declarations
PhysicalTopDerivative.lean 3 declarations
PlanarFrequencyPackets.lean 10 declarations
PlanarPacketContinuity.lean 7 declarations
PlanarPacketDerivative.lean 4 declarations
PlanarPacketDifferentiation.lean 10 declarations
PlanarPacketEnvelope.lean 3 declarations
PlanarPacketFamily.lean 11 declarations
PlanarPacketLocality.lean 3 declarations
PlanarPacketScaling.lean 2 declarations
PolynomialPacket.lean 6 declarations
PositivePacketDerivative.lean 6 declarations
PositivePacketSquare.lean 9 declarations
ReferencePacketFamily.lean 6 declarations
ScaledPlanarPacket.lean 9 declarations
SchwartzPacketDecay.lean 5 declarations
SeparatedPacketForm.lean 3 declarations
ShortPacketBoxes.lean 8 declarations
SourceAssignedPacketSum.lean 4 declarations
SourceBoundaryPacketError.lean 5 declarations
SourceBoundaryPacketRegroup.lean 3 declarations
SourceDensityPacketGeometry.lean 2 declarations
SourceDropPackets.lean 4 declarations
SourceFrozenCellIntegral.lean 7 declarations
SourceFrozenCenteredCoefficient.lean 4 declarations
SourceFrozenCoefficientEnergy.lean 5 declarations
SourceFrozenDensitySum.lean 1 declarations
SourceFrozenLongInterval.lean 6 declarations
SourceFrozenProfile.lean 10 declarations
SourceFrozenSpectrum.lean 2 declarations
SourceFrozenTreeEstimate.lean 1 declarations
SourceFrozenTreeGlobal.lean 2 declarations
SourceFrozenWhitneyLocal.lean 6 declarations
SourceLabeledPacketRestriction.lean 14 declarations
SourceLatticePacket.lean 26 declarations
SourcePackedPacketPairing.lean 1 declarations
SourcePacketDensity.lean 4 declarations
SourcePacketGram.lean 3 declarations
SourcePacketLongCell.lean 1 declarations
SourcePacketMotionBudget.lean 2 declarations
SourcePacketOwnDensity.lean 3 declarations
SourcePacketPathProduct.lean 1 declarations
SourcePacketRegroup.lean 4 declarations
SourcePacketScaleCount.lean 3 declarations
SourcePacketShear.lean 5 declarations
SourcePacketShortSum.lean 7 declarations
SourcePacketSpectrum.lean 8 declarations
SourcePacketStoppedBound.lean 1 declarations
SourcePhysicalPacketAssembly.lean 1 declarations
SourceReferencePacketEnvelope.lean 1 declarations
SourceRestrictedPacketAmplitude.lean 3 declarations
SourceSelectedPackets.lean 2 declarations
SourceSelectorCoefficientNorm.lean 1 declarations
SourceSelectorConcentration.lean 1 declarations
SourceSelectorConcentrationActive.lean 5 declarations
SourceSelectorConcentrationCentered.lean 14 declarations
SourceSelectorConcentrationCenteredFamily.lean 5 declarations
SourceSelectorConcentrationErrorBudget.lean 4 declarations
SourceSelectorConcentrationErrorFamily.lean 1 declarations
SourceSelectorConcentrationErrorMoments.lean 4 declarations
SourceSelectorConcentrationErrorNeighborhood.lean 1 declarations
SourceSelectorConcentrationErrorPhysical.lean 1 declarations
SourceSelectorConcentrationErrorRaw.lean 4 declarations
SourceSelectorConcentrationErrorSynthesis.lean 2 declarations
SourceSelectorConcentrationFamily.lean 1 declarations
SourceSelectorConcentrationJets.lean 12 declarations
SourceSelectorConcentrationJoint.lean 2 declarations
SourceSelectorConcentrationMain.lean 1 declarations
SourceSelectorConcentrationMainSlots.lean 2 declarations
SourceSelectorConcentrationNeighborhood.lean 1 declarations
SourceSelectorConcentrationSpectral.lean 1 declarations
SourceSelectorConcentrationSplit.lean 9 declarations
SourceSelectorConcentrationWeighted.lean 1 declarations
SourceSelectorDerivative.lean 4 declarations
SourceSelectorEnvelope.lean 1 declarations
SourceSelectorInsignificant.lean 1 declarations
SourceSelectorMarkedIntegral.lean 1 declarations
SourceSelectorMotion.lean 3 declarations
SourceSelectorNodeEnvelope.lean 1 declarations
SourceSelectorOffchild.lean 1 declarations
SourceSelectorPhysicalMotion.lean 3 declarations
SourceSelectorPlaneIntegral.lean 2 declarations
SourceSizeOnePacket.lean 3 declarations
SourceSupportedAnalyzedGlobal.lean 1 declarations
SourceSupportedAnalyzedNeighborhood.lean 1 declarations
SourceSupportedBandStops.lean 2 declarations
SourceSupportedConcentration.lean 1 declarations
SourceSupportedConcentrationCentered.lean 3 declarations
SourceSupportedConcentrationFamily.lean 1 declarations
SourceSupportedConcentrationMain.lean 1 declarations
SourceSupportedConcentrationMainSlots.lean 1 declarations
SourceSupportedConcentrationNeighborhood.lean 1 declarations
SourceSupportedConcentrationSpectral.lean 1 declarations
SourceSupportedConcentrationWeighted.lean 1 declarations
SourceSupportedCovariantRescale.lean 1 declarations
SourceSupportedErrorFamily.lean 1 declarations
SourceSupportedErrorPhysical.lean 1 declarations
SourceSupportedErrorRaw.lean 2 declarations
SourceSupportedErrorSynthesis.lean 1 declarations
SourceSupportedGrid.lean 4 declarations
SourceSupportedInhabitedGeometry.lean 1 declarations
SourceSupportedLabeledGeometry.lean 3 declarations
SourceSupportedLatticeData.lean 2 declarations
SourceSupportedLineNeighborhood.lean 1 declarations
SourceSupportedLinearEnvelope.lean 1 declarations
SourceSupportedMoments.lean 8 declarations
SourceSupportedPacketData.lean 4 declarations
SourceSupportedPacketNeighborhood.lean 1 declarations
SourceSupportedPolynomialMoments.lean 1 declarations
SourceSupportedRawRescale.lean 1 declarations
SourceSupportedSelectorDerivative.lean 3 declarations
SourceSupportedSelectorInsignificant.lean 1 declarations
SourceSupportedSelectorIntervalMotion.lean 3 declarations
SourceSupportedSelectorMarkedIntegral.lean 1 declarations
SourceSupportedSelectorMotion.lean 3 declarations
SourceSupportedSelectorPlaneIntegral.lean 1 declarations
SourceSupportedSynthesisNeighborhood.lean 1 declarations
SourceSupportedTreeMaximal.lean 3 declarations
SourceSupportedWeightedDerivative.lean 2 declarations
SourceSupportedWeightedMaximal.lean 1 declarations
SourceTreePacketPath.lean 5 declarations
TopCovariantPacket.lean 8 declarations
TopPacketWindow.lean 8 declarations
TopRawPacketData.lean 3 declarations
TopWeightedPacket.lean 9 declarations
UniformAnalyzedLine.lean 2 declarations
UnitPacketSelector.lean 7 declarations
VariationPacketL1.lean 5 declarations
VerticalFrameBound.lean 2 declarations
VerticalFrameSynthesis.lean 1 declarations
WeightedPacketEnergy.lean 2 declarations