`OAI/GroupTheory/PolycyclicRecognition/Geometry/`

2888 declarations, 0 contain sorry, 0 declared as axioms; 1047 files

Files

AbelianFiniteRankRootCore.lean 1 declarations
AbelianLieModel.lean 4 declarations
AbelianRootGenerators.lean 3 declarations
ActualRotationLieAlgebra.lean 5 declarations
ActualRotationalModification.lean 9 declarations
ActualSmoothRotation.lean 9 declarations
AdjointDeterminant.lean 1 declarations
AdjointExponentialRepresentation.lean 4 declarations
AdjointMatrixHeight.lean 8 declarations
AffineProfileBoundary.lean 3 declarations
AlgebraExponential.lean 7 declarations
AlgebraExponentialNaturality.lean 1 declarations
AlgebraHomLieDifferential.lean 6 declarations
AlgebraRepresentationDerivative.lean 1 declarations
AlgebraTangentLie.lean 2 declarations
AnalyticDerivationAction.lean 4 declarations
AnalyticDerivationFlow.lean 7 declarations
AnalyticInverseChart.lean 1 declarations
AnalyticNilpotentExponential.lean 2 declarations
AnalyticNilpotentLogarithm.lean 2 declarations
AnalyticRepresentationAtlas.lean 8 declarations
AnalyticRepresentationGroup.lean 5 declarations
AnalyticTriangularRealization.lean 2 declarations
AutomaticSmoothAlgebraHom.lean 3 declarations
BasisAdjointNilpotent.lean 1 declarations
BasisDerivativeField.lean 2 declarations
BilinearCentralLieModel.lean 4 declarations
BoundaryAveragedTrace.lean 1 declarations
BoundaryCompactSandwich.lean 2 declarations
BoundaryFamilyHomeomorphism.lean 1 declarations
BoundaryFamilyMass.lean 1 declarations
BoundaryFromLogProducts.lean 2 declarations
BoundaryGeneratorActionBounds.lean 1 declarations
BoundaryGeneratorHeight.lean 1 declarations
BoundaryHeight.lean 7 declarations
BoundaryImageMass.lean 2 declarations
BoundaryInverseShadow.lean 4 declarations
BoundaryLeaf.lean 4 declarations
BoundaryLimits.lean 5 declarations
BoundaryMapFamily.lean 1 declarations
BoundaryMass.lean 1 declarations
BoundaryPublishedMetricAveraging.lean 1 declarations
BoundaryRaySeparation.lean 3 declarations
BoundaryShadowDescent.lean 1 declarations
BoundaryTranslateMass.lean 3 declarations
BoundaryVolumeAveraging.lean 1 declarations
BoundaryVolumeComparison.lean 1 declarations
BoundaryVolumeTrace.lean 1 declarations
BoundedAssociativeBCH.lean 4 declarations
BoundedCenteredHeight.lean 1 declarations
BoundedDegreeRootsOfUnity.lean 2 declarations
CanonicalExponentialMeasure.lean 2 declarations
CanonicalHeight.lean 12 declarations
CanonicalHeightContractionModel.lean 1 declarations
CanonicalHeightFromRepresentation.lean 2 declarations
CanonicalHeightIntegration.lean 3 declarations
CanonicalHeightMetricChoice.lean 1 declarations
CanonicalHeightMetricModel.lean 1 declarations
CanonicalHeightMinimizingModel.lean 1 declarations
CanonicalHeightRepresentationModel.lean 1 declarations
CartanAccessibleComparison.lean 1 declarations
CartanActionCoefficients.lean 1 declarations
CartanActualChainConcentration.lean 1 declarations
CartanActualConjugation.lean 4 declarations
CartanActualProbeProfiles.lean 7 declarations
CartanActualScaleComparison.lean 1 declarations
CartanAdjointAction.lean 5 declarations
CartanAllowedProbeChains.lean 2 declarations
CartanAllowedProfileCompactness.lean 1 declarations
CartanAlternatingComparison.lean 1 declarations
CartanAlternatingLimit.lean 1 declarations
CartanAlternatingSchemes.lean 2 declarations
CartanAmbientPacking.lean 1 declarations
CartanAmbientWords.lean 2 declarations
CartanBasepointAffineComparison.lean 2 declarations
CartanBasepointBoxes.lean 2 declarations
CartanBasepointCellDomination.lean 1 declarations
CartanBasepointConcentration.lean 1 declarations
CartanBasepointFactorCover.lean 1 declarations
CartanBasepointGeometryOfBounds.lean 1 declarations
CartanBasepointProfileIdentity.lean 2 declarations
CartanBasisComparison.lean 1 declarations
CartanBoundaryAveraging.lean 1 declarations
CartanBoundaryBoundedHeight.lean 2 declarations
CartanBoundaryContinuity.lean 1 declarations
CartanBoundaryFamilyShadow.lean 1 declarations
CartanBoundaryGeneratorAction.lean 1 declarations
CartanBoundaryHaarAction.lean 1 declarations
CartanBoundaryInverse.lean 1 declarations
CartanBoundaryLeaf.lean 1 declarations
CartanBoundaryLeafComparison.lean 1 declarations
CartanBoundaryLeafTemplate.lean 1 declarations
CartanBoundaryOrbitFibers.lean 1 declarations
CartanBoundaryRayMatching.lean 2 declarations
CartanBoundaryRetainedRay.lean 2 declarations
CartanBoundaryShadow.lean 1 declarations
CartanBoundaryTopology.lean 1 declarations
CartanBoundedHeightEndgame.lean 1 declarations
CartanBoundedTemplatePaths.lean 3 declarations
CartanBoxDilation.lean 7 declarations
CartanBoxExponents.lean 7 declarations
CartanBoxIncrementConcentration.lean 1 declarations
CartanBoxMaps.lean 7 declarations
CartanBoxPaths.lean 1 declarations
CartanBoxProbeChains.lean 4 declarations
CartanBoxRadiusProbability.lean 1 declarations
CartanBoxScaling.lean 5 declarations
CartanBoxSchemes.lean 2 declarations
CartanBridgeAbsorption.lean 1 declarations
CartanBridgeGeometry.lean 1 declarations
CartanCanonicalPolarSamplers.lean 1 declarations
CartanCanonicalProfiles.lean 3 declarations
CartanCellPairLaws.lean 1 declarations
CartanCellProbability.lean 2 declarations
CartanCellProfileAffinity.lean 1 declarations
CartanCellProfileComparison.lean 1 declarations
CartanCellProfileConcentration.lean 1 declarations
CartanCellTransport.lean 3 declarations
CartanChainCompactProfiles.lean 1 declarations
CartanChartAction.lean 1 declarations
CartanChartSlack.lean 1 declarations
CartanChartSlackRealization.lean 1 declarations
CartanChosenSamplingHeight.lean 1 declarations
CartanCocycleRestriction.lean 2 declarations
CartanCocycleWordGrowth.lean 2 declarations
CartanCocycleWords.lean 3 declarations
CartanCommonBundlePaths.lean 1 declarations
CartanCommonCellAffinity.lean 1 declarations
CartanCompactProbeBridge.lean 1 declarations
CartanCompactSupportSlack.lean 1 declarations
CartanCompactTemplatePaths.lean 1 declarations
CartanCompactWords.lean 2 declarations
CartanComparisonSchemes.lean 1 declarations
CartanConcentratedFrames.lean 1 declarations
CartanConcentratedPaths.lean 1 declarations
CartanConcentratedProbeSelection.lean 1 declarations
CartanConcentratedRootFrames.lean 1 declarations
CartanConeAction.lean 4 declarations
CartanConeAmbientAction.lean 1 declarations
CartanConeGroup.lean 4 declarations
CartanConeHaarAction.lean 2 declarations
CartanConeIdeal.lean 6 declarations
CartanConeIdealExponent.lean 2 declarations
CartanConeInvariance.lean 4 declarations
CartanConeTrace.lean 5 declarations
CartanConjugationBounds.lean 3 declarations
CartanConjugationHeightBound.lean 3 declarations
CartanContactProbeBridge.lean 1 declarations
CartanContactStepBridge.lean 1 declarations
CartanContinuousRayLimits.lean 1 declarations
CartanContractedRoots.lean 2 declarations
CartanControlledAction.lean 5 declarations
CartanControlledFolner.lean 1 declarations
CartanControlledProducts.lean 2 declarations
CartanCoordinatePacking.lean 1 declarations
CartanCoupledProfileComparison.lean 1 declarations
CartanCoupledRecurrenceCells.lean 1 declarations
CartanCoupledSourceImage.lean 1 declarations
CartanCoupledTargetTuples.lean 1 declarations
CartanCoverBoxRadius.lean 2 declarations
CartanCoverGeometry.lean 2 declarations
CartanCoverMetricProducts.lean 1 declarations
CartanCoverRootDistortion.lean 2 declarations
CartanCoverWordBoxes.lean 2 declarations
CartanDMetric.lean 2 declarations
CartanDProfiles.lean 1 declarations
CartanDecomposition.lean 5 declarations
CartanDensityOccupation.lean 1 declarations
CartanDependentProfileCompactness.lean 1 declarations
CartanDiagonalNeighborLabels.lean 1 declarations
CartanDilatedLinkedChains.lean 1 declarations
CartanDilatedProbeChains.lean 1 declarations
CartanDirectionalVisits.lean 2 declarations
CartanDominatedGeneratorChain.lean 1 declarations
CartanErgodicIncrement.lean 1 declarations
CartanErgodicLabel.lean 1 declarations
CartanErgodicTemplateIncrement.lean 1 declarations
CartanErgodicTemplateLabel.lean 1 declarations
CartanEventualNeighborLabels.lean 1 declarations
CartanFacetProfileAgreement.lean 1 declarations
CartanFacetSupportedAgreement.lean 2 declarations
CartanFactorAsymptotics.lean 1 declarations
CartanFactorCharts.lean 2 declarations
CartanFactorHaarInvariance.lean 2 declarations
CartanFactorHeight.lean 3 declarations
CartanFactorLogVolume.lean 1 declarations
CartanFactorModel.lean 2 declarations
CartanFactorRepresentation.lean 2 declarations
CartanFactorization.lean 1 declarations
CartanFixedPolarTargets.lean 1 declarations
CartanFixedProbeBridge.lean 1 declarations
CartanFixedProfileMeasurable.lean 1 declarations
CartanFixedSamplingGeometry.lean 2 declarations
CartanFixedSlicePacking.lean 1 declarations
CartanFixedTiledProbeChains.lean 3 declarations
CartanFullCellAffinity.lean 1 declarations
CartanGeneratorChain.lean 1 declarations
CartanGeneratorPrefixes.lean 1 declarations
CartanGeneratorSchemes.lean 2 declarations
CartanGeneratorSequence.lean 1 declarations
CartanGenerators.lean 6 declarations
CartanGlobalGeneratorWords.lean 2 declarations
CartanGoodCellLegs.lean 1 declarations
CartanGoodFacetAgreement.lean 1 declarations
CartanGoodRootNeighborLabels.lean 1 declarations
CartanGoodTemplateComparison.lean 1 declarations
CartanGoodWordPaths.lean 1 declarations
CartanGradedGeometry.lean 2 declarations
CartanGroupBoxes.lean 6 declarations
CartanGroupConjugation.lean 3 declarations
CartanHaarConjugation.lean 2 declarations
CartanHeightPublishedAssembly.lean 1 declarations
CartanHeightRays.lean 5 declarations
CartanHomKernel.lean 3 declarations
CartanHomLinear.lean 1 declarations
CartanIdealFiberAsymptotics.lean 1 declarations
CartanIdenticalNeighborProfiles.lean 1 declarations
CartanIndependentBoxConcentration.lean 1 declarations
CartanIndependentChainConcentration.lean 1 declarations
CartanIntegratedAction.lean 1 declarations
CartanInteriorNeighbor.lean 1 declarations
CartanInteriorProfileHeights.lean 1 declarations
CartanInteriorSwitch.lean 2 declarations
CartanIntervalDenominator.lean 1 declarations
CartanIntervalVisits.lean 2 declarations
CartanIntrinsicBridge.lean 1 declarations
CartanInverseCoefficients.lean 1 declarations
CartanInverseSections.lean 1 declarations
CartanJacobian.lean 6 declarations
CartanJordanDecomposition.lean 3 declarations
CartanKernelRegionVolume.lean 1 declarations
CartanLeafHeight.lean 1 declarations
CartanLiftMultiplicity.lean 1 declarations
CartanLinkedChainConcentration.lean 1 declarations
CartanLinkedNeighborBoxes.lean 1 declarations
CartanLinkedProbeChains.lean 4 declarations
CartanLinkedProbePaths.lean 1 declarations
CartanLinkedProfileSelection.lean 1 declarations
CartanLocalProduct.lean 4 declarations
CartanLogRegionVolume.lean 1 declarations
CartanMappedTemplatePaths.lean 1 declarations
CartanMeanFactorization.lean 1 declarations
CartanMeasurableBoxChains.lean 1 declarations
CartanMeasurableGeneratorChains.lean 1 declarations
CartanMeasurableTemplateCoding.lean 1 declarations
CartanMeasuredCone.lean 4 declarations
CartanMeasuredConeCells.lean 2 declarations
CartanMeasuredConeHaar.lean 5 declarations
CartanMeasuredConeRealization.lean 1 declarations
CartanMeasuredProbeRegions.lean 1 declarations
CartanMeasuredRegionsFromLifts.lean 1 declarations
CartanMetricBasepointComparison.lean 1 declarations
CartanMetricBasepointGeometry.lean 1 declarations
CartanMetricBasepointSampling.lean 1 declarations
CartanMetricChartShift.lean 1 declarations
CartanMetricLogChartShift.lean 1 declarations
CartanMixedScaleBoxes.lean 4 declarations
CartanModel.lean 7 declarations
CartanMultiplication.lean 9 declarations
CartanNLogMetric.lean 1 declarations
CartanNMetric.lean 4 declarations
CartanNegativeChainAsymptotics.lean 1 declarations
CartanNeighborBoxAffinity.lean 1 declarations
CartanNeighborChainConcentration.lean 1 declarations
CartanNeighborCompactProfiles.lean 1 declarations
CartanNeighborConcentration.lean 1 declarations
CartanNeighborFrameLaw.lean 1 declarations
CartanNeighborLawCompactness.lean 1 declarations
CartanNeighborProfileAffinity.lean 1 declarations
CartanNeighborRateBridge.lean 1 declarations
CartanNeighborRowBasis.lean 2 declarations
CartanNeighborRowChart.lean 2 declarations
CartanNeighborRowOffset.lean 1 declarations
CartanNeighborRowOffsetsEqual.lean 2 declarations
CartanNeighborRowProfile.lean 3 declarations
CartanNeighborRowReverse.lean 1 declarations
CartanNeighborSamplingReindex.lean 1 declarations
CartanNeighborSamplingRow.lean 2 declarations
CartanNeighborSuffixRate.lean 1 declarations
CartanNontrivialHeight.lean 2 declarations
CartanNormalOccupation.lean 1 declarations
CartanNormalizedBoundedHeight.lean 1 declarations
CartanNormalizedNeighborStep.lean 3 declarations
CartanNormalizedPolarSamplers.lean 1 declarations
CartanOccupationInvariance.lean 1 declarations
CartanOffsetThreshold.lean 2 declarations
CartanOneConeThreshold.lean 1 declarations
CartanOrdinaryBoxCover.lean 2 declarations
CartanOrdinaryMetricBound.lean 1 declarations
CartanOriginalNeighborFrames.lean 1 declarations
CartanOriginalNeighborOffset.lean 1 declarations
CartanOriginalStepBridge.lean 1 declarations
CartanOverlapBound.lean 1 declarations
CartanOverlapCoordinates.lean 2 declarations
CartanPairMean.lean 1 declarations
CartanPathAlternatingComparison.lean 1 declarations
CartanPathLifts.lean 1 declarations
CartanPathPacking.lean 1 declarations
CartanPathQuotientRestriction.lean 1 declarations
CartanPathTupleLifts.lean 1 declarations
CartanPerturbedBox.lean 2 declarations
CartanPivotCancellation.lean 3 declarations
CartanPivotCoordinateBound.lean 2 declarations
CartanPivotProbePaths.lean 1 declarations
CartanPivotSupportSwitch.lean 1 declarations
CartanPivotTemplateCoding.lean 1 declarations
CartanPivotVisits.lean 1 declarations
CartanPivotWordImage.lean 1 declarations
CartanPivotWordPath.lean 5 declarations
CartanPolarBoxOffset.lean 1 declarations
CartanPolarConeAction.lean 4 declarations
CartanPolarConeKernel.lean 10 declarations
CartanPolarConeModels.lean 4 declarations
CartanPolarFixedSection.lean 2 declarations
CartanPolarFlowTiling.lean 1 declarations
CartanPolarLinkedSource.lean 1 declarations
CartanPolarMeasuredOffset.lean 1 declarations
CartanPolarOffsetExponents.lean 3 declarations
CartanPolarOriginalOffset.lean 1 declarations
CartanPolarProbeTemplates.lean 9 declarations
CartanPolarRegionMeasure.lean 2 declarations
CartanPolarSamplingGeometry.lean 1 declarations
CartanPolarSourceBounds.lean 1 declarations
CartanPolarSourceCells.lean 1 declarations
CartanPolarSourceFrames.lean 3 declarations
CartanPolarSourceFramesCanonical.lean 1 declarations
CartanPolarSourceProbability.lean 1 declarations
CartanPolarSourceVolumes.lean 2 declarations
CartanPolarTiledChains.lean 2 declarations
CartanPolarTiledSamplers.lean 3 declarations
CartanPolynomialBoxWords.lean 1 declarations
CartanProbeBridgeLength.lean 2 declarations
CartanProbeChainDilation.lean 3 declarations
CartanProbeChainSequence.lean 1 declarations
CartanProbeCoordinateRegions.lean 1 declarations
CartanProbeInteriorHeights.lean 1 declarations
CartanProductCoordinates.lean 2 declarations
CartanProfileAffinity.lean 1 declarations
CartanProfileAnchors.lean 1 declarations
CartanProfileBridgeRestriction.lean 2 declarations
CartanProfileChainConcentration.lean 1 declarations
CartanProfileCompactness.lean 1 declarations
CartanProfileConcentration.lean 2 declarations
CartanProfileEndpointLifts.lean 1 declarations
CartanProfileIncrement.lean 1 declarations
CartanProfilePacking.lean 1 declarations
CartanProfilePivot.lean 1 declarations
CartanProfileQuotientRestriction.lean 1 declarations
CartanProfileSegmentVolume.lean 1 declarations
CartanProfileTemplateIncrement.lean 1 declarations
CartanPublishedAffineMean.lean 1 declarations
CartanPublishedAllowedChains.lean 1 declarations
CartanPublishedBasepointComparison.lean 1 declarations
CartanPublishedBoundedHeight.lean 1 declarations
CartanPublishedChainConcentration.lean 1 declarations
CartanPublishedHeightSelection.lean 1 declarations
CartanPublishedMixedScaleConcentration.lean 1 declarations
CartanPublishedNeighborConcentration.lean 1 declarations
CartanPublishedOffsetThreshold.lean 1 declarations
CartanPublishedOrdinaryConcentration.lean 1 declarations
CartanPublishedPolarAction.lean 1 declarations
CartanPublishedPolarRegions.lean 3 declarations
CartanPublishedProfileEstimates.lean 1 declarations
CartanPublishedRawChain.lean 1 declarations
CartanPublishedScaleStabilization.lean 1 declarations
CartanPublishedSublinearHeight.lean 1 declarations
CartanPublishedSuffixConcentration.lean 1 declarations
CartanPublishedUniformScale.lean 1 declarations
CartanRawChainConcentration.lean 1 declarations
CartanRayActionTopology.lean 2 declarations
CartanRayBoundaryComparison.lean 2 declarations
CartanRayBoundaryFamily.lean 1 declarations
CartanRayBoundaryHaar.lean 1 declarations
CartanRayBoundaryHomeomorphism.lean 1 declarations
CartanRayBoundaryInverse.lean 1 declarations
CartanRayBoundaryMass.lean 1 declarations
CartanRayBoundaryModel.lean 9 declarations
CartanRayCompactCollapse.lean 1 declarations
CartanRayCompactLimits.lean 1 declarations
CartanRayFactorContraction.lean 3 declarations
CartanRayFactorPaths.lean 1 declarations
CartanRayFiberPaths.lean 3 declarations
CartanRayTrace.lean 1 declarations
CartanRealDiagonal.lean 4 declarations
CartanRealShadow.lean 6 declarations
CartanRealShadowSolvable.lean 4 declarations
CartanRecurrenceBoxes.lean 1 declarations
CartanRecurrenceCells.lean 1 declarations
CartanRecurrentProfilePacking.lean 1 declarations
CartanRepresentationDescent.lean 1 declarations
CartanResidualAction.lean 5 declarations
CartanResidualBounds.lean 5 declarations
CartanResidualDerivation.lean 17 declarations
CartanResidualExponential.lean 3 declarations
CartanRestrictedNeighborLaw.lean 1 declarations
CartanReverseNeighborLaw.lean 5 declarations
CartanRootBoxes.lean 2 declarations
CartanRootCocycle.lean 1 declarations
CartanRootIntervalSlack.lean 1 declarations
CartanRootNeighborLabels.lean 1 declarations
CartanRootWidths.lean 7 declarations
CartanSampledBridge.lean 2 declarations
CartanSampledProbeFrames.lean 5 declarations
CartanSampledVisits.lean 3 declarations
CartanSamplingFacet.lean 2 declarations
CartanSamplingNonzero.lean 1 declarations
CartanSamplingParameters.lean 11 declarations
CartanScaleTransition.lean 3 declarations
CartanSectionProbeBox.lean 2 declarations
CartanSegmentCellPacking.lean 1 declarations
CartanSegmentCoding.lean 1 declarations
CartanSegmentExponent.lean 2 declarations
CartanSegmentPaths.lean 1 declarations
CartanSegmentSupportTimes.lean 1 declarations
CartanSegmentVisits.lean 6 declarations
CartanSegmentWordPath.lean 4 declarations
CartanSelectedProbePaths.lean 2 declarations
CartanSelectedProfilePaths.lean 1 declarations
CartanSemidirectCover.lean 7 declarations
CartanSemidirectWords.lean 2 declarations
CartanSeparatedAlternatingComparison.lean 4 declarations
CartanSeparatedTuples.lean 1 declarations
CartanSheetAgreement.lean 2 declarations
CartanShrinkingBoxEnvelope.lean 1 declarations
CartanSmallHeight.lean 3 declarations
CartanSmallMetricFactors.lean 1 declarations
CartanSmallWordFactors.lean 1 declarations
CartanSourceBundleTerminals.lean 1 declarations
CartanSourceDilation.lean 6 declarations
CartanSourceDilationUniqueness.lean 1 declarations
CartanSourceIntervals.lean 1 declarations
CartanSourceOffsetComparison.lean 1 declarations
CartanSourceProfile.lean 2 declarations
CartanSourceSectionCoordinates.lean 2 declarations
CartanSourceTargetComparison.lean 1 declarations
CartanSourceTerminalCover.lean 1 declarations
CartanSourceTuplePacking.lean 1 declarations
CartanStationaryComparison.lean 1 declarations
CartanStationaryFactor.lean 1 declarations
CartanStationaryIncrement.lean 1 declarations
CartanStationaryLabel.lean 1 declarations
CartanStationaryPacking.lean 1 declarations
CartanStationaryPaths.lean 1 declarations
CartanStationaryTemplateComparison.lean 1 declarations
CartanStationaryTemplateFactor.lean 1 declarations
CartanStationaryTemplateIncrement.lean 1 declarations
CartanStationaryTemplateLabel.lean 1 declarations
CartanStationaryTemplatePacking.lean 1 declarations
CartanStationaryTemplatePaths.lean 1 declarations
CartanSubexponentialGroupChain.lean 1 declarations
CartanSubexponentialSuffixSequence.lean 1 declarations
CartanSubgroupRealization.lean 4 declarations
CartanSublinearBoundedHeight.lean 1 declarations
CartanSublinearRayComparison.lean 1 declarations
CartanSuccessfulBundlePaths.lean 1 declarations
CartanSuffixGeneratorSequence.lean 1 declarations
CartanSupportData.lean 2 declarations
CartanSupportLegs.lean 4 declarations
CartanSupportPositions.lean 1 declarations
CartanSupportSwitch.lean 1 declarations
CartanSupportVisits.lean 1 declarations
CartanSupportedCellAgreement.lean 1 declarations
CartanSupportedCellLipschitz.lean 1 declarations
CartanSupportedNeighborProfiles.lean 1 declarations
CartanSupportedTemplateComparison.lean 1 declarations
CartanTangentConjugation.lean 1 declarations
CartanTargetBundlePaths.lean 1 declarations
CartanTemplateCoding.lean 1 declarations
CartanTemplateProfilePaths.lean 1 declarations
CartanTemplateSections.lean 1 declarations
CartanTemplateSupports.lean 1 declarations
CartanTemplateVisits.lean 2 declarations
CartanTemplateWordPath.lean 6 declarations
CartanTerminalComparison.lean 1 declarations
CartanTerminalCorrections.lean 1 declarations
CartanThreeTemplatePaths.lean 1 declarations
CartanTiledLinkedEndpoints.lean 1 declarations
CartanTiledOffsetRates.lean 1 declarations
CartanTiledProbeBoxes.lean 3 declarations
CartanTiledProbeChains.lean 3 declarations
CartanTiledProbeEndpoints.lean 1 declarations
CartanTiledSourceBridge.lean 1 declarations
CartanTiledSourceCell.lean 10 declarations
CartanTiledSourceChains.lean 1 declarations
CartanTiledSourceEndpoints.lean 1 declarations
CartanTrace.lean 2 declarations
CartanTransformedPolarTemplates.lean 7 declarations
CartanTranslatedProbeChains.lean 1 declarations
CartanTuplePerturbation.lean 1 declarations
CartanTwoPathProbeRestrictions.lean 1 declarations
CartanUniformAction.lean 1 declarations
CartanUniformBoxProfiles.lean 1 declarations
CartanUniformBridgeAbsorption.lean 1 declarations
CartanUniformBridgeGeometry.lean 2 declarations
CartanUniformCommonAffinity.lean 1 declarations
CartanUniformCompactProbeBridge.lean 1 declarations
CartanUniformContactBridge.lean 1 declarations
CartanUniformGeneration.lean 1 declarations
CartanUniformImagePaths.lean 1 declarations
CartanUniformIntrinsicBridge.lean 1 declarations
CartanUniformMeasuredRegions.lean 1 declarations
CartanUniformMetricFactorBounds.lean 1 declarations
CartanUniformNeighborLabels.lean 2 declarations
CartanUniformOffsetThreshold.lean 1 declarations
CartanUniformProfileBridge.lean 3 declarations
CartanUniformSmallHeight.lean 1 declarations
CartanUniformSuffixMetric.lean 1 declarations
CartanUniformTiledSourceBridge.lean 1 declarations
CartanUniformTwoPathRestrictions.lean 1 declarations
CartanUnitarySublinear.lean 2 declarations
CartanVisitPath.lean 1 declarations
CartanWeightDerivation.lean 16 declarations
CartanWeightDilation.lean 12 declarations
CartanWeightHaar.lean 2 declarations
CartanWeights.lean 9 declarations
CartanWordBasis.lean 6 declarations
CartanWordLifts.lean 3 declarations
CartanWordLogarithms.lean 9 declarations
CartanWordModel.lean 10 declarations
CartanWordPacking.lean 2 declarations
CartanWordThickening.lean 1 declarations
CartanWordTrace.lean 3 declarations
CartanWordVolume.lean 1 declarations
CenteredHeightError.lean 3 declarations
CentralExtensionRootCore.lean 1 declarations
CentralRootGenerators.lean 1 declarations
CentralizerLiftJordanFactor.lean 2 declarations
CharacterHemisphereContraction.lean 1 declarations
CharacteristicSemidirectSubgroup.lean 4 declarations
ChartContraction.lean 4 declarations
ChartedExponentialFlow.lean 7 declarations
ClosedIntegrationInHeightKernel.lean 1 declarations
ClosedIntegrationOverHeight.lean 1 declarations
CoarseFlowBounds.lean 2 declarations
CoarsePairHeight.lean 1 declarations
CoarsePathHeightWords.lean 2 declarations
CocycleContractingFlow.lean 4 declarations
CommutatorBarBoundary.lean 5 declarations
CommutingLiePowerLogarithms.lean 1 declarations
CompactDerivativeBounds.lean 1 declarations
CompactFlowNeighborhood.lean 1 declarations
CompactFlowSegments.lean 4 declarations
CompactFlowTest.lean 1 declarations
CompactLieLaws.lean 4 declarations
CompactRotationalTwist.lean 8 declarations
CompactSemidirectModel.lean 2 declarations
ComplexAdjointGroup.lean 2 declarations
ComplexAdjointKernel.lean 9 declarations
ComplexAdjointWeights.lean 5 declarations
ComplexCartanJordan.lean 4 declarations
ComplexCartanQuotient.lean 7 declarations
ComplexCartanRotations.lean 18 declarations
ComplexNilradical.lean 5 declarations
ComplexPhaseDerivative.lean 2 declarations
ComplexRotationDerivation.lean 10 declarations
ComplexRotationTorus.lean 14 declarations
ComplexTriangularExponential.lean 4 declarations
ComplexTriangularPolynomial.lean 3 declarations
ComplexWeightFactorModel.lean 2 declarations
ComplexWeightKernel.lean 1 declarations
ComplexWeightLift.lean 2 declarations
ComplexWeightRange.lean 1 declarations
ComplexifiedCartan.lean 3 declarations
ComplexifiedLieAutomorphism.lean 7 declarations
ComplexifiedOperatorExponential.lean 3 declarations
ConeHeightMultiplier.lean 2 declarations
ConeIdealFlowConjugation.lean 2 declarations
ConeIdealFlowTiling.lean 5 declarations
ConeIdealInsideAdjoint.lean 3 declarations
ConjugateCartanWeights.lean 5 declarations
ConjugationFlow.lean 9 declarations
ConstructExponential.lean 11 declarations
ConstructMinimizingLieMetric.lean 3 declarations
ContactFlowTime.lean 2 declarations
ContinuousFlowAffinity.lean 9 declarations
ContinuousFlowDistortion.lean 3 declarations
ContractedNilpotentFlow.lean 2 declarations
ControlledContraction.lean 3 declarations
CoordinateFlowDerivative.lean 6 declarations
CoordinateFlowProfileIdentity.lean 2 declarations
CoordinateLieBrackets.lean 6 declarations
CoordinateProfileFlow.lean 3 declarations
CorrectedHeightRecognition.lean 3 declarations
CoupledRootIntervals.lean 7 declarations
CyclicJoinHeight.lean 10 declarations
DenseDerivativeLabels.lean 3 declarations
DerivationFlowRepresentation.lean 3 declarations
DerivationLieSpace.lean 6 declarations
DerivativeOscillation.lean 1 declarations
DifferentialAlongExponential.lean 1 declarations
DiscreteAbelianHeightKernel.lean 1 declarations
DiscreteHeightKernel.lean 4 declarations
DiscreteNilpotentLieGroup.lean 2 declarations
DominantEigenlineContraction.lean 8 declarations
DynkinGlobalExponential.lean 1 declarations
DynkinLocalExponential.lean 3 declarations
ExponentialAutomorphismTopology.lean 2 declarations
ExponentialBasisGeneration.lean 2 declarations
ExponentialBasisSection.lean 4 declarations
ExponentialBoxCompact.lean 1 declarations
ExponentialBoxCoordinates.lean 4 declarations
ExponentialBoxMass.lean 1 declarations
ExponentialBoxNeighborhood.lean 3 declarations
ExponentialBoxRadius.lean 1 declarations
ExponentialBoxRadiusVolume.lean 1 declarations
ExponentialBridgeComposition.lean 1 declarations
ExponentialCellMass.lean 2 declarations
ExponentialChartBridge.lean 1 declarations
ExponentialCoarseMetric.lean 2 declarations
ExponentialCoefficientStability.lean 4 declarations
ExponentialDuhamel.lean 2 declarations
ExponentialDuhamelDerivative.lean 2 declarations
ExponentialEmbedding.lean 3 declarations
ExponentialGoodCells.lean 2 declarations
ExponentialHaarImage.lean 1 declarations
ExponentialHaarMultiplier.lean 1 declarations
ExponentialHeightKernel.lean 5 declarations
ExponentialHomExt.lean 2 declarations
ExponentialHomLinear.lean 1 declarations
ExponentialIdeal.lean 3 declarations
ExponentialIntegralCurve.lean 2 declarations
ExponentialKernelCentral.lean 1 declarations
ExponentialLocalSeparation.lean 2 declarations
ExponentialNaturality.lean 3 declarations
ExponentialNormality.lean 2 declarations
ExponentialParameterChart.lean 2 declarations
ExponentialProduct.lean 9 declarations
ExponentialProductChart.lean 9 declarations
ExponentialProductCoefficients.lean 8 declarations
ExponentialProductCoordinates.lean 3 declarations
ExponentialProfileCells.lean 1 declarations
ExponentialQuotientSection.lean 4 declarations
ExponentialRangeSubgroup.lean 2 declarations
ExponentialRepresentationDescent.lean 1 declarations
ExponentialRepresentationInput.lean 4 declarations
ExponentialRepresentationTopology.lean 1 declarations
ExponentialRightHaar.lean 3 declarations
ExponentialSmoothHom.lean 4 declarations
ExponentialSubsetVolume.lean 3 declarations
ExponentialTangentUniqueness.lean 2 declarations
ExponentialTriangularImage.lean 1 declarations
ExponentialTupleCoordinates.lean 7 declarations
ExponentialVolumeRatio.lean 1 declarations
ExtremeFlowAffinity.lean 1 declarations
FacetRootSwitch.lean 1 declarations
FactorExponentialOverlap.lean 1 declarations
FactorPhaseDerivative.lean 3 declarations
FactorPhaseOperatorDerivative.lean 2 declarations
FactorRotationCharacter.lean 8 declarations
FaithfulDifferential.lean 1 declarations
FaithfulRepresentationBCH.lean 1 declarations
FaithfulTriangularRepresentation.lean 1 declarations
FiniteAssociativeBCH.lean 4 declarations
FiniteCoordinateSmoothness.lean 3 declarations
FiniteExponentialLogarithm.lean 5 declarations
FiniteFlowSlopes.lean 2 declarations
FiniteLieNorm.lean 7 declarations
FiniteLieSmooth.lean 4 declarations
FixedVectorLieLogarithm.lean 6 declarations
FixedWeightContact.lean 2 declarations
FlowDerivativeIntegral.lean 2 declarations
FlowDerivativeTransport.lean 2 declarations
FlowIntegrationByParts.lean 1 declarations
FlowLineAffinity.lean 1 declarations
FlowLineDifferentiability.lean 2 declarations
FlowLineLabels.lean 1 declarations
FlowNeighborhoods.lean 2 declarations
FlowProbabilityCutoffs.lean 1 declarations
FlowSampleDomination.lean 3 declarations
FlowSegmentImages.lean 5 declarations
FlowStepIteration.lean 2 declarations
FlowSupportedProfileIncrement.lean 1 declarations
GeneralizedLieEigenvectors.lean 3 declarations
GenericFlowChambers.lean 1 declarations
GenericWeightDirections.lean 4 declarations
GlobalHeight.lean 3 declarations
GoodProfileFlow.lean 2 declarations
GoodRescaledFlowLegs.lean 1 declarations
GradedFlowLimit.lean 5 declarations
GradedHeight.lean 5 declarations
HarmonicAnalyticScales.lean 1 declarations
HeightChangeOfCoordinates.lean 3 declarations
HeightConjugationDifferential.lean 3 declarations
HeightFactorization.lean 4 declarations
HeightHomomorphism.lean 3 declarations
HeightKernelCoordinates.lean 1 declarations
HeightKernelDeterminant.lean 1 declarations
HeightKernelModel.lean 2 declarations
HeightKernelNilpotentStructure.lean 3 declarations
HeightKernelRecognition.lean 1 declarations
HeightKernelTorsionBound.lean 2 declarations
HeightKernelVirtualSolvable.lean 1 declarations
HeightLipschitz.lean 2 declarations
HomExponentialDerivative.lean 1 declarations
HorizontalDerivativeLabel.lean 3 declarations
HorizontalFlowDerivative.lean 5 declarations
HorizontalLinearDerivative.lean 1 declarations
IndependentWeightCone.lean 8 declarations
IndividualRotationDerivative.lean 4 declarations
InducingFromHeightKernel.lean 1 declarations
InnerCentralizerLieSubalgebra.lean 7 declarations
InnerCorrectedJordanFactor.lean 1 declarations
InnerTwistJordanFactor.lean 2 declarations
IntegralAbelianBarBoundary.lean 3 declarations
IntegralSemidirectEmbedding.lean 5 declarations
IntegralSemidirectPowerTopology.lean 2 declarations
IntegratedCartanRotations.lean 7 declarations
IntegratedNilradicalRotations.lean 11 declarations
IntrinsicAdjointDerivative.lean 1 declarations
IntrinsicAdjointExponential.lean 5 declarations
IntrinsicAdjointHeight.lean 6 declarations
IntrinsicCanonicalHeight.lean 3 declarations
IntrinsicCartanFactorModel.lean 1 declarations
IntrinsicCartanHeightAssembly.lean 1 declarations
IntrinsicContractionModel.lean 1 declarations
IntrinsicDerivationFlow.lean 2 declarations
IntrinsicExponentialSmooth.lean 1 declarations
IntrinsicHeightKernel.lean 4 declarations
IntrinsicSmoothCoordinates.lean 2 declarations
IntrinsicTriangularRealization.lean 2 declarations
IntrinsicTriangularRepresentation.lean 2 declarations
IntrinsicTriangularTopology.lean 1 declarations
InvariantGraphLieModel.lean 8 declarations
InvariantTriangularBasis.lean 2 declarations
InvertibleJordanDecomposition.lean 2 declarations
JointFlowRelation.lean 2 declarations
JordanInnerTwist.lean 2 declarations
JordanLangTransversal.lean 2 declarations
JordanLieFactor.lean 2 declarations
JordanTransversalLinearMap.lean 1 declarations
LieAdjointSmoothness.lean 2 declarations
LieConjugationDifferential.lean 6 declarations
LieExponential.lean 2 declarations
LieHomDifferential.lean 4 declarations
LieIdealNormalityInput.lean 1 declarations
LieIntegrationInput.lean 2 declarations
LieIntegrationNaturality.lean 3 declarations
LieModelMetric.lean 10 declarations
LieModelUnimodular.lean 2 declarations
LieModularInput.lean 4 declarations
LieProductDifferential.lean 2 declarations
LieWordDerivative.lean 3 declarations
LieWordDifference.lean 7 declarations
LieWordDifferential.lean 9 declarations
LinearContractingPingPong.lean 2 declarations
LinearExponentialAction.lean 6 declarations
LinkedRootProbeFrames.lean 2 declarations
ListBarBoundaryGrade.lean 2 declarations
ListBarBoundaryOperators.lean 8 declarations
ListBarDifferential.lean 4 declarations
LocalExponentialOpen.lean 1 declarations
LocalFlowLabel.lean 3 declarations
LocalParameterSmoothness.lean 1 declarations
ManifoldLocalCoordinates.lean 1 declarations
ManifoldLocalParameter.lean 1 declarations
ManifoldRelatedBracket.lean 3 declarations
MatrixDifferentialFromSmoothness.lean 1 declarations
MeasurableDerivativeLabels.lean 2 declarations
MetricCartanFactorBounds.lean 1 declarations
MinimizingLieMetric.lean 4 declarations
MovingBaseFlow.lean 3 declarations
MultilinearBarBoundary.lean 4 declarations
MultiplicativeJordanUniqueness.lean 2 declarations
NetSmoothing.lean 3 declarations
NilpotentBoundaryAveraging.lean 1 declarations
NilpotentCentralRoots.lean 2 declarations
NilpotentCoordinateFlow.lean 10 declarations
NilpotentDerivationFlow.lean 3 declarations
NilpotentDerivationFlowDerivative.lean 1 declarations
NilpotentDerivationFlowSmooth.lean 2 declarations
NilpotentDifferenceDerivative.lean 2 declarations
NilpotentExponential.lean 5 declarations
NilpotentExponentialSurjective.lean 2 declarations
NilpotentFiniteRankRootCore.lean 4 declarations
NilpotentFlow.lean 5 declarations
NilpotentLieExistenceConstruction.lean 2 declarations
NilpotentLieGroupNilpotent.lean 2 declarations
NilpotentLieModel.lean 4 declarations
NilpotentLinearFlow.lean 6 declarations
NilpotentRootDimension.lean 3 declarations
NilpotentRootExhaustion.lean 2 declarations
NilpotentRootGenerators.lean 2 declarations
NilpotentSemidirectGroup.lean 8 declarations
NilpotentSemidirectNilpotence.lean 1 declarations
NilpotentSemidirectTangent.lean 9 declarations
NilpotentUniqueRoots.lean 1 declarations
NilpotentUpperCentralRoots.lean 3 declarations
NilradicalRotationAction.lean 3 declarations
NormalizedExponentialLaws.lean 3 declarations
NormalizedPairBackwardHeight.lean 2 declarations
NormalizedPairHeightTransfer.lean 1 declarations
NormalizedWeightRays.lean 7 declarations
NormedLiePolynomial.lean 2 declarations
OccupationFlowLimit.lean 1 declarations
OccupationFlowMicrosteps.lean 1 declarations
OrderedInterpolationWeights.lean 2 declarations
OrderedSemidirectWords.lean 5 declarations
PairHeightCocycle.lean 9 declarations
ParametricLieWords.lean 7 declarations
PolycyclicRootIndex.lean 3 declarations
PolynomialCoordinateSmooth.lean 1 declarations
PolynomialDerivativeGrowth.lean 8 declarations
PolynomialDifferential.lean 4 declarations
PolynomialExponentialChart.lean 1 declarations
PolynomialExponentialCoordinates.lean 2 declarations
PolynomialInnerAdjoint.lean 3 declarations
PolynomialLieWordCoordinates.lean 4 declarations
PolynomialMatrixLieRepresentation.lean 3 declarations
PolynomialMinorDifferential.lean 6 declarations
PolynomialModelExponential.lean 3 declarations
PositiveSizeTriangularRepresentation.lean 7 declarations
PositiveWeightCones.lean 11 declarations
PresentationRotation.lean 22 declarations
PrimitiveNilpotentExponential.lean 3 declarations
ProductLieAlgebra.lean 9 declarations
ProfileChainHeightBounds.lean 3 declarations
ProfileDerivativeLabel.lean 3 declarations
ProfileFlowConvergence.lean 3 declarations
ProfileHeightIdentity.lean 2 declarations
ProfileWeightSigns.lean 1 declarations
PublishedRootDistortion.lean 1 declarations
RationalFlowBoxes.lean 3 declarations
RationalLieWordProjection.lean 5 declarations
RationalRootSurjection.lean 2 declarations
RayGroupContraction.lean 6 declarations
RayQuotientContraction.lean 5 declarations
RayTangentContraction.lean 4 declarations
RealCartanQuotient.lean 7 declarations
RealCartanRotations.lean 13 declarations
RealJordanLieFactor.lean 1 declarations
RealLieAutomorphismPowerLog.lean 2 declarations
RealLieJordanDecomposition.lean 2 declarations
RealNormedLieAlgebra.lean 1 declarations
RealPhaseDerivative.lean 1 declarations
RealPhaseExponential.lean 3 declarations
RealRotationDerivation.lean 13 declarations
RealRotationTorus.lean 5 declarations
RealSemisimpleLieLogarithm.lean 1 declarations
RealShadowCartan.lean 5 declarations
RealShadowConjugation.lean 4 declarations
RealShadowOperators.lean 5 declarations
RealShadowRepresentation.lean 1 declarations
RealShadowRepresentationTransport.lean 1 declarations
RealShadowSplit.lean 9 declarations
RealTorusAdjoint.lean 3 declarations
RealTorusSmoothRepresentation.lean 4 declarations
RecognitionFromAffineHeight.lean 1 declarations
RecognitionFromHeight.lean 4 declarations
RecognitionFromUniformHeight.lean 1 declarations
RecognitionInLieModel.lean 2 declarations
RelativeJordanInnerTwist.lean 1 declarations
RepresentationFromDifferential.lean 2 declarations
RepresentationHeightFactor.lean 1 declarations
RepresentationKernelAdjoint.lean 2 declarations
RepresentedAdjoint.lean 1 declarations
RepresentedExponentialDifferential.lean 2 declarations
RepresentedExponentialLogSmooth.lean 1 declarations
RepresentedSolvableLieModel.lean 3 declarations
RescaledFlowLipschitz.lean 2 declarations
RescaledHeightLegs.lean 1 declarations
RescaledLieFamily.lean 4 declarations
RiemannianExponentialInputs.lean 2 declarations
RootCoreAbelianRank.lean 1 declarations
RootCoreExtensionDimension.lean 1 declarations
RootFlow.lean 5 declarations
RootGeneratorHomExt.lean 2 declarations
RootIntervalPadding.lean 2 declarations
RootIntervalSampling.lean 7 declarations
RootIntervalSlack.lean 1 declarations
RootIntervalSupports.lean 3 declarations
RootRepresentation.lean 7 declarations
RootSupportSwitch.lean 2 declarations
RootSwitchBounds.lean 2 declarations
RootSwitchCurves.lean 6 declarations
RotationExponentialProduct.lean 3 declarations
RotationFactorAction.lean 3 declarations
RotationFactorDifferentials.lean 2 declarations
RotationFactorKernel.lean 6 declarations
RotationFactorLifts.lean 8 declarations
RotationFactorParameter.lean 4 declarations
RotationFactorProduct.lean 7 declarations
RotationLieRepresentation.lean 1 declarations
RotationRepresentationFaithful.lean 1 declarations
RotationRepresentationIntegration.lean 1 declarations
RotationRepresentationRelations.lean 3 declarations
RotationRepresentedChart.lean 1 declarations
RotationTriangulableModel.lean 2 declarations
RotationTriangularRepresentation.lean 1 declarations
RotationalTwistBracket.lean 1 declarations
RotationalTwistCharacter.lean 3 declarations
RotationalTwistConjugation.lean 1 declarations
RotationalTwistInvariantField.lean 1 declarations
RotationalTwistLift.lean 3 declarations
ScalarNilpotentExponential.lean 3 declarations
SectionWeightedBoxes.lean 4 declarations
SegmentIncrementDerivative.lean 1 declarations
SegmentVolumeDerivative.lean 1 declarations
SemidirectAxisExponential.lean 2 declarations
SemidirectCoordinateOrbit.lean 8 declarations
SemidirectExponentialCoordinates.lean 1 declarations
SemidirectIntegration.lean 4 declarations
SemidirectPolynomialCurves.lean 5 declarations
SemidirectPolynomialMaps.lean 5 declarations
SemidirectPolynomialRepresentation.lean 3 declarations
SemidirectPrefixTuples.lean 11 declarations
SemidirectProductHaar.lean 10 declarations
SemidirectProductTopology.lean 13 declarations
SemidirectUnipotentRepresentation.lean 2 declarations
SemisimpleExponential.lean 2 declarations
SemisimpleLieLogarithm.lean 4 declarations
SequenceCartanAccessible.lean 1 declarations
SequenceCartanBoxAction.lean 1 declarations
SequenceCartanConjugationBoxes.lean 1 declarations
SequenceCartanDenominator.lean 1 declarations
SequenceCartanOccupation.lean 1 declarations
SequenceCartanOverlap.lean 2 declarations
SequenceCartanPathLifts.lean 2 declarations
SequenceCartanPrefixes.lean 1 declarations
SequenceCartanProducts.lean 1 declarations
SequenceCartanProfileIncrement.lean 1 declarations
SequenceCartanProfilePacking.lean 1 declarations
SequenceCartanRecurrenceBoxes.lean 1 declarations
SequenceCartanTupleLifts.lean 1 declarations
SequenceCellFlowLegs.lean 1 declarations
SequenceConeIdealFlowTiling.lean 1 declarations
SequenceRescaledFlowLegs.lean 1 declarations
SequenceRootSwitch.lean 1 declarations
SequenceSmallExponentialProducts.lean 1 declarations
SequenceSmoothPolynomialImage.lean 1 declarations
SequenceWeightedSectionError.lean 1 declarations
ShadowExponentialCoordinates.lean 5 declarations
SheetEndpointHeight.lean 2 declarations
SimultaneousAdjointBasis.lean 2 declarations
SmallHeightSamplingBall.lean 1 declarations
SmoothAutonomousCurve.lean 2 declarations
SmoothComplexWeightFactors.lean 4 declarations
SmoothCoordinateAction.lean 5 declarations
SmoothExponentialCurve.lean 2 declarations
SmoothExponentialDifferential.lean 2 declarations
SmoothExponentialHeight.lean 1 declarations
SmoothFactorRotations.lean 2 declarations
SmoothFaithfulRepresentation.lean 1 declarations
SmoothFlowTest.lean 1 declarations
SmoothFromRiemannian.lean 1 declarations
SmoothHomLieDifferential.lean 4 declarations
SmoothImmersionCancellation.lean 1 declarations
SmoothIndividualRotations.lean 4 declarations
SmoothIntegralActionExtension.lean 1 declarations
SmoothIntegralCurve.lean 2 declarations
SmoothIntoRiemannian.lean 1 declarations
SmoothLieDifferential.lean 4 declarations
SmoothLieExponential.lean 14 declarations
SmoothLieNaturality.lean 3 declarations
SmoothLieRegularity.lean 3 declarations
SmoothLocalSection.lean 3 declarations
SmoothManifoldImmersionCancellation.lean 1 declarations
SmoothPolynomialAutomorphisms.lean 2 declarations
SmoothPolynomialFamilyImage.lean 2 declarations
SmoothPolynomialRepresentation.lean 5 declarations
SmoothRealActionModel.lean 7 declarations
SmoothRotationExtension.lean 6 declarations
SmoothRotationalAction.lean 7 declarations
SmoothRotationalTwist.lean 7 declarations
SmoothRotationalTwistLift.lean 2 declarations
SmoothVectorActionModel.lean 7 declarations
SolvableGroupLieAlgebra.lean 1 declarations
SolvableWeightEigenvectors.lean 1 declarations
SpectralLieDerivation.lean 2 declarations
SpectralLogExponential.lean 2 declarations
SplitLieQuotient.lean 1 declarations
SublinearHeightComposition.lean 3 declarations
SupportFlowLegs.lean 5 declarations
SupportedFlowLipschitz.lean 5 declarations
TangentRotationRepresentation.lean 3 declarations
TemplateWeightRays.lean 1 declarations
TransferredHeight.lean 3 declarations
TransportedManifold.lean 4 declarations
TriangulableLieModel.lean 6 declarations
TriangularAdjointEmbedding.lean 12 declarations
TriangularAdjointSolvable.lean 1 declarations
TriangularAdjointTransport.lean 2 declarations
TriangularBilinearFactor.lean 2 declarations
TriangularChainPacking.lean 4 declarations
TriangularExponentialAverage.lean 7 declarations
TriangularExponentialInjective.lean 1 declarations
TriangularExponentialKernel.lean 4 declarations
TriangularGroupIntegration.lean 1 declarations
TriangularHeight.lean 18 declarations
TriangularInverseBounds.lean 1 declarations
TriangularLieDifferential.lean 6 declarations
TriangularLocalLogarithm.lean 5 declarations
TriangularMatrixExponential.lean 3 declarations
TriangularMatrixExponentialInjective.lean 2 declarations
TriangularMatrixHeight.lean 11 declarations
TriangularMatrixLieAlgebra.lean 7 declarations
TriangularOperatorAverage.lean 3 declarations
TriangularPrimary.lean 3 declarations
TriangularProducts.lean 7 declarations
TriangularRealizationConstruction.lean 1 declarations
TriangularRealizationInput.lean 3 declarations
TriangularRepresentationKernel.lean 1 declarations
TriangularWordBounds.lean 9 declarations
TruncatedSemidirectRepresentation.lean 8 declarations
TruncatedWordExponential.lean 9 declarations
TupleBarBoundaryRecursion.lean 1 declarations
UniformBasepointHeight.lean 3 declarations
UniformCartanHeight.lean 1 declarations
UniformCartanPublishedCharts.lean 1 declarations
UniformCoarseCartanHeight.lean 1 declarations
UniformWeightedSectionError.lean 2 declarations
UnipotentConjugationFlow.lean 2 declarations
UnipotentCoordinateBCH.lean 1 declarations
UnipotentLieFlow.lean 7 declarations
UnipotentLieLogarithm.lean 2 declarations
UnitsLieAlgebra.lean 6 declarations
UniversalAllScaleCartanProfiles.lean 3 declarations
UniversalBCHCoefficientBound.lean 4 declarations
UniversalCartanProfiles.lean 1 declarations
ValuedEigenlineContraction.lean 6 declarations
WeightBasisTrace.lean 1 declarations
WeightChamberAction.lean 9 declarations
WeightChamberLimits.lean 7 declarations
WeightChambers.lean 10 declarations
WeightRayPermutation.lean 3 declarations
WeightRotationCharacter.lean 6 declarations
WeightRotationDerivation.lean 9 declarations
WeightSamplingPolytope.lean 12 declarations
WeightSamplingSupport.lean 2 declarations
WeightSpaceWordSpan.lean 1 declarations
WeightedBasisComparison.lean 1 declarations
WeightedBoxVolume.lean 5 declarations
WeightedChainMetric.lean 7 declarations
WeightedColumnBasis.lean 11 declarations
WeightedHaarVolume.lean 4 declarations
WeightedMetricChains.lean 2 declarations
WeightedSectionError.lean 2 declarations
WeightedWordBound.lean 1 declarations
WeightedWordComponents.lean 4 declarations
WeightedWordLogarithm.lean 4 declarations
WeightedWordNorm.lean 18 declarations
WeightedWordSubalgebra.lean 7 declarations
WeightedWordSubstitution.lean 6 declarations
WeightedZonotope.lean 3 declarations
WordChartFlowHeight.lean 2 declarations
WordChartHeight.lean 1 declarations
WordLieProjection.lean 6 declarations
WordProjectionAdjoint.lean 3 declarations