OAI/Analysis/BiholderTransport/Coordinates/
302 declarations, 0 contain sorry, 0 declared as axioms; 105 files
Files
- AECertificates.lean 3 declarations
- ActiveCompact.lean 4 declarations
- ActiveDifferentiability.lean 5 declarations
- ActiveHull.lean 4 declarations
- ActiveHullUniform.lean 3 declarations
- ActiveUniformGrowth.lean 3 declarations
- ActualLowerTestBound.lean 1 declarations
- Add.lean 1 declarations
- AePullbackLipschitzChart.lean 2 declarations
- BranchChartBaseline.lean 1 declarations
- BranchChartJets.lean 1 declarations
- BranchInverse.lean 2 declarations
- BranchJets.lean 1 declarations
- ChartActiveLimit.lean 4 declarations
- ChartAlexandrov.lean 1 declarations
- ChartCenterGain.lean 1 declarations
- ChartCostJets.lean 3 declarations
- ChartGradientMap.lean 7 declarations
- ChartHopfLocalization.lean 1 declarations
- ChartLipschitz.lean 1 declarations
- ChartParameter.lean 2 declarations
- ChartTransition.lean 9 declarations
- ChartTrueCenter.lean 1 declarations
- Charts.lean 1 declarations
- CompactConfigurations.lean 4 declarations
- CompactEventuallyFiberwise.lean 1 declarations
- CoordinateExpansion.lean 5 declarations
- CoordinateGradient.lean 3 declarations
- CoordinateMatrices.lean 5 declarations
- CoordinateMetricNorm.lean 4 declarations
- CoordinatePairingDerivative.lean 1 declarations
- CoordinatePole.lean 3 declarations
- CoordinateTrueLog.lean 1 declarations
- CoordinateVariation.lean 2 declarations
- Coordinates.lean 9 declarations
- CutCharacterization.lean 2 declarations
- Endpoint.lean 1 declarations
- ExpJacContinuity.lean 3 declarations
- ExpLocalBounds.lean 2 declarations
- ExpNonconjugacy.lean 4 declarations
- ExpNonconjugateLimit.lean 0 declarations
- ExpReciprocity.lean 1 declarations
- ExpVertical.lean 2 declarations
- FactorNorm.lean 4 declarations
- FiberLog.lean 2 declarations
- FiberNormal.lean 1 declarations
- FiberwiseHomeomorphism.lean 4 declarations
- FiniteActiveGrowth.lean 2 declarations
- FiniteLogScaleAvoidance.lean 2 declarations
- FixedJoinDifference.lean 1 declarations
- FixedJoinSmooth.lean 3 declarations
- GraphCoordinates.lean 5 declarations
- Inner.lean 1 declarations
- IntrinsicGradient.lean 3 declarations
- JetDiffeomorphism.lean 1 declarations
- JoinCoordinates.lean 2 declarations
- JoiningCoordinates.lean 1 declarations
- JointExpInverse.lean 1 declarations
- JointNormalChart.lean 2 declarations
- KernelRadial.lean 2 declarations
- LocalInverseCalculus.lean 1 declarations
- LocalMetricCharts.lean 4 declarations
- LocalOuterJetBound.lean 1 declarations
- LocalOuterLog.lean 1 declarations
- LogActionMixed.lean 4 declarations
- ManifoldLipschitz.lean 5 declarations
- ManifoldMinimum.lean 2 declarations
- MetricLocalGrowth.lean 3 declarations
- Midpoint.lean 3 declarations
- MovingNormalEndpointJoin.lean 3 declarations
- NormalCoordinates.lean 1 declarations
- NormalCoordinates2.lean 3 declarations
- NormalCoordinates3.lean 10 declarations
- NormalEikonal.lean 3 declarations
- NormalEndpointInverse.lean 1 declarations
- NormalEndpointJoin.lean 3 declarations
- NormalFrameTaylor.lean 1 declarations
- NormalGradient.lean 1 declarations
- NormalLogMixed.lean 4 declarations
- NormalLowerTaylorBound.lean 2 declarations
- NormalPoleTaylor.lean 3 declarations
- NormalRigidity.lean 3 declarations
- NormalSubdifferential.lean 5 declarations
- NormalTestChart.lean 2 declarations
- OuterCoordinate.lean 1 declarations
- PoleCoordinates.lean 7 declarations
- Prefix.lean 6 declarations
- ProperPieces.lean 4 declarations
- RadialFactor.lean 2 declarations
- RadialIdentity.lean 7 declarations
- RayBenchmark.lean 4 declarations
- ReverseIsotropicGain.lean 2 declarations
- ScalarExpansion.lean 4 declarations
- ShortLocalMinimum.lean 1 declarations
- SmoothUpperTest.lean 3 declarations
- SplitAction.lean 6 declarations
- SplitLogInjective.lean 6 declarations
- SplitPairing.lean 3 declarations
- Stationary.lean 2 declarations
- TangentLift.lean 8 declarations
- Taylor.lean 2 declarations
- TotalInjectivity.lean 5 declarations
- TwoSidedFiberLog.lean 2 declarations
- UniformLog.lean 2 declarations
- UniformShort.lean 4 declarations