OAI/Combinatorics/Progressions/Geometry/

Files

• ActualCandidateSpatialCenter.lean 3 declarations
• ActualFixedSpatialDenseSliceCenter.lean 13 declarations
• ActualFixedSpatialNumericalPatchEndpoint.lean 2 declarations
• ActualFixedSpatialPreparedCertificate.lean 3 declarations
• ActualFixedSpatialRetainedModulusBudget.lean 16 declarations
• ActualFixedSpatialRetainedPatchEndpoint.lean 31 declarations
• ActualFixedSpatialSlicedAnalyticIdentification.lean 7 declarations
• ActualFixedSpatialSlicedDataComparison.lean 9 declarations
• ActualFixedSpatialSlicedModelPrecision.lean 15 declarations
• ActualFixedSpatialSlicedPrimitiveGeometry.lean 5 declarations
• ActualFixedSpatialSlicedSourceLog.lean 4 declarations
• ActualFixedSpatialSlicedTargetReal.lean 25 declarations
• AllocatedActiveSiteChartValues.lean 6 declarations
• AllocatedActiveSiteSupport.lean 4 declarations
• AllocatedAmbientBoxTests.lean 28 declarations
• AllocatedAmbientLongBox.lean 14 declarations
• AllocatedAmbientSiteCoordinates.lean 6 declarations
• AllocatedArraySupport.lean 2 declarations
• AllocatedCanonicalSpatialCoarseSource.lean 5 declarations
• AllocatedCanonicalSpatialProxy.lean 6 declarations
• AllocatedCenteredJointExcessTransport.lean 2 declarations
• AllocatedChartIdealAmbientLift.lean 1 declarations
• AllocatedChartIdealModelBound.lean 1 declarations
• AllocatedCommonSupportedMesh.lean 6 declarations
• AllocatedConstructedSpatialIdeal.lean 1 declarations
• AllocatedDetectedSpatialNativeSource.lean 3 declarations
• AllocatedEnormousProfileSupport.lean 2 declarations
• AllocatedExternalCandidateAxisChartOrbit.lean 3 declarations
• AllocatedExternalCandidateBufferedCoordinates.lean 4 declarations
• AllocatedExternalCandidateNativeMiddleCoordinates.lean 2 declarations
• AllocatedExternalCandidateRefilteredSupportedStep.lean 8 declarations
• AllocatedExternalCandidateSpatialNativeAdaptedConclusion.lean 5 declarations
• AllocatedExternalCandidateSpatialNativeAdaptedPhysicalTerminal.lean 1 declarations
• AllocatedExternalCandidateSpatialNativeAdaptedTerminal.lean 1 declarations
• AllocatedExternalCandidateSpatialNativeAutomaticGeometry.lean 1 declarations
• AllocatedExternalCandidateSpatialNativeAutomaticLongGeometry.lean 26 declarations
• AllocatedExternalCandidateSpatialNativeBudget.lean 49 declarations
• AllocatedExternalCandidateSpatialNativeLongCommonFactors.lean 4 declarations
• AllocatedExternalCandidateSpatialNativeOrdinaryTerminal.lean 4 declarations
• AllocatedExternalCandidateSpatialNativePhysicalConclusion.lean 1 declarations
• AllocatedExternalCandidateSpatialNativeReindex.lean 18 declarations
• AllocatedExternalLocalCandidateOptionQuotientChart.lean 1 declarations
• AllocatedExternalLocalChartKeepBounds.lean 16 declarations
• AllocatedExternalLocalChartOrbitValues.lean 2 declarations
• AllocatedFixedPathLiftSupport.lean 4 declarations
• AllocatedFullSiteSupport.lean 27 declarations
• AllocatedGenuineSpatialReindex.lean 12 declarations
• AllocatedGeometricInputBudget.lean 14 declarations
• AllocatedIdealRowTransport.lean 1 declarations
• AllocatedInactiveNaturalSupport.lean 2 declarations
• AllocatedInactiveSupport.lean 3 declarations
• AllocatedInactiveSupportBudget.lean 20 declarations
• AllocatedJetChartSupport.lean 2 declarations
• AllocatedJetSupportBudget.lean 5 declarations
• AllocatedLayerQuarterSupport.lean 3 declarations
• AllocatedMaskedChartProduct.lean 12 declarations
• AllocatedMixedFixedSupport.lean 3 declarations
• AllocatedNarrowSpatialCanonicalComparison.lean 28 declarations
• AllocatedNaturalAmbientCoordinates.lean 3 declarations
• AllocatedNaturalChartScale.lean 6 declarations
• AllocatedNormalizedSpatialApproximation.lean 2 declarations
• AllocatedOneCubeCoordinates.lean 8 declarations
• AllocatedOriginalBoxInputs.lean 2 declarations
• AllocatedOriginalCoarseBoxSource.lean 1 declarations
• AllocatedPaddedParameterBoxEarlyFreeze.lean 2 declarations
• AllocatedParameterBoxEarlyFreeze.lean 2 declarations
• AllocatedPhysicalChartBounds.lean 8 declarations
• AllocatedPhysicalLongBoxVolume.lean 10 declarations
• AllocatedPositiveSpatialComparison.lean 6 declarations
• AllocatedPrescribedSpatialData.lean 1 declarations
• AllocatedPrescribedSpatialTest.lean 1 declarations
• AllocatedProductChartRadius.lean 11 declarations
• AllocatedProductSiteSupport.lean 2 declarations
• AllocatedProjectedSpatialComparison.lean 5 declarations
• AllocatedProxyOutputSupport.lean 3 declarations
• AllocatedQuotientSupport.lean 5 declarations
• AllocatedRecoveredChartSlow.lean 2 declarations
• AllocatedRecoveredNormalizedTopChart.lean 5 declarations
• AllocatedRecoveredSampleSiteChart.lean 3 declarations
• AllocatedReferenceSpatialRemeshing.lean 9 declarations
• AllocatedRefinedSpatialData.lean 1 declarations
• AllocatedRowSlicedIdealCoordinates.lean 21 declarations
• AllocatedSiteSpatialPrimitiveBudget.lean 10 declarations
• AllocatedSiteTermSupport.lean 4 declarations
• AllocatedSlicedIdealSupport.lean 2 declarations
• AllocatedSlicedOneCubeRowTransport.lean 2 declarations
• AllocatedSlicedRowIdealSupport.lean 9 declarations
• AllocatedSlicedSpatialToCoarse.lean 5 declarations
• AllocatedSlicedSupportedSite.lean 1 declarations
• AllocatedSpatialIdealCoverExpansion.lean 1 declarations
• AllocatedSpatialProxyCap.lean 23 declarations
• AllocatedSpatialTermSupport.lean 5 declarations
• AllocatedSpatialWitnessComparison.lean 2 declarations
• AllocatedSupportedBufferedPhysicalFactorization.lean 9 declarations
• AllocatedSupportedMaskedAmbientFactor.lean 1 declarations
• AllocatedSupportedPhysicalSiteFactorization.lean 2 declarations
• AllocatedSupportedPointBudget.lean 2 declarations
• AllocatedSupportedRecentering.lean 2 declarations
• AllocatedSupportedReference.lean 3 declarations
• AllocatedSupportedSiteApproximation.lean 17 declarations
• AllocatedSupportedSlicedAccurateSource.lean 2 declarations
• AllocatedSupportedSlicedInactiveFixedCap.lean 3 declarations
• AllocatedSupportedSlicedInactiveSource.lean 1 declarations
• AllocatedSupportedSlicedNaturalCap.lean 5 declarations
• AllocatedSupportedSlicedNaturalSiteError.lean 1 declarations
• AllocatedSupportedSlicedPoint.lean 2 declarations
• AllocatedSupportedSlicedUniformPhysicalSource.lean 14 declarations
• AllocatedTestUniformSpatialComparison.lean 1 declarations
• AllocatedWindowMixedSupport.lean 2 declarations
• AllocatedZeroLayerDetectionTransport.lean 2 declarations
• AnisotropicSpatialCapBudget.lean 13 declarations
• AntisymmetricBoxPrecision.lean 2 declarations
• AntisymmetricBoxStepDrop.lean 4 declarations
• AntisymmetricPairCoordinateTest.lean 5 declarations
• AtomSupportBounds.lean 2 declarations
• AuxiliaryBoxPartition.lean 5 declarations
• AveragedIdealSupport.lean 2 declarations
• BinaryWordSupports.lean 5 declarations
• BlockCubeCoordinates.lean 8 declarations
• BoundedBooleanRowTransport.lean 1 declarations
• BoundedCertifiedFullChartMajorIteration.lean 15 declarations
• BoundedDependentCoordinates.lean 3 declarations
• BoundedFullChartGradeMajorMatching.lean 2 declarations
• BoxBlockBudget.lean 26 declarations
• BoxCertificate.lean 2 declarations
• BoxChartCutoff.lean 12 declarations
• BoxCornerMean.lean 43 declarations
• BoxCyclicEncoding.lean 12 declarations
• BoxDetectionExponents.lean 15 declarations
• BoxDifferenceHom.lean 31 declarations
• BoxDifferenceSubstitution.lean 1 declarations
• BoxImageComparison.lean 2 declarations
• BoxNormalizationComparison.lean 3 declarations
• BoxOverlapSize.lean 6 declarations
• BoxPairCorrelation.lean 1 declarations
• BoxPairDivisibility.lean 4 declarations
• BoxTestSmoothing.lean 7 declarations
• BoxWindowAveraging.lean 10 declarations
• BufferedActiveIdealSiteSupport.lean 1 declarations
• BufferedActiveSlicedIdealSiteSupport.lean 1 declarations
• CanonicalScalarFullBoxDiscrepancy.lean 2 declarations
• CanonicalScalarParameterBox.lean 4 declarations
• CanonicalSpatialSupport.lean 8 declarations
• CanonicalSpatialSupportTwo.lean 2 declarations
• CenteredCoefficientDeckChartMeasurable.lean 8 declarations
• CenteredFiniteEventSupport.lean 3 declarations
• CenteredFiniteSpatialModularGoodSet.lean 1 declarations
• CentralOrbitMetric.lean 1 declarations
• CertifiedFullChartBudgetedTreeBounds.lean 41 declarations
• CertifiedFullChartBudgetedTreeBudget.lean 3 declarations
• CertifiedFullChartBudgetedTreeTerminal.lean 2 declarations
• CertifiedFullChartDecompositionSource.lean 13 declarations
• CertifiedFullChartForwardEarlyTree.lean 17 declarations
• CertifiedFullChartFrozenTerminal.lean 19 declarations
• CertifiedFullChartRationalTerminal.lean 1 declarations
• CertifiedFullChartRecoveredTerminal.lean 11 declarations
• ChartCutoff.lean 6 declarations
• ChordBoxCutoff.lean 6 declarations
• CoarseSpatialPartitionBudget.lean 5 declarations
• CoefficientAmbientCoordinates.lean 6 declarations
• CoefficientCoordinateEquiv.lean 3 declarations
• CoefficientDeckChartRecovery.lean 16 declarations
• CoefficientDeckCoordinates.lean 5 declarations
• CoefficientJetChartHaar.lean 1 declarations
• CoefficientJetCoordinates.lean 4 declarations
• CoefficientSquareSpatialBudget.lean 9 declarations
• CommonMarkedDirectionCoordinates.lean 1 declarations
• CommonNativeCoordinateCorrections.lean 10 declarations
• CommonRationalModelCoordinates.lean 2 declarations
• CommonRefilteredFactorsSymbolTransport.lean 16 declarations
• CommonStrideCoordinates.lean 11 declarations
• CommonSupportRadius.lean 5 declarations
• CompactBoxIntegral.lean 2 declarations
• ComparableScalarSliceParameterBox.lean 1 declarations
• ComparisonProductMetric.lean 1 declarations
• ConjugationCoordinates.lean 9 declarations
• ContainedSupportedProgressionReference.lean 4 declarations
• ContinuousOutputBox.lean 8 declarations
• ControlledCoordinateLifts.lean 1 declarations
• ControlledGradedBaseCoordinates.lean 14 declarations
• ControlledIntegralCoordinates.lean 17 declarations
• ControlledLayerOneCoordinates.lean 6 declarations
• ControlledSumCoordinates.lean 4 declarations
• CoordinateConstantDecomposition.lean 19 declarations
• CoordinateCopySum.lean 7 declarations
• CoordinateDerivativeBounds.lean 3 declarations
• CoordinateDeterminant.lean 7 declarations
• CoordinateExceptionUnion.lean 1 declarations
• CoordinateFiberPatch.lean 15 declarations
• CoordinateInjection.lean 6 declarations
• CoordinateLeafCount.lean 21 declarations
• CoordinateMinorCovolume.lean 4 declarations
• CoordinateProductCap.lean 8 declarations
• CoordinateQuotientModel.lean 5 declarations
• CoordinateSubstitutionAlgebra.lean 3 declarations
• CoordinateSupNorm.lean 9 declarations
• CoordinateTreeBatch.lean 1 declarations
• CoordinateTreeCardBudget.lean 1 declarations
• CoordinateTreeOutside.lean 4 declarations
• CoordinateTreeRelabel.lean 5 declarations
• CoordinateTreeTrace.lean 11 declarations
• CoordinatedMatchingScale.lean 4 declarations
• CoordinatewiseLipschitz.lean 2 declarations
• CoveredJetChart.lean 10 declarations
• CubeSignalCoordinates.lean 9 declarations
• CubicBoxFactorizationTransport.lean 1 declarations
• CubicBoxGlobalExpansion.lean 7 declarations
• CubicBoxOrbitFactors.lean 1 declarations
• CubicBoxStepDrop.lean 25 declarations
• CubicCoordinateSlices.lean 4 declarations
• CubicPairCoordinateTest.lean 7 declarations
• CutoffBoxImageComparison.lean 3 declarations
• CyclicProgressionCoordinates.lean 12 declarations
• DenseRealBoxCell.lean 10 declarations
• DependentCoordinateCorrections.lean 2 declarations
• DerivativeVerticalCoordinates.lean 4 declarations
• DetectedTranslationCoordinateBudget.lean 4 declarations
• DetectedTranslationCoordinateZero.lean 5 declarations
• DetectedTranslationLogCoordinates.lean 43 declarations
• DetectedTranslationUniformCoordinateBounds.lean 3 declarations
• DifferenceEventSupport.lean 3 declarations
• DilationPairCoordinates.lean 8 declarations
• DivergenceSupport.lean 7 declarations
• EmbeddingCoordinateHeight.lean 2 declarations
• EmptyCubeCoordinate.lean 2 declarations
• EmptyLayerChartBounds.lean 9 declarations
• Erdos3AllocatedZeroLayerDetectionTransport.lean 2 declarations
• ExplicitMixedUniformBox.lean 2 declarations
• FastCoefficientDerivativeCoordinates.lean 8 declarations
• FilteredSubalgebraCoordinates.lean 4 declarations
• FilteredSymbolMapCoordinates.lean 3 declarations
• FiniteChoiceLeafCoordinates.lean 2 declarations
• FiniteCoordinateSlice.lean 1 declarations
• FiniteGoodSupport.lean 10 declarations
• FiniteImageSupportTransport.lean 3 declarations
• FiniteNormalizedChartCorrection.lean 19 declarations
• FiniteRowChartRadiusBudget.lean 4 declarations
• FiniteSumCoordinate.lean 15 declarations
• FiniteSupportApproximation.lean 1 declarations
• FiniteSupportCutoffTransfer.lean 4 declarations
• FiniteSupportTranslation.lean 2 declarations
• FiniteUniformCoordinateRefresh.lean 4 declarations
• FiniteUnitCoordinate.lean 1 declarations
• FixedCenterBoxDomination.lean 1 declarations
• FixedSpatialEmptyCoordinates.lean 11 declarations
• FixedSpatialNativeAmbientComparison.lean 1 declarations
• FixedSpatialNativeRawSupport.lean 6 declarations
• FixedSpatialSliceNativeAmbientRationalComparison.lean 2 declarations
• FixedSupportRawArray.lean 5 declarations
• FullChartHomogeneousCorrection.lean 29 declarations
• FullFastCoefficientCoordinates.lean 2 declarations
• FullTaggedChartCoefficientRange.lean 32 declarations
• FullTaggedSlowChartCenterDependence.lean 3 declarations
• GeometricLocalizationThreshold.lean 6 declarations
• GeometricRetainedCommonCover.lean 13 declarations
• GeometricSpectralBudgets.lean 4 declarations
• GlobalChartNativeFactorization.lean 27 declarations
• GlobalMarkedChartwiseNormalization.lean 2 declarations
• GlobalMarkedNativeChartResetConditions.lean 8 declarations
• GoodPartSpatialAverage.lean 5 declarations
• GradedTopCoordinates.lean 8 declarations
• HorizontalCoordinateBounds.lean 49 declarations
• HorizontalSeparationTransport.lean 1 declarations
• IdealSiteBoxRadius.lean 3 declarations
• ImageCoordinateDerivative.lean 2 declarations
• IndependentProductTransport.lean 8 declarations
• IndexedComparableScalarParameterBox.lean 6 declarations
• InhomogeneousFullChartLift.lean 13 declarations
• IntervalBoxDifference.lean 11 declarations
• JetAxisCoordinates.lean 4 declarations
• JointExceptionalSpatialWidthBudget.lean 3 declarations
• LayerOneTransportBudget.lean 1 declarations
• LieCoordinateHeight.lean 9 declarations
• LieCoordinateScalarExtension.lean 6 declarations
• LieCoordinateSmooth.lean 6 declarations
• LieStructureTransport.lean 10 declarations
• LieTreeSupport.lean 4 declarations
• LinearMapCoordinateHeight.lean 1 declarations
• LocalCoordinateDivergence.lean 1 declarations
• LowTaggedCoordinateRestriction.lean 23 declarations
• MajorTranslationBaseCoordinates.lean 2 declarations
• MarkedDirectionCoordinates.lean 5 declarations
• MarkedLocalObservableMetric.lean 14 declarations
• MetricOpenCharts.lean 1 declarations
• MinkowskiSecondBox.lean 34 declarations
• MinkowskiSecondBoxGlue.lean 15 declarations
• MissingCoordinateDownsets.lean 6 declarations
• MissingCoordinateErrorAbsorption.lean 1 declarations
• MissingCoordinateProducts.lean 5 declarations
• MixedAntisymmetricBox.lean 2 declarations
• MixedArrayImageSupport.lean 1 declarations
• MixedArraySourceSupport.lean 5 declarations
• MixedBoxFactorizationTransport.lean 1 declarations
• MixedBoxOrbitFactors.lean 1 declarations
• MixedBoxStepDrop.lean 31 declarations
• MixedCoefficientSmallSupport.lean 34 declarations
• MixedCoordinateTransfer.lean 27 declarations
• MixedCoveredChart.lean 7 declarations
• MixedCoveredChartCompact.lean 7 declarations
• MixedEvaluationCoordinates.lean 5 declarations
• MixedPairCoordinateTest.lean 7 declarations
• MixedProfileCoordinates.lean 8 declarations
• MixedRealCoordinates.lean 6 declarations
• MixedReplicatedCoordinates.lean 14 declarations
• MixedShiftCoordinate.lean 3 declarations
• ModerateSliceGeometricApproximation.lean 3 declarations
• MultidegreeCoordinateFreezing.lean 8 declarations
• MultidegreeCoordinateSplit.lean 7 declarations
• MultidegreeOrbitTransport.lean 2 declarations
• MultilinearBoxInverse.lean 6 declarations
• MultilinearCoordinateExpansion.lean 2 declarations
• NarrowSpatialSiteVariation.lean 3 declarations
• NativeChartPairSymbolCompatibility.lean 3 declarations
• NativeChartPartition.lean 1 declarations
• NativeCoordinateDerivativeSystem.lean 2 declarations
• NativeCoordinateErrorReduction.lean 3 declarations
• NativeCoordinateEstimates.lean 20 declarations
• NativeCoordinateFiber.lean 1 declarations
• NativeCoordinatePairs.lean 2 declarations
• NativeCoordinateSplitFreezing.lean 15 declarations
• NativeCorrelationCoordinates.lean 4 declarations
• NativeDilationObservableMetric.lean 2 declarations
• NativeEquivalenceCoordinateMaps.lean 1 declarations
• NativeFiniteSumCoordinate.lean 1 declarations
• NativeIntervalCoordinate.lean 3 declarations
• NativeMixedCoordinateSlices.lean 9 declarations
• NativePairChartSymbol.lean 4 declarations
• NativeProductOrbitMetric.lean 13 declarations
• NativeQuadrupleCoordinates.lean 3 declarations
• NativeSampleSliceChartVerticalPartners.lean 1 declarations
• NativeTernaryCoordinate.lean 23 declarations
• NativeTopQuotientMetric.lean 2 declarations
• NativeTranslatedBoxInverse.lean 4 declarations
• NativeTripleObservableMetric.lean 2 declarations
• NaturalWindowCoordinateBound.lean 1 declarations
• NestedBoxReindex.lean 1 declarations
• NormalizedChartLift.lean 2 declarations
• NormalizedCoordinateCutoff.lean 2 declarations
• NormalizedCoveredChart.lean 5 declarations
• NormalizedMarkedChart.lean 4 declarations
• NormalizedMinorCoordinates.lean 3 declarations
• NormalizedRestrictionTransport.lean 1 declarations
• NormalizedSpatialAmplitudeShift.lean 4 declarations
• NormalizedSpatialChoiceBudget.lean 10 declarations
• NormalizedSpatialReplacement.lean 4 declarations
• NormalizedSupportPlateau.lean 7 declarations
• NormalizedTwistSpatialPartition.lean 14 declarations
• NormalizedTwistUniformBoxHaar.lean 1 declarations
• NormalizedTwistUniformSpatialHaar.lean 1 declarations
• OneCubeSliceSupport.lean 2 declarations
• OneDimensionalBox.lean 5 declarations
• OperatorCoordinateBound.lean 2 declarations
• OptionProductMetric.lean 2 declarations
• OutsideProductTransport.lean 4 declarations
• PMFSupportedMean.lean 2 declarations
• PartitionedIdealSupport.lean 4 declarations
• PhysicalActiveProfileRelativeSupport.lean 2 declarations
• PhysicalBoxControl.lean 11 declarations
• PhysicalBoxPartition.lean 16 declarations
• PhysicalChartRadiusBudget.lean 4 declarations
• PhysicalFactorCoordinates.lean 2 declarations
• PhysicalNormalizedSpatialFactor.lean 6 declarations
• PhysicalRowChartMatching.lean 1 declarations
• PhysicalRowsStandardCoordinates.lean 5 declarations
• PhysicalSpatialAnalyticFactor.lean 3 declarations
• PhysicalSpatialScales.lean 36 declarations
• PhysicalSupportedCubes.lean 9 declarations
• PivotCoordinateChange.lean 8 declarations
• PolarizedCoefficientCoordinates.lean 3 declarations
• PositiveCyclicCoordinateProduct.lean 5 declarations
• PreparedBadProductSpatialBudget.lean 1 declarations
• PreparedDeterminingCoordinates.lean 11 declarations
• PreparedEarlySpatialWidth.lean 1 declarations
• PreparedFullChartNativeDetection.lean 10 declarations
• PreparedGeometryDecidableTransport.lean 2 declarations
• PreparedModularCanonicalDetectorFullBoxConsumer.lean 2 declarations
• PreparedModularCanonicalDetectorFullBoxConsumerGeneral.lean 2 declarations
• PreparedModularCanonicalDetectorGeometricBounds.lean 14 declarations
• PreparedModularCanonicalDetectorGeometricBoundsGeneral.lean 14 declarations
• PreparedModularCanonicalDetectorSpatialBounds.lean 3 declarations
• PreparedModularGeneralDetectorFreeSpatialBounds.lean 3 declarations
• PreparedModularGeneralProductivityFreeSpatialBounds.lean 1 declarations
• PreparedScalarSpatialWidthPower.lean 1 declarations
• PreparedSpatialWitnessWidth.lean 4 declarations
• PrincipalCoefficientPositiveSupport.lean 2 declarations
• PrincipalCoordinatePartition.lean 2 declarations
• PrincipalCubeSupportedCell.lean 12 declarations
• PrincipalSpatialJointTest.lean 1 declarations
• PrincipalSpatialL1Comparison.lean 1 declarations
• PrincipalSpatialMixedComparison.lean 1 declarations
• PrincipalSpatialSiteComparison.lean 17 declarations
• PrincipalSpatialTestComparison.lean 1 declarations
• ProductChartReference.lean 2 declarations
• ProductComponentCoordinates.lean 2 declarations
• ProductEquivTransport.lean 12 declarations
• ProductEuclideanCoordinates.lean 6 declarations
• ProductMarginalSupport.lean 1 declarations
• ProductSectionSupport.lean 10 declarations
• ProductTupleSupport.lean 2 declarations
• ProgressionCoordinateResampling.lean 7 declarations
• ProgressionEndpointUnitBox.lean 1 declarations
• ProgressionGeometricApproximation.lean 1 declarations
• ProgressionTupleSliceSupport.lean 6 declarations
• QuadraticAntisymmetricBox.lean 1 declarations
• QuadraticBoxExpansion.lean 1 declarations
• QuadraticLocalBox.lean 2 declarations
• QuantitativeMetricPartition.lean 28 declarations
• QuantitativeProjectedChart.lean 9 declarations
• QuarticAntisymmetricBox.lean 2 declarations
• QuarticBoxFactorizationTransport.lean 3 declarations
• QuarticBoxGlobalExpansion.lean 4 declarations
• QuarticBoxOrbitFactors.lean 1 declarations
• QuarticBoxStepDrop.lean 29 declarations
• QuarticCoordinateSlices.lean 3 declarations
• QuarticPairCoordinateTest.lean 7 declarations
• QuotientCoordinateRadius.lean 8 declarations
• QuotientSubgroupCoordinates.lean 1 declarations
• RationalModelCoordinates.lean 6 declarations
• RealChartReindexCoefficients.lean 3 declarations
• RealCoordinateFunctionals.lean 7 declarations
• RealFastCoefficientCoordinates.lean 27 declarations
• RealOrderedChartPatch.lean 1 declarations
• RealPolarizedCoefficientCoordinates.lean 3 declarations
• RealSquarefreeCoordinates.lean 4 declarations
• RealSubspaceCoordinateRetraction.lean 38 declarations
• RealSupportedQuotientCoordinates.lean 1 declarations
• RealifiedPairCoordinates.lean 5 declarations
• RealifiedSquareCoordinates.lean 5 declarations
• RealifiedSquareMetric.lean 1 declarations
• RealifiedTripleCoordinates.lean 17 declarations
• ReducedSquareCoefficientCoordinates.lean 5 declarations
• RelativePatchBoxRestriction.lean 8 declarations
• RelativePatchFiniteCoordinateReduction.lean 14 declarations
• RelativePatchStageTransport.lean 6 declarations
• RelativePatchWholeBoxConclusion.lean 8 declarations
• RepresentativeWindowTransport.lean 6 declarations
• RestrictedChartPrefixControl.lean 24 declarations
• RestrictedChartReindex.lean 1 declarations
• RestrictedComplexChartSupport.lean 3 declarations
• RestrictedGradeScalarCoordinates.lean 3 declarations
• RiemannianLocalCoordinates.lean 4 declarations
• RightCosetMetricMap.lean 16 declarations
• RoundedGraphCyclicCoordinates.lean 3 declarations
• SampledCommonBox.lean 14 declarations
• SampledDenseCommonBox.lean 2 declarations
• ScalarBoxGeometry.lean 2 declarations
• ScalarCubeCoordinates.lean 7 declarations
• ScalarCubeProductSupport.lean 11 declarations
• ScalarReferenceNativeDetectionCoordinateEquiv.lean 29 declarations
• ScalarSpatialScaleBounds.lean 12 declarations
• ScalarSupportTranslationL1.lean 2 declarations
• SelectedCenteredJointSupport.lean 2 declarations
• SelectedJointSpatialCutoff.lean 1 declarations
• SeparatedChartExtension.lean 2 declarations
• SharedWidthAllocatedCanonicalSpatialNativeSource.lean 4 declarations
• SharedWidthAllocatedDetectedSpatialNativeSourceGeneral.lean 4 declarations
• SharedWidthPreparedFullChartNativeDetection.lean 1 declarations
• ShiftedBoxSites.lean 3 declarations
• SigmaAxisCoordinates.lean 9 declarations
• SignedSplitCoordinates.lean 4 declarations
• SmallBoxCutoff.lean 7 declarations
• SmallDifferenceGraphCoordinates.lean 3 declarations
• SmoothSpatialCostBudget.lean 23 declarations
• SmoothSpatialSiteExpansion.lean 1 declarations
• SortedLayerCoordinateEnumeration.lean 7 declarations
• SparseCoordinateCorrections.lean 1 declarations
• SpatialChoiceEnvelope.lean 60 declarations
• SpatialNumericEnvelopeFunctoriality.lean 47 declarations
• SpatialOutputChoice.lean 3 declarations
• SpatialPivotNormalization.lean 13 declarations
• SpatialShiftedWindowError.lean 23 declarations
• SpatialSiteNativePartner.lean 3 declarations
• SpatialSiteShift.lean 31 declarations
• SpatialStarCoordinates.lean 9 declarations
• SpatialTupleErrorBudget.lean 9 declarations
• SpatialTwoBlockEquiv.lean 8 declarations
• SplitFreeCoordinates.lean 5 declarations
• SquareQuotientHeightTransport.lean 5 declarations
• SquareRecoveryCoordinates.lean 6 declarations
• SquarefreeActionMetric.lean 4 declarations
• SquarefreeAlgebraCoordinates.lean 7 declarations
• SquarefreeSupportPermutation.lean 8 declarations
• StepOneCoordinateMetric.lean 4 declarations
• SublatticeOrbitMetric.lean 1 declarations
• SubmoduleCoordinateHeight.lean 1 declarations
• SubmoduleQuotientCoordinates.lean 5 declarations
• SupportCutoffSplit.lean 2 declarations
• SupportMaskComplexMean.lean 3 declarations
• SupportPairingAggregation.lean 1 declarations
• SupportedBoxLipschitz.lean 1 declarations
• SupportedComplexSelection.lean 3 declarations
• SupportedCorrelationPairs.lean 1 declarations
• SupportedCubeEquivTransport.lean 66 declarations
• SupportedCubeUnitBounds.lean 3 declarations
• SupportedFiberApproximation.lean 6 declarations
• SupportedFiberFiniteMeanError.lean 3 declarations
• SupportedFiniteComparison.lean 3 declarations
• SupportedLieQuotient.lean 3 declarations
• SupportedMeanBounds.lean 2 declarations
• SupportedQuotientFamilyFaithful.lean 2 declarations
• SupportedQuotientSection.lean 10 declarations
• SupportedSubquotient.lean 1 declarations
• SupportedTriangularSum.lean 2 declarations
• SymbolCoordinateFreezeBounds.lean 6 declarations
• SymbolFactorizationTransport.lean 3 declarations
• SymbolRepresentativeTransport.lean 3 declarations
• SymmetricEvaluationMetric.lean 2 declarations
• TerminalChartSlowEvaluation.lean 32 declarations
• TopSupportSubstitution.lean 5 declarations
• TranslationCoordinateBudget.lean 1 declarations
• TranslationLogCoordinateHomogeneous.lean 2 declarations
• TranslationLogCoordinateInputBounds.lean 7 declarations
• TranslationLogCoordinateScaling.lean 7 declarations
• TranslationShearCoordinateSeries.lean 18 declarations
• TripleBoxAnchorApproximation.lean 9 declarations
• TwoBoxSmoothingComplex.lean 13 declarations
• UnconditionedCommonSideSupport.lean 3 declarations
• UnconditionedJointReferenceSupport.lean 2 declarations
• UnconditionedSpatialWidthBudget.lean 46 declarations
• UniformCoordinatePartition.lean 2 declarations
• UniformDependentSubtypeCoordinates.lean 3 declarations
• UniformDependentSumCoordinates.lean 4 declarations
• UniformSumCoordinates.lean 4 declarations
• UnitBoxAmplitude.lean 14 declarations
• UnitBoxInteriorCutoff.lean 21 declarations
• UnitIntervalBox.lean 3 declarations
• VariableRoundedGraphCoordinates.lean 3 declarations
• VectorSpatialPartitionBudget.lean 2 declarations
• WeightedBlockSupportScale.lean 4 declarations
• WeightedCoordinateExtraction.lean 5 declarations
• WeightedSubstitutionSupport.lean 1 declarations
• WeightedSupportDropRename.lean 12 declarations
• WeightedTranslationBufferedCoordinates.lean 14 declarations
• WeightedTranslationIntegralCoordinates.lean 7 declarations