`OAI/Analysis/LipschitzHilbert/Trees/`

2387 declarations, 0 contain sorry, 0 declared as axioms; 553 files

Files

AmplitudeMassTails.lean 2 declarations
BadStripMass.lean 1 declarations
BoundaryDepthCrossing.lean 3 declarations
BoundaryDistanceAverage.lean 2 declarations
BoundaryErrorFubini.lean 1 declarations
BoundaryTelescoping.lean 2 declarations
ComplementaryMass.lean 3 declarations
DyadicLineGrid.lean 14 declarations
EventMass.lean 7 declarations
FiniteGoodPath.lean 1 declarations
FiniteLineGrid.lean 11 declarations
FixedPathAverage.lean 5 declarations
FourGridBandErrors.lean 12 declarations
GeometricBoundaryDepth.lean 9 declarations
GraphPathBaseline.lean 11 declarations
HierarchyNormalization.lean 4 declarations
HierarchyVariation.lean 4 declarations
HierarchyWeights.lean 6 declarations
LineGridBMO.lean 13 declarations
LineGridBMO_Tail.lean 1 declarations
LineGridConditionalBMO.lean 2 declarations
LineGridLimit.lean 6 declarations
LineGridMartingale.lean 13 declarations
LineGridPoincare.lean 5 declarations
LineGridPrimitive.lean 3 declarations
LineSamplingL2Path.lean 7 declarations
LineSamplingPath.lean 12 declarations
PathCoefficient.lean 8 declarations
PathDrops.lean 5 declarations
PathExpansion.lean 5 declarations
ResidualBlocks.lean 4 declarations
ResidualBudget.lean 3 declarations
ResidualOscillation.lean 3 declarations
SegmentMassSum.lean 3 declarations
SlopePartitionGrid.lean 8 declarations
SourceAdjointPairingBound.lean 2 declarations
SourceAllDyadicMaximal.lean 6 declarations
SourceAllStrongMaximal.lean 12 declarations
SourceAmplitudeAssembly.lean 2 declarations
SourceAmplitudeBounds.lean 2 declarations
SourceAmplitudeEntire.lean 2 declarations
SourceAmplitudeExhaustion.lean 8 declarations
SourceAmplitudeExponential.lean 3 declarations
SourceAmplitudeIntegral.lean 3 declarations
SourceAmplitudeMeasurable.lean 8 declarations
SourceAmplitudeMotion.lean 2 declarations
SourceAssignedBoundaryPrefix.lean 5 declarations
SourceAssignedLabelCount.lean 1 declarations
SourceAssignedLabelCountAt.lean 1 declarations
SourceAssignedLinearEnvelope.lean 1 declarations
SourceAssignedMarkedBound.lean 2 declarations
SourceAssignedMarkedPath.lean 1 declarations
SourceAssignedMaskSums.lean 7 declarations
SourceAssignedModelInterval.lean 1 declarations
SourceAssignedParentCentralGain.lean 1 declarations
SourceAssignedParentCentralInputs.lean 1 declarations
SourceAssignedParentMarkedBound.lean 2 declarations
SourceAssignedParentPhysicalPlane.lean 1 declarations
SourceAssignedParentVertexIntegral.lean 1 declarations
SourceAssignedPathIntegral.lean 11 declarations
SourceAssignedPlaneIntegral.lean 1 declarations
SourceAssignedPlanePath.lean 2 declarations
SourceAssignedStoppedBound.lean 9 declarations
SourceAssignedStoppedInputs.lean 1 declarations
SourceAssignedSupportedGeometry.lean 1 declarations
SourceAssignedSupportedPath.lean 1 declarations
SourceAssignedTopConcentration.lean 1 declarations
SourceAssignedTopEnvelope.lean 6 declarations
SourceAssignedTopFamily.lean 10 declarations
SourceAssignedTopOffchild.lean 1 declarations
SourceAssignedTopPhysical.lean 7 declarations
SourceAssignedTopReference.lean 1 declarations
SourceAssignedTopSelector.lean 24 declarations
SourceAssignedTubeEnvelope.lean 1 declarations
SourceAssignedVertexPath.lean 2 declarations
SourceAveraging.lean 2 declarations
SourceAxisMaximal.lean 6 declarations
SourceBadEventUnion.lean 3 declarations
SourceBalancedBlend.lean 2 declarations
SourceBalancedGrid.lean 1 declarations
SourceBlockChildren.lean 7 declarations
SourceBlockConservation.lean 4 declarations
SourceBlockDisintegration.lean 2 declarations
SourceBlockException.lean 1 declarations
SourceBlockGraph.lean 2 declarations
SourceBlockLineGrid.lean 5 declarations
SourceBlockModulus.lean 4 declarations
SourceBlockPathMass.lean 5 declarations
SourceBlockPathMotion.lean 1 declarations
SourceBoundaryDeficit.lean 5 declarations
SourceBoundaryEntropy.lean 5 declarations
SourceBoundaryEntropyError.lean 1 declarations
SourceBoundaryErrorDecay.lean 2 declarations
SourceBoundaryExpectedLoss.lean 1 declarations
SourceBoundaryGeometry.lean 10 declarations
SourceBoundaryIntegrability.lean 1 declarations
SourceBoundaryIntegratedError.lean 1 declarations
SourceBoundaryIntegratedGain.lean 2 declarations
SourceBoundaryJointMeasurable.lean 5 declarations
SourceBoundaryLossBounds.lean 1 declarations
SourceBoundaryMajorant.lean 1 declarations
SourceBoundaryRadial.lean 3 declarations
SourceBoundaryRadius.lean 3 declarations
SourceBoundaryScales.lean 5 declarations
SourceBoundaryTotalError.lean 1 declarations
SourceBoundedDuality.lean 4 declarations
SourceBoundedInputEnergy.lean 2 declarations
SourceBoundedTreeSize.lean 5 declarations
SourceBoxIntegralComparison.lean 4 declarations
SourceBoxReproduction.lean 4 declarations
SourceBoxSupremum.lean 7 declarations
SourceBoxSupremumEnergy.lean 1 declarations
SourceCappedStepArithmetic.lean 4 declarations
SourceCarrierFreeEnvelope.lean 6 declarations
SourceCellMarking.lean 8 declarations
SourceCellPolynomial.lean 4 declarations
SourceCenteredCoefficient.lean 6 declarations
SourceCenteredMaskedVariation.lean 10 declarations
SourceCenteredSquareBound.lean 5 declarations
SourceCenteredSquareTail.lean 1 declarations
SourceCentralBudget.lean 3 declarations
SourceCentralBudgetAE.lean 2 declarations
SourceCentralHolder.lean 2 declarations
SourceCentralHolderAE.lean 1 declarations
SourceCentralPathGain.lean 1 declarations
SourceCentralPowerGain.lean 4 declarations
SourceCentralRootBudgetAE.lean 1 declarations
SourceCoefficientIntegrability.lean 3 declarations
SourceCommonTerminalIntegral.lean 2 declarations
SourceComparablePlanarGram.lean 1 declarations
SourceCoordinateSpectrum.lean 14 declarations
SourceCountParameters.lean 6 declarations
SourceCovariantTop.lean 1 declarations
SourceCrossAdjointEnergy.lean 2 declarations
SourceCrossConcentration.lean 1 declarations
SourceCrossDerivative.lean 4 declarations
SourceCrudeMassBudget.lean 1 declarations
SourceCrudeMoment.lean 3 declarations
SourceCrudeMomentAE.lean 2 declarations
SourceDeletionForest.lean 10 declarations
SourceDeletionTreeEstimate.lean 1 declarations
SourceDemodulatedCellEnergy.lean 1 declarations
SourceDemodulatedFourier.lean 4 declarations
SourceDemodulatedLong.lean 2 declarations
SourceDemodulatedSynthesis.lean 3 declarations
SourceDensityForest.lean 1 declarations
SourceDensityForestIntegral.lean 1 declarations
SourceDensityGeometry.lean 5 declarations
SourceDensityKeepers.lean 7 declarations
SourceDensityModel.lean 13 declarations
SourceDensityPowerForest.lean 3 declarations
SourceDensityRadius.lean 6 declarations
SourceDensityRebase.lean 8 declarations
SourceDensityRemovalIntegral.lean 1 declarations
SourceDensityScaledForest.lean 6 declarations
SourceDensitySpatialCost.lean 4 declarations
SourceDensityTail.lean 11 declarations
SourceDropDensity.lean 4 declarations
SourceDropSize.lean 4 declarations
SourceDropTreeTransport.lean 3 declarations
SourceEitherGrid.lean 1 declarations
SourceEnclosingScale.lean 1 declarations
SourceEnvelopeWeightComparison.lean 2 declarations
SourceErrorSupported.lean 5 declarations
SourceErrorTail.lean 4 declarations
SourceExponentialIntegral.lean 2 declarations
SourceFiberGram.lean 2 declarations
SourceFiniteExponentialIntegral.lean 4 declarations
SourceFiniteLongTree.lean 1 declarations
SourceFiniteSizeBound.lean 2 declarations
SourceFiniteThresholdLevels.lean 3 declarations
SourceFixedException.lean 1 declarations
SourceFourPolarizedConcentration.lean 5 declarations
SourceGlobalDyadicMaximal.lean 9 declarations
SourceGoodPathArea.lean 1 declarations
SourceGoodPathBudget.lean 1 declarations
SourceGoodPathSet.lean 4 declarations
SourceGramGeometry.lean 4 declarations
SourceGramMargin.lean 2 declarations
SourceGramSchur.lean 2 declarations
SourceGridParameters.lean 3 declarations
SourceHighDensityForest.lean 2 declarations
SourceInhabitedLabels.lean 23 declarations
SourceInsignificantShrink.lean 2 declarations
SourceInteractionGeometry.lean 5 declarations
SourceKernelIntegral.lean 2 declarations
SourceKernelShells.lean 6 declarations
SourceL2Gram.lean 3 declarations
SourceL2Sums.lean 2 declarations
SourceLabelScaleEnergy.lean 1 declarations
SourceLabeledActiveCardTail.lean 5 declarations
SourceLabeledActiveReference.lean 18 declarations
SourceLabeledActiveSpectrum.lean 5 declarations
SourceLabeledAdjointPolarization.lean 2 declarations
SourceLabeledCoefficientSplit.lean 4 declarations
SourceLabeledComparableEnergy.lean 4 declarations
SourceLabeledCrossIdentity.lean 2 declarations
SourceLabeledCrossResidual.lean 5 declarations
SourceLabeledDerivative.lean 3 declarations
SourceLabeledErrorBudget.lean 2 declarations
SourceLabeledErrorConvolution.lean 2 declarations
SourceLabeledErrorFamily.lean 15 declarations
SourceLabeledErrorPhysicalTail.lean 1 declarations
SourceLabeledErrorTail.lean 4 declarations
SourceLabeledGoodEvents.lean 9 declarations
SourceLabeledGoodQuantities.lean 6 declarations
SourceLabeledGoodTail.lean 2 declarations
SourceLabeledMainRestriction.lean 11 declarations
SourceLabeledMainSlots.lean 7 declarations
SourceLabeledMainTail.lean 4 declarations
SourceLabeledMaskedSlots.lean 10 declarations
SourceLabeledMotion.lean 5 declarations
SourceLabeledMultiscaleEnergy.lean 4 declarations
SourceLabeledNarrowTail.lean 5 declarations
SourceLabeledPolarization.lean 4 declarations
SourceLabeledPositiveSplit.lean 6 declarations
SourceLabeledRawEnvelope.lean 8 declarations
SourceLabeledRecenter.lean 8 declarations
SourceLabeledResidualEnvelope.lean 4 declarations
SourceLabeledResidualThreshold.lean 2 declarations
SourceLabeledScaleEnergy.lean 2 declarations
SourceLabeledSelectedVariation.lean 3 declarations
SourceLabeledSpectralGoodTail.lean 1 declarations
SourceLabeledStoppingVariation.lean 8 declarations
SourceLabeledSynthesisEnvelope.lean 7 declarations
SourceLabeledTopSum.lean 4 declarations
SourceLabeledUniformErrorTail.lean 1 declarations
SourceLabeledUniformGoodTail.lean 1 declarations
SourceLabeledVariationSplit.lean 9 declarations
SourceLabeledVariationTail.lean 3 declarations
SourceLatticeConcentration.lean 1 declarations
SourceLatticeGeometry.lean 4 declarations
SourceLatticeMultiscaleEnergy.lean 4 declarations
SourceLatticePolarization.lean 15 declarations
SourceLatticePolarizationSpectrum.lean 7 declarations
SourceLatticeRawData.lean 9 declarations
SourceLatticeScaleEnergy.lean 3 declarations
SourceLatticeSpectrum.lean 2 declarations
SourceLengthRestriction.lean 4 declarations
SourceLineGrid.lean 4 declarations
SourceLineMaximal.lean 12 declarations
SourceLineRescale.lean 2 declarations
SourceLineWindow.lean 7 declarations
SourceLocalLabelEnergy.lean 1 declarations
SourceLocalLabelVectorEnergy.lean 1 declarations
SourceLogMass.lean 1 declarations
SourceLongCellEnergy.lean 1 declarations
SourceLongCellMask.lean 5 declarations
SourceLongErrorGlobal.lean 2 declarations
SourceLongPrefixes.lean 8 declarations
SourceLongTreeSplit.lean 14 declarations
SourceLongTreeSupport.lean 2 declarations
SourceLpDamping.lean 3 declarations
SourceLpExhaustion.lean 5 declarations
SourceMarkedFactorsIntegral.lean 2 declarations
SourceMarkedIntegral.lean 4 declarations
SourceMarkedResidual.lean 1 declarations
SourceMarkedStop.lean 2 declarations
SourceMarkingParameters.lean 2 declarations
SourceMaskGeometry.lean 3 declarations
SourceMaskIntegral.lean 1 declarations
SourceMaskMotion.lean 8 declarations
SourceMaskTail.lean 4 declarations
SourceMaskedAmplitude.lean 3 declarations
SourceMaskedFrozenEstimate.lean 1 declarations
SourceMaskedPhysicalMoments.lean 2 declarations
SourceMaskedPhysicalTail.lean 1 declarations
SourceMaskedReference.lean 1 declarations
SourceMaskedSynthesis.lean 10 declarations
SourceMaskedTreeSplit.lean 2 declarations
SourceMaskedVariationTail.lean 6 declarations
SourceMassStopping.lean 10 declarations
SourceMaximalBound.lean 7 declarations
SourceMixedReference.lean 8 declarations
SourceModelDegenerateCases.lean 2 declarations
SourceModelThresholdScale.lean 5 declarations
SourceMonotoneMaximal.lean 5 declarations
SourceMotionBudget.lean 3 declarations
SourceMovingException.lean 1 declarations
SourceMovingWeights.lean 1 declarations
SourceNodeMeasurable.lean 7 declarations
SourceNodeRatio.lean 10 declarations
SourceNormalizedDecay.lean 4 declarations
SourceNormalizedMotion.lean 2 declarations
SourceNormalizedRemovalStep.lean 1 declarations
SourceOffchildMask.lean 4 declarations
SourceOffchildRegroup.lean 1 declarations
SourceOrdinaryAdjoint.lean 7 declarations
SourceOrdinaryAdjointEnergy.lean 1 declarations
SourceOrdinaryDensityForest.lean 2 declarations
SourceOrdinaryModelBound.lean 3 declarations
SourceOrdinaryModelConfig.lean 6 declarations
SourceOrdinaryModelEstimate.lean 2 declarations
SourceOrdinaryRemovalStep.lean 1 declarations
SourceOrdinarySizeStopping.lean 7 declarations
SourceOrdinarySizeTest.lean 9 declarations
SourceOrdinaryTreeEstimate.lean 3 declarations
SourceOrdinaryTreeIdentity.lean 1 declarations
SourceOriginalIntegrability.lean 4 declarations
SourceOriginalMarkedPath.lean 2 declarations
SourceOriginalParentMarkedPath.lean 2 declarations
SourceOriginalPathRegularity.lean 2 declarations
SourceOriginalRecovery.lean 1 declarations
SourcePackedEnvelopeEnergy.lean 2 declarations
SourceParameters.lean 11 declarations
SourceParentFullResidual.lean 1 declarations
SourceParentReferenceEvents.lean 13 declarations
SourceParentResidualReference.lean 2 declarations
SourceParentResidualSquare.lean 1 declarations
SourceParentStoppedBound.lean 2 declarations
SourceParentWidth.lean 1 declarations
SourcePathAmplitudeCongr.lean 4 declarations
SourcePathCoefficientMotion.lean 2 declarations
SourcePathCostBudget.lean 1 declarations
SourcePathCountInvariant.lean 3 declarations
SourcePathDropMotion.lean 2 declarations
SourcePathIntegrand.lean 7 declarations
SourcePathProduct.lean 13 declarations
SourcePathValues.lean 4 declarations
SourcePhysicalAmplitudeMeasurable.lean 4 declarations
SourcePhysicalAmplitudeMotion.lean 1 declarations
SourcePhysicalCellMarking.lean 1 declarations
SourcePhysicalCoefficient.lean 8 declarations
SourcePhysicalFullResidual.lean 1 declarations
SourcePhysicalGoodPath.lean 5 declarations
SourcePhysicalGoodResidual.lean 1 declarations
SourcePhysicalInsignificant.lean 1 declarations
SourcePhysicalNormalizedMotion.lean 1 declarations
SourcePhysicalOffchildGrouping.lean 2 declarations
SourcePhysicalPathAssembly.lean 3 declarations
SourcePhysicalPositiveScale.lean 10 declarations
SourcePhysicalPowerGain.lean 1 declarations
SourcePhysicalPropagatedTail.lean 1 declarations
SourcePhysicalReferenceSquare.lean 5 declarations
SourcePhysicalResidualNorm.lean 3 declarations
SourcePhysicalResidualSquare.lean 1 declarations
SourcePhysicalShiftedResidual.lean 1 declarations
SourcePhysicalSingleScale.lean 6 declarations
SourcePhysicalSquareTail.lean 1 declarations
SourcePhysicalStoppedBound.lean 2 declarations
SourcePhysicalTail.lean 2 declarations
SourcePhysicalUnaryEndpoint.lean 3 declarations
SourcePlanarGramSchur.lean 2 declarations
SourcePlanarKernelBound.lean 8 declarations
SourcePlanarPlancherel.lean 11 declarations
SourcePlanarPolynomial.lean 8 declarations
SourcePlanarSynthesis.lean 5 declarations
SourcePlanarVectorReproduction.lean 4 declarations
SourcePlaneIntegral.lean 3 declarations
SourcePlaneWeightCost.lean 2 declarations
SourcePolarizedCoefficient.lean 2 declarations
SourcePolarizedInterval.lean 8 declarations
SourcePolynomialGoodPathArea.lean 1 declarations
SourcePolynomialMassLog.lean 1 declarations
SourcePolynomialReferenceArea.lean 1 declarations
SourcePolynomialSelectedGoodPath.lean 1 declarations
SourcePositiveSelectedSynthesis.lean 3 declarations
SourcePropagatedTailBound.lean 2 declarations
SourceRadialAverage.lean 2 declarations
SourceRadialIntegral.lean 2 declarations
SourceRadialLoss.lean 4 declarations
SourceRadialMassBounds.lean 4 declarations
SourceRadialScales.lean 4 declarations
SourceRadialTelescoping.lean 1 declarations
SourceRecenterTransport.lean 5 declarations
SourceRecenteredSelectedTree.lean 1 declarations
SourceRecenteredTreeData.lean 2 declarations
SourceReciprocalWeightEnergy.lean 1 declarations
SourceRecordedEnergy.lean 4 declarations
SourceReferenceBandAll.lean 1 declarations
SourceReferenceBounds.lean 4 declarations
SourceReferenceCoordinates.lean 6 declarations
SourceReferenceLabelCount.lean 1 declarations
SourceReferenceLattice.lean 9 declarations
SourceReferenceMainRestriction.lean 4 declarations
SourceReferenceMask.lean 14 declarations
SourceReferenceMasks.lean 2 declarations
SourceReferenceMoments.lean 9 declarations
SourceReferenceOrdinaryTree.lean 1 declarations
SourceReferencePhysicalIdentity.lean 7 declarations
SourceReferencePolynomialTail.lean 1 declarations
SourceReferenceRestriction.lean 10 declarations
SourceReferenceSelectedVariation.lean 2 declarations
SourceReferenceSelectorGeometry.lean 3 declarations
SourceReferenceTail.lean 6 declarations
SourceReferenceTailOrder.lean 1 declarations
SourceReferenceThreshold.lean 3 declarations
SourceReferenceTreeSize.lean 4 declarations
SourceReferenceUnion.lean 19 declarations
SourceReferenceWeightedMaximal.lean 1 declarations
SourceReferenceWindowBudget.lean 5 declarations
SourceReproduction.lean 8 declarations
SourceResidualBlockBudget.lean 2 declarations
SourceResidualBlockGeometry.lean 7 declarations
SourceResidualCostBudget.lean 1 declarations
SourceResidualEnvelopes.lean 8 declarations
SourceResidualGeometry.lean 7 declarations
SourceResidualMask.lean 5 declarations
SourceResidualPolynomial.lean 1 declarations
SourceResidualPropagation.lean 18 declarations
SourceResidualSplit.lean 6 declarations
SourceResidualSquare.lean 4 declarations
SourceResidualVariation.lean 7 declarations
SourceResidualWeightBudget.lean 1 declarations
SourceRestrictedGram.lean 3 declarations
SourceReverseBlocks.lean 21 declarations
SourceReverseCellMarking.lean 1 declarations
SourceReverseDropComparison.lean 1 declarations
SourceReverseMarkedIntegral.lean 1 declarations
SourceReverseSnapshot.lean 3 declarations
SourceReverseWeights.lean 12 declarations
SourceRootCells.lean 5 declarations
SourceRootIntegral.lean 1 declarations
SourceRootedSelectedTree.lean 1 declarations
SourceScaleGramSplit.lean 3 declarations
SourceScaleRestriction.lean 5 declarations
SourceScaleRestrictionSums.lean 5 declarations
SourceScaledTopGood.lean 1 declarations
SourceSelectedArea.lean 1 declarations
SourceSelectedBoxSeparation.lean 3 declarations
SourceSelectedCoefficientBound.lean 1 declarations
SourceSelectedDuality.lean 4 declarations
SourceSelectedEnvelopeEnergy.lean 2 declarations
SourceSelectedFamily.lean 17 declarations
SourceSelectedGoodEvent.lean 2 declarations
SourceSelectedGoodPathArea.lean 1 declarations
SourceSelectedGram.lean 4 declarations
SourceSelectedPrefix.lean 7 declarations
SourceSelectedQuadratic.lean 2 declarations
SourceSelectedRecordSums.lean 2 declarations
SourceSelectedReferenceData.lean 5 declarations
SourceSelectedReferenceGeometry.lean 3 declarations
SourceSelectedResidualSquare.lean 1 declarations
SourceSelectedScale.lean 4 declarations
SourceSelectedTopEstimate.lean 1 declarations
SourceSelectedTopGeometry.lean 2 declarations
SourceSelectedTreeData.lean 5 declarations
SourceSharedGoodPath.lean 3 declarations
SourceSharpDensityForest.lean 2 declarations
SourceShearedEnvelopeEnergy.lean 4 declarations
SourceShiftNormalization.lean 3 declarations
SourceShiftSimplex.lean 4 declarations
SourceShiftedCellMotion.lean 5 declarations
SourceShiftedDrop.lean 7 declarations
SourceShiftedReferenceVariation.lean 2 declarations
SourceShiftedScales.lean 3 declarations
SourceShortDyadicBudget.lean 5 declarations
SourceShortTreeGlobal.lean 7 declarations
SourceShortTreeIntegral.lean 2 declarations
SourceShortTreeSum.lean 4 declarations
SourceSignedBoxSeparation.lean 4 declarations
SourceSignedSelectedArea.lean 1 declarations
SourceSignedSelectedSynthesis.lean 1 declarations
SourceSignedTopGeometry.lean 1 declarations
SourceSimplexLp.lean 3 declarations
SourceSimplexLpExhaustion.lean 1 declarations
SourceSimplexLpOn.lean 3 declarations
SourceSimultaneousCount.lean 3 declarations
SourceSingleScaleEnvelope.lean 4 declarations
SourceSizeRemovalIntegral.lean 1 declarations
SourceSlopeLabels.lean 16 declarations
SourceSlotTails.lean 7 declarations
SourceSlottedCoefficient.lean 20 declarations
SourceSlottedConcentration.lean 5 declarations
SourceSlottedLattice.lean 25 declarations
SourceSnapshotAmplitudeScale.lean 2 declarations
SourceSnapshotChoice.lean 1 declarations
SourceSnapshotPolynomial.lean 2 declarations
SourceSnapshotSize.lean 6 declarations
SourceSnapshotWindow.lean 8 declarations
SourceSpatialSelectedTree.lean 1 declarations
SourceSpatialSubdivision.lean 7 declarations
SourceSpatialTreePieces.lean 4 declarations
SourceStepArithmetic.lean 3 declarations
SourceStopCostBudget.lean 1 declarations
SourceStoppedAmplitude.lean 7 declarations
SourceStoppedError.lean 5 declarations
SourceStoppedIntegral.lean 2 declarations
SourceStoppedMarking.lean 1 declarations
SourceStoppedMassPower.lean 2 declarations
SourceStoppedRecurrence.lean 4 declarations
SourceStrongDyadicMaximal.lean 11 declarations
SourceTerminalScale.lean 7 declarations
SourceThreeGridMaximal.lean 8 declarations
SourceThreeGridPlane.lean 16 declarations
SourceThresholdSum.lean 10 declarations
SourceThresholdWeights.lean 5 declarations
SourceTiledLineIntegral.lean 10 declarations
SourceTopConcentration.lean 1 declarations
SourceTopGood.lean 1 declarations
SourceTopReferenceGeometry.lean 2 declarations
SourceTopWeightTransfer.lean 2 declarations
SourceTotalWeightBudget.lean 2 declarations
SourceTreeCellDensity.lean 5 declarations
SourceTreeCellGluing.lean 7 declarations
SourceTreeCells.lean 13 declarations
SourceTreeConservation.lean 9 declarations
SourceTreeDensityTerm.lean 5 declarations
SourceTreeErrorIntegral.lean 2 declarations
SourceTreeExitBound.lean 1 declarations
SourceTreeExpansion.lean 5 declarations
SourceTreeForestIntegral.lean 1 declarations
SourceTreeGoodPaths.lean 1 declarations
SourceTreeMomentBudget.lean 1 declarations
SourceTreeProbability.lean 4 declarations
SourceTreeSelectorError.lean 8 declarations
SourceTreeSpectrum.lean 6 declarations
SourceTreeVertexIntegral.lean 1 declarations
SourceTreeVertexMoment.lean 1 declarations
SourceTrimInteractions.lean 1 declarations
SourceTwoSidedRemovedIntegral.lean 1 declarations
SourceTwoSidedSizeArea.lean 1 declarations
SourceTypeUniformCentral.lean 2 declarations
SourceTypeUniformMoments.lean 3 declarations
SourceUnaryErrorBudget.lean 2 declarations
SourceUniformDamping.lean 2 declarations
SourceUnsignedSizeMonotone.lean 1 declarations
SourceVectorEnvelope.lean 3 declarations
SourceVectorPolynomial.lean 4 declarations
SourceVectorReproduction.lean 3 declarations
SourceVectorSchwartz.lean 9 declarations
SourceVectorSlices.lean 6 declarations
SourceVertexConstantBudget.lean 2 declarations
SourceVertexPlaneParameters.lean 1 declarations
SourceVerticalDemodulation.lean 12 declarations
SourceWeightPointwiseBudget.lean 3 declarations
SourceWeightedBadPath.lean 3 declarations
SourceWeightedCellSupremum.lean 2 declarations
SourceWeightedEnvelopeKernel.lean 6 declarations
SourceWeightedPairing.lean 2 declarations
SourceWeightedTreeEnergy.lean 8 declarations
SourceWeightedTreeMajorant.lean 5 declarations
SourceWeightedTreeMaximal.lean 17 declarations
SourceWhitneyDensityTest.lean 4 declarations
SourceWhitneyGluing.lean 12 declarations
SourceWhitneyIntervals.lean 14 declarations
SourceWhitneySummation.lean 4 declarations
SourceWideLogMass.lean 4 declarations
SourceWindowAverage.lean 4 declarations
SourceZeroDensity.lean 2 declarations
StripMassOperations.lean 8 declarations
ThreeGridWeakL1.lean 5 declarations
UnaryEnergy.lean 11 declarations
UnaryPartitionSum.lean 5 declarations
UnaryPropagation.lean 10 declarations
UnaryRunCharging.lean 11 declarations
UnaryRunResidual.lean 1 declarations
UnaryRunVariation.lean 2 declarations
UnaryRuns.lean 6 declarations
UnarySegmentEstimate.lean 2 declarations
UnarySegmentation.lean 3 declarations
UnaryTelescope.lean 8 declarations
VertexIntegration.lean 9 declarations