`OAI/GroupTheory/PolycyclicRecognition/Analysis/`

1749 declarations, 0 contain sorry, 0 declared as axioms; 549 files

Files

AbelianMultilinearChains.lean 3 declarations
AccessibleProfilePaths.lean 1 declarations
AccessibleWordPaths.lean 1 declarations
AffineAction.lean 10 declarations
AffineFacetAgreement.lean 1 declarations
AffineFromHorizontalLabels.lean 1 declarations
AffineLabels.lean 2 declarations
AffineMeanApproximation.lean 5 declarations
AffinePolynomialTopology.lean 11 declarations
AffineProfileConcentration.lean 6 declarations
AffineProfileControlledPaths.lean 1 declarations
AffineProfileGluing.lean 2 declarations
AffineProfileLines.lean 2 declarations
AffineScaleStabilization.lean 1 declarations
AffineSheetAgreement.lean 5 declarations
AllScaleProfileEquicontinuity.lean 3 declarations
AlternatingBarEndpoints.lean 1 declarations
AlternatingHaarImage.lean 1 declarations
AmenableCorrection.lean 17 declarations
AnchoredTilePacking.lean 2 declarations
ApproximateHarmonicLimit.lean 2 declarations
ApproximateInvariantMean.lean 3 declarations
AscendingBaseTransport.lean 6 declarations
AsymptoticEquicontinuity.lean 2 declarations
BackwardRecurrenceAsymptotics.lean 3 declarations
BackwardRecurrenceProbability.lean 1 declarations
BackwardSwitchProbability.lean 7 declarations
BadCharacterCompactness.lean 5 declarations
BarChainExhaustion.lean 4 declarations
BasedImagePaths.lean 5 declarations
BasepointAffineSeparation.lean 2 declarations
BasepointCellDomination.lean 2 declarations
BasepointProfileIdentity.lean 2 declarations
BasisDynkinHaar.lean 1 declarations
BoundedCoarseRayFactorBounds.lean 1 declarations
BoundedPathGrowth.lean 8 declarations
BoundedPathPacking.lean 2 declarations
BoundedProbabilityMean.lean 1 declarations
BoxCoordinateChanges.lean 6 declarations
BoxInteriorSlack.lean 1 declarations
BoxWordExpansion.lean 2 declarations
BridgedProfileBounds.lean 1 declarations
CayleyBallCover.lean 11 declarations
CayleyBallCutoff.lean 9 declarations
CayleyHarmonic.lean 7 declarations
CayleyWordBallAlgebra.lean 4 declarations
CellOccupationError.lean 3 declarations
CellProbabilityTransport.lean 1 declarations
CellProfileRestriction.lean 2 declarations
CenteredImagePaths.lean 3 declarations
CenteredProfilePaths.lean 3 declarations
CenteredTuplePaths.lean 6 declarations
ChainProducts.lean 6 declarations
ChainSuccessor.lean 14 declarations
ChainWords.lean 1 declarations
ChainZeroProjection.lean 7 declarations
ChronologicalAlternatingHaar.lean 1 declarations
CoarseEquivalence.lean 11 declarations
CoarseEquivalenceMetric.lean 5 declarations
CoarseModelMean.lean 1 declarations
CoarseModelUnimodular.lean 1 declarations
CoarseMultiplicity.lean 2 declarations
CoarseNegativeQuotient.lean 3 declarations
CoarsePackingAsymptotics.lean 4 declarations
CoarsePairMetricChange.lean 1 declarations
CoarsePathConcatenation.lean 8 declarations
CoarsePathMesh.lean 1 declarations
CoarsePathRadius.lean 2 declarations
CoarsePathWords.lean 5 declarations
CoarseRayFactorBounds.lean 1 declarations
CoarseRayQuotientLimits.lean 1 declarations
CocycleCompactWords.lean 3 declarations
CocycleHaarAverage.lean 2 declarations
CocyclePullbackSublinear.lean 1 declarations
CofiberChainConnecting.lean 2 declarations
CofiberChainSequence.lean 7 declarations
CommutingIntegralHom.lean 3 declarations
CompactAeExhaustion.lean 1 declarations
CompactCharacterCertificates.lean 3 declarations
CompactCharacterSeparation.lean 1 declarations
CompactErgodicDecomposition.lean 1 declarations
CompactExtensionModels.lean 3 declarations
CompactFiniteDimensionalHull.lean 5 declarations
CompactGeneratingBalls.lean 3 declarations
CompactImageVolume.lean 1 declarations
CompactInverseSections.lean 1 declarations
CompactLiftContinuity.lean 1 declarations
CompactLiftQuotient.lean 2 declarations
CompactLifts.lean 1 declarations
CompactPairs.lean 8 declarations
CompactProbabilityDensity.lean 2 declarations
CompactProbabilityProduct.lean 4 declarations
CompactProbeLift.lean 3 declarations
CompactProbeSequence.lean 1 declarations
CompactProfileEstimates.lean 1 declarations
CompactSamplingMean.lean 4 declarations
CompactSectionVolume.lean 2 declarations
CompactSegmentLimit.lean 1 declarations
CompactSetMeanApproximation.lean 3 declarations
CompactSubmersionFamily.lean 2 declarations
CompactSupportSlack.lean 1 declarations
CompactTupleThickening.lean 1 declarations
CompactWordCost.lean 13 declarations
CompatibleMetricComparison.lean 1 declarations
ConditionedGoodProbeOffset.lean 1 declarations
ConditionedProbeSelection.lean 2 declarations
ConditionedProbeSequence.lean 1 declarations
ConeAdaptedPathBasis.lean 3 declarations
ConeIdealBoxCalculus.lean 10 declarations
ConeIdealInnerHaar.lean 2 declarations
ConeIdealMeasuredTiling.lean 1 declarations
ConeIdealTiling.lean 1 declarations
ConeKernelHaar.lean 1 declarations
ConeOffsetExponent.lean 2 declarations
ConeOffsetPacking.lean 2 declarations
ConeProbeEndpoints.lean 6 declarations
ConeProbeIntrinsicTiles.lean 4 declarations
ConeProbeRestrictionPacking.lean 1 declarations
ConeProfileOffsetPacking.lean 1 declarations
ConeQuotientHaar.lean 1 declarations
ConeQuotientHaarAction.lean 1 declarations
ConeSamplingTemplate.lean 1 declarations
ConeSourceCellVolumes.lean 1 declarations
ConjugatedSheetPaths.lean 1 declarations
ConnectedEMetric.lean 1 declarations
ConnectedHomCovering.lean 3 declarations
ConnectedQuasiUnipotentAction.lean 3 declarations
ConstructChainMetric.lean 2 declarations
ContinuousCoarseRayLimits.lean 1 declarations
ControlledChainGenerators.lean 2 declarations
ControlledChainRepresentation.lean 4 declarations
ControlledChainWords.lean 4 declarations
ControlledFaceSupport.lean 7 declarations
ControlledFiniteChains.lean 8 declarations
ControlledMetricFolner.lean 2 declarations
ControlledPathErrorEnvelope.lean 1 declarations
ConvergingPolynomialImage.lean 2 declarations
ConvexMicrosteps.lean 1 declarations
ConvexOrbit.lean 2 declarations
CoordinateChartSampling.lean 7 declarations
CoordinatePacking.lean 3 declarations
CoordinateRemez.lean 1 declarations
CoordinateStationaryPaths.lean 1 declarations
CorrelatedAlternatingHaar.lean 1 declarations
CountableErgodicComponents.lean 2 declarations
CountableMeasureTests.lean 6 declarations
CyclicInvariantMean.lean 6 declarations
DenseConvexConstraints.lean 2 declarations
DenseInvariantMeasure.lean 1 declarations
DeterministicProbabilityComparison.lean 2 declarations
DeterministicProfileCenters.lean 2 declarations
DiagonalAffineCellProfiles.lean 1 declarations
DiagonalCellProfilePairs.lean 2 declarations
DiagonalProfileSampling.lean 3 declarations
DifferentCellDomination.lean 1 declarations
DominatedAffineComparison.lean 1 declarations
DominatedAffineLabels.lean 1 declarations
DominatedProfileConcentration.lean 1 declarations
DynkinHaarConstruction.lean 1 declarations
ElementaryAmenable.lean 8 declarations
ErgodicDecompositionInput.lean 3 declarations
ErgodicMap.lean 1 declarations
ErgodicMixtureLimits.lean 2 declarations
EventualLiftVolumeCover.lean 1 declarations
EventualPolynomialImage.lean 1 declarations
EventualSupportedSampling.lean 2 declarations
ExactProfileTransport.lean 4 declarations
ExtensionInvariantMean.lean 14 declarations
ExteriorShiftIntegrality.lean 6 declarations
FactorProductPacking.lean 6 declarations
FactorProductVolumeBound.lean 1 declarations
FactorQuotientChainDecay.lean 1 declarations
FiniteAffineSelection.lean 5 declarations
FiniteConjugateTiling.lean 1 declarations
FiniteFolnerMean.lean 2 declarations
FiniteIndexQuasiUnipotentAction.lean 1 declarations
FiniteIntegralRepresentations.lean 5 declarations
FiniteIntegralTorsion.lean 1 declarations
FiniteKernelCoarseEquivalence.lean 2 declarations
FiniteLabelTransport.lean 3 declarations
FiniteModeProfileChains.lean 2 declarations
FiniteModuleOfIntegralAction.lean 1 declarations
FiniteNormalConjugationCover.lean 2 declarations
FiniteProfileEnvelope.lean 1 declarations
FiniteSupportChainPaths.lean 2 declarations
FiniteSupportInterpolation.lean 7 declarations
FiniteTranslateCover.lean 3 declarations
FiniteWordMetric.lean 8 declarations
FixedSlicePacking.lean 6 declarations
FixedSliceVolumeComparison.lean 1 declarations
FlatSwitchSamples.lean 5 declarations
FolnerInvariantMean.lean 5 declarations
FolnerRatio.lean 1 declarations
GeneratorPrefixChain.lean 4 declarations
GenericLipschitzProfile.lean 1 declarations
GenericProfileChambers.lean 2 declarations
GenericProfileSigns.lean 1 declarations
GlobalProfileAffinity.lean 1 declarations
GoodProfileSampling.lean 2 declarations
GoodProfileSegment.lean 1 declarations
GoodSheetProfileAgreement.lean 1 declarations
GradedHaar.lean 3 declarations
GroupDimensionTransport.lean 2 declarations
GroupIncrementLipschitz.lean 1 declarations
GrowingConvergingPolynomialImage.lean 1 declarations
GrowingEventualPolynomialImage.lean 1 declarations
GrowingPolynomialImage.lean 1 declarations
GrowingSubmersivePolynomialImage.lean 1 declarations
HaarAveraging.lean 14 declarations
HaarAveragingScales.lean 3 declarations
HaarBoxRadius.lean 2 declarations
HaarInvariantRepresentative.lean 2 declarations
HaarMeasureTransfer.lean 1 declarations
HaarOrbitAverages.lean 3 declarations
HaarPrefixCoordinates.lean 12 declarations
HaarProduct.lean 12 declarations
HarmonicAveragingDimension.lean 3 declarations
HarmonicCoverEnergy.lean 8 declarations
HarmonicCoverFactorBound.lean 1 declarations
HarmonicDimensionCriterion.lean 3 declarations
HarmonicGoodScaleFactors.lean 7 declarations
HarmonicGoodScales.lean 3 declarations
HarmonicSeparatedRadii.lean 7 declarations
HarmonicSpectralSubspace.lean 7 declarations
HarmonicTranslationImage.lean 3 declarations
HarmonicVolumeDeterminant.lean 7 declarations
HorizontalProfileLabels.lean 1 declarations
HorseshoeCover.lean 22 declarations
IdealSectionBoxCoordinates.lean 7 declarations
IndependentCellConcentration.lean 1 declarations
IndependentCellDomination.lean 1 declarations
IndependentConditionedOffset.lean 1 declarations
IndependentProfileLimits.lean 1 declarations
IndependentSupportedSampling.lean 1 declarations
InjectivePatchVolume.lean 1 declarations
IntegralBarNaturality.lean 3 declarations
IntegralBilinearExtension.lean 8 declarations
IntegralBilinearRealization.lean 2 declarations
IntegralFinsuppFunctor.lean 5 declarations
IntegralKernelRepresentation.lean 11 declarations
IntegralLinearExtension.lean 6 declarations
IntegralMatrixFiniteOrder.lean 3 declarations
IntegralQuotientKernel.lean 12 declarations
IntegralRepresentationMap.lean 4 declarations
IntegralSemisimpleTwist.lean 1 declarations
IntrinsicKernelPacking.lean 1 declarations
IntrinsicTraceFromHaar.lean 1 declarations
InvariantIntegralCurve.lean 3 declarations
InvariantMeanGenerators.lean 2 declarations
InvariantMetrization.lean 14 declarations
InverseCompactControl.lean 4 declarations
InwardFacetSegment.lean 1 declarations
JacobianMeasure.lean 2 declarations
KernelHaarTransport.lean 4 declarations
LeftInvariantRiemannianMetric.lean 9 declarations
LiftVolumeCover.lean 2 declarations
LinearDeterminantMeasure.lean 4 declarations
LinearHaarCoordinates.lean 2 declarations
LinearMetricChains.lean 4 declarations
LinearProfilesOnBall.lean 5 declarations
LinearSupportSymmetries.lean 3 declarations
LinkedProbeOffset.lean 1 declarations
LipschitzInversePairBounds.lean 2 declarations
LipschitzPairReplacement.lean 1 declarations
LipschitzProfileFTC.lean 3 declarations
LipschitzReplacement.lean 1 declarations
LocalLipschitzMinimizing.lean 1 declarations
LocalProfileAffinity.lean 2 declarations
LocallyCompactErgodicComponents.lean 3 declarations
LocallyCompactGroupEmbedding.lean 1 declarations
LogarithmicBoxScale.lean 1 declarations
LowerPacking.lean 3 declarations
MatrixPacking.lean 7 declarations
MeanProbabilityConverse.lean 1 declarations
MeanSubgroup.lean 8 declarations
MeasurableGeneratorChain.lean 1 declarations
MeasurableProbeProfiles.lean 2 declarations
MeasurePacking.lean 6 declarations
MeasurePreservingLimit.lean 2 declarations
MeasuredGoodProbeOffset.lean 1 declarations
MeasuredProbeOffset.lean 1 declarations
MeasuredProbeRegions.lean 2 declarations
MeasuredRegionOffset.lean 1 declarations
MeasuredRegionsFromCoordinates.lean 1 declarations
MeasuredTwoPathOffset.lean 1 declarations
MetricChainWords.lean 1 declarations
MetricCoarseBridge.lean 5 declarations
MetricFactorBounds.lean 1 declarations
MetricFactorComparison.lean 1 declarations
MetricFolnerCount.lean 2 declarations
MetricFolnerMean.lean 2 declarations
MetricFolnerTransfer.lean 1 declarations
MetricFolnerUnimodular.lean 1 declarations
MetricFolnerVolume.lean 5 declarations
MetricQuasiEquivalence.lean 6 declarations
MetricSegmentsFromMidpoints.lean 1 declarations
MetricTent.lean 9 declarations
MidpointStepPaths.lean 6 declarations
MinimizingMetricChains.lean 1 declarations
MixedCellConcentration.lean 1 declarations
MixedScaleBasisBound.lean 1 declarations
MixedWordBoxModel.lean 18 declarations
ModelBoxTranslation.lean 1 declarations
ModelCellOccupation.lean 1 declarations
ModelCubeHaar.lean 1 declarations
NaturalOrientationTransport.lean 2 declarations
NegativePathWords.lean 3 declarations
NeighborProfileGluing.lean 5 declarations
NilpotentBallVolume.lean 4 declarations
NilpotentBoxes.lean 6 declarations
NilpotentChainPacking.lean 2 declarations
NilpotentConjugationMetric.lean 1 declarations
NilpotentHaarAutomorphisms.lean 3 declarations
NilpotentHaarConstruction.lean 1 declarations
NilpotentHaarInput.lean 3 declarations
NilpotentHaarSymmetry.lean 2 declarations
NilpotentNegativePaths.lean 1 declarations
NilpotentWordMetric.lean 2 declarations
NoetherianIntegralTorsion.lean 1 declarations
NormalInductionSupport.lean 2 declarations
NormalizedCellDomination.lean 1 declarations
NormalizedEndpointMeasure.lean 4 declarations
NormalizedMetricTent.lean 9 declarations
NormalizedPairErgodicDecomposition.lean 1 declarations
NormalizedPairPacking.lean 4 declarations
NormalizedProbeGenerator.lean 3 declarations
NormalizedTuplePacking.lean 3 declarations
OccupationCompactRestriction.lean 4 declarations
OccupationSampling.lean 9 declarations
OneParameterIntegralCurve.lean 2 declarations
OrbitAverageErgodicity.lean 1 declarations
OrbitAverageIntegral.lean 2 declarations
OrbitFiberAsymptotics.lean 2 declarations
Packing.lean 10 declarations
PairChainSublinear.lean 2 declarations
PairChartSampling.lean 4 declarations
PairErgodic.lean 2 declarations
PairMeanApproximation.lean 1 declarations
PairMeanControl.lean 4 declarations
PairMeasureScaling.lean 4 declarations
PairPathMesh.lean 4 declarations
PairStationaryIncrement.lean 2 declarations
PairSublinear.lean 5 declarations
ParametrizedSupportPaths.lean 4 declarations
PathVolumeComparison.lean 1 declarations
PolarProbeImages.lean 1 declarations
PolycyclicInvariantMean.lean 6 declarations
PolynomialBallScales.lean 6 declarations
PolynomialBoxAbsorption.lean 2 declarations
PolynomialEndpointCoordinates.lean 7 declarations
PolynomialEndpointSchemes.lean 6 declarations
PolynomialEnergyScales.lean 2 declarations
PolynomialHarmonicFiniteDimensional.lean 2 declarations
PolynomialHarmonicFunctions.lean 9 declarations
PolynomialNegativePaths.lean 1 declarations
PolynomialPackingAlgebra.lean 3 declarations
PositiveProjectionCell.lean 1 declarations
ProbeAnchorHaarBounds.lean 2 declarations
ProbeCellVolume.lean 2 declarations
ProbeImageBridge.lean 9 declarations
ProbeImageGeometry.lean 1 declarations
ProbeImageTileCover.lean 2 declarations
ProbeKernelVolume.lean 4 declarations
ProbePivotBridge.lean 2 declarations
ProbeRestrictionComposition.lean 3 declarations
ProbeSectionRestrictions.lean 3 declarations
ProbeSourcePacking.lean 3 declarations
ProbeTileSelector.lean 1 declarations
ProductProbeSelection.lean 6 declarations
ProfileAffinityCriterion.lean 1 declarations
ProfileChainConcentration.lean 2 declarations
ProfileCompactness.lean 1 declarations
ProfileIncrementLimits.lean 4 declarations
ProfileLawIntegral.lean 2 declarations
ProfileLawProduct.lean 2 declarations
ProfileParameterContinuity.lean 5 declarations
ProfilePointwiseBounds.lean 3 declarations
ProfileRegularity.lean 4 declarations
ProperCocompactMetric.lean 4 declarations
ProperMetricMidpoints.lean 1 declarations
QuantitativeInjectiveCover.lean 1 declarations
QuotientChainDecay.lean 3 declarations
QuotientSectionHaar.lean 1 declarations
QuotientSectionMeasure.lean 2 declarations
QuotientSectionRightHaar.lean 8 declarations
QuotientSectionVolume.lean 3 declarations
RationalQuasiUnipotentFiltration.lean 2 declarations
RayCompactCollapse.lean 2 declarations
ReachableTuplePaths.lean 2 declarations
RecognitionFromCanonicalAffine.lean 2 declarations
RecurrenceIntegralBounds.lean 2 declarations
ReflectedSegmentSupport.lean 6 declarations
RegularWalkHarmonic.lean 3 declarations
RemezFromInterpolation.lean 1 declarations
RemezInput.lean 1 declarations
RescaledAffineComparison.lean 6 declarations
RescaledAlternatingEndpoints.lean 2 declarations
RescaledBasisScaleChange.lean 2 declarations
RescaledBoxTranslation.lean 1 declarations
RescaledImageVolume.lean 2 declarations
RescaledMetricSmallness.lean 3 declarations
RescaledProbeChains.lean 1 declarations
RescaledProfileLegs.lean 2 declarations
RescaledProfiles.lean 4 declarations
RescaledTranslatedChains.lean 1 declarations
RescaledTupleVolume.lean 4 declarations
RescaledWordEndpoints.lean 3 declarations
RetainedProbeAnchors.lean 3 declarations
RightFolnerExpansion.lean 5 declarations
SampledProfileIncrements.lean 1 declarations
SampledSuccessfulVolume.lean 3 declarations
ScaleExtension.lean 4 declarations
ScaleLabelStabilization.lean 6 declarations
ScaledIntegralCover.lean 2 declarations
SectionProbePacking.lean 1 declarations
SectionProbeReparametrization.lean 6 declarations
SectionSubtypeProbePacking.lean 2 declarations
SectionTileVolume.lean 2 declarations
SectionVolume.lean 1 declarations
SegmentProfileLegs.lean 2 declarations
SegmentSupportTimes.lean 4 declarations
SelfQuasiIsometry.lean 5 declarations
SeparatedTupleVolume.lean 2 declarations
SequenceAccessiblePaths.lean 1 declarations
SequenceBackwardAsymptotics.lean 3 declarations
SequenceCellProfilePairs.lean 3 declarations
SequenceCellProfileSegment.lean 1 declarations
SequenceCellProfiles.lean 2 declarations
SequenceCompactImage.lean 1 declarations
SequenceCompactSections.lean 1 declarations
SequenceConeQuotientBoxes.lean 1 declarations
SequenceConvergingPolynomialImage.lean 1 declarations
SequenceEventualPolynomialImage.lean 1 declarations
SequenceFixedSliceVolume.lean 1 declarations
SequenceGoodProfileSegment.lean 1 declarations
SequenceLogMetric.lean 1 declarations
SequenceMetricFactorBounds.lean 1 declarations
SequencePathCover.lean 1 declarations
SequencePathPacking.lean 1 declarations
SequencePolynomialImage.lean 1 declarations
SequenceProfileSampling.lean 3 declarations
SequenceQuotientVolume.lean 2 declarations
SequenceRescaledImageVolume.lean 1 declarations
SequenceSampledSuccessfulVolume.lean 1 declarations
SequenceScaleExtraction.lean 2 declarations
SequenceSectionTileVolume.lean 3 declarations
SequenceSubmersivePolynomialImage.lean 1 declarations
SequenceTilePacking.lean 1 declarations
SequenceTupleVolume.lean 2 declarations
SequenceVolumeComparison.lean 3 declarations
ShortSubgroupChains.lean 5 declarations
ShrinkingProfileDomains.lean 3 declarations
SkewMeasureFiber.lean 1 declarations
SmallCoefficientMean.lean 8 declarations
SmallCoefficientRationalMean.lean 7 declarations
SmallFactorCell.lean 2 declarations
SourceBundleBlockPaths.lean 7 declarations
SourceBundleHaarImage.lean 2 declarations
SourceBundlePaths.lean 1 declarations
SourceBundleTerminalPaths.lean 1 declarations
SourceMetricFolner.lean 2 declarations
StationaryApproximation.lean 4 declarations
StationaryCentered.lean 12 declarations
StationaryIntegralMicrosteps.lean 1 declarations
StationaryMesh.lean 3 declarations
StationaryPathSampling.lean 1 declarations
StationaryProbability.lean 11 declarations
StationarySampling.lean 2 declarations
StationarySlope.lean 15 declarations
StationaryVolumeAlgebra.lean 3 declarations
SubexponentialCompactImage.lean 1 declarations
SubexponentialPathPacking.lean 1 declarations
SubexponentialPolynomialImage.lean 1 declarations
SubexponentialQuotientVolume.lean 1 declarations
SubexponentialVolumeComparison.lean 3 declarations
SubgroupPacking.lean 2 declarations
SublinearAccessiblePaths.lean 1 declarations
SublinearRayIdentification.lean 2 declarations
SublinearScaleOffsets.lean 1 declarations
SublinearSheetLimits.lean 1 declarations
SubmersivePolynomialImage.lean 1 declarations
SuccessfulBlockPaths.lean 2 declarations
SuccessfulSampleBlockPaths.lean 3 declarations
SuccessfulSamplePaths.lean 2 declarations
SuccessfulWordPaths.lean 5 declarations
SupportDirectionCap.lean 1 declarations
SupportFromTrace.lean 3 declarations
SupportNorm.lean 20 declarations
SupportPolytope.lean 10 declarations
SupportStrictInterior.lean 1 declarations
SupportSymmetries.lean 6 declarations
SupportTemplates.lean 22 declarations
SupportTransport.lean 2 declarations
SupportVisitImage.lean 2 declarations
SupportVisitPaths.lean 6 declarations
SupportVisitRescale.lean 2 declarations
SupportWordImage.lean 3 declarations
SupportedAffineProbeSelection.lean 1 declarations
SupportedCellOccupation.lean 1 declarations
SupportedChainProbeSelection.lean 1 declarations
SupportedGoodSetSelection.lean 2 declarations
SupportedPairAgreement.lean 1 declarations
SupportedProbabilityRestriction.lean 4 declarations
SupportedProbeSelection.lean 2 declarations
SupportedProfileConstraints.lean 3 declarations
SwitchEndpoints.lean 5 declarations
TemplateBoxEnvelopes.lean 4 declarations
TemplateOffsetCones.lean 8 declarations
TemplateSupportDirections.lean 1 declarations
TemplateSupportOrder.lean 3 declarations
ThreeProbeConcentration.lean 2 declarations
TiledProbeSamplers.lean 1 declarations
TraceFromKernelHaar.lean 1 declarations
TranslatedBoxMass.lean 3 declarations
TranslatedCellDomination.lean 1 declarations
TranslatedNegativeChains.lean 2 declarations
TranslationCovering.lean 6 declarations
TriangulableMetricChoice.lean 1 declarations
TrivialTensorChainNaturality.lean 2 declarations
TrivialTensorChains.lean 3 declarations
TupleChainPrism.lean 7 declarations
TupleFixedSlicePacking.lean 4 declarations
TupleMeasureScaling.lean 2 declarations
UniformBoxTranslation.lean 2 declarations
UniformHarmonicDimensionBound.lean 1 declarations
UniformIntervalSamples.lean 6 declarations
UniformProfileConcentration.lean 6 declarations
UnitSeparatedNet.lean 3 declarations
UnitaryApproximateHarmonic.lean 1 declarations
UnitaryCompactAverage.lean 1 declarations
UnivariateRemez.lean 2 declarations
VolumeExponents.lean 1 declarations
WordBallControlledSubspace.lean 6 declarations
WordBallEscape.lean 1 declarations
WordBallGram.lean 8 declarations
WordBallGramOrder.lean 6 declarations
WordBallLeftShift.lean 2 declarations
WordBallQuadraticForms.lean 10 declarations
WordBallSamplingSequence.lean 1 declarations
WordBoxComparison.lean 2 declarations
WordChartLeftShift.lean 8 declarations
WordChartLogBound.lean 2 declarations
WordChartPivot.lean 3 declarations
WordChartScaleTransition.lean 5 declarations
WordChartSmallProducts.lean 3 declarations
WordChartTranslations.lean 1 declarations
WordMetricBridge.lean 7 declarations
WordSupportPaths.lean 1 declarations
ZeroWidthQuotientBoxes.lean 3 declarations