OAI/Geometry/SmoothYau/Smoothness/
1640 declarations, 0 contain sorry, 0 declared as axioms; 95 files
Files
- ActualCoordinateHessianApply.lean 8 declarations
- AdmissibleCutoffWaveLocalizedDerivatives.lean 8 declarations
- BoundedDegreeMonomials.lean 108 declarations
- BundleMetricInner.lean 9 declarations
- BundleRankOne.lean 7 declarations
- CenteredNormalInverseFderiv.lean 2 declarations
- ChartDerivativeNeZeroTransfer.lean 160 declarations
- ChartGradientProjectionSmooth.lean 28 declarations
- ChartJetBoundGlobalValue.lean 6 declarations
- ChartTensorCoordLocal1.lean 47 declarations
- ChartTransition.lean 7 declarations
- CompactActualWavesSignJets.lean 4 declarations
- CompactDisjointSmoothCutoffs.lean 1 declarations
- CompactMetricAllJets.lean 10 declarations
- CompactMetricInverseJets.lean 21 declarations
- CompactSmoothJetMap.lean 4 declarations
- ComplexPolarWeight.lean 21 declarations
- ComplexWaveJetGerm.lean 2 declarations
- ConstantComplexProductJetBound.lean 34 declarations
- ContDiffMetricFluxC1.lean 5 declarations
- ContDiffPartialIteratedFDeriv.lean 4 declarations
- ContDiffSmoothFiniteWave.lean 39 declarations
- ContinuousCompactSmoothJets.lean 35 declarations
- ContinuousSobolevFirstDerivative.lean 35 declarations
- CoordinateMetricFlux.lean 9 declarations
- CutoffExactificationSmoothNeighborhood.lean 8 declarations
- CutoffPullbackLinear.lean 4 declarations
- DistanceSquare.lean 35 declarations
- EventuallyPositiveFactorEventualJets.lean 1 declarations
- ExistsFinitePatchPartition.lean 7 declarations
- ExistsSmoothComplexCutoff.lean 1 declarations
- ExistsSphericalRadialCutoff.lean 5 declarations
- ExistsSupportedPinningBump.lean 2 declarations
- FamilyInverseFst.lean 3 declarations
- FderivCofactorApply.lean 11 declarations
- FderivMetricPairing.lean 7 declarations
- FiniteAmplitudeCentralBound.lean 7 declarations
- FiniteTaylorFunctionThree.lean 2 declarations
- FlowInitialFderiv.lean 7 declarations
- FlowParameters.lean 16 declarations
- FourLiftThreeSmul.lean 8 declarations
- FrameInverseApply.lean 9 declarations
- GlobalPrepDualNorm.lean 37 declarations
- HessianJet.lean 18 declarations
- IteratedFDerivCompClm.lean 4 declarations
- JointMetricDet.lean 10 declarations
- LinearMetricForm.lean 10 declarations
- LinearPowerDirectional.lean 16 declarations
- LocalIntegrationParts.lean 27 declarations
- LpNormTwoBounds.lean 37 declarations
- LpProductLinearMap.lean 8 declarations
- MixedPiolaIdentity.lean 3 declarations
- MomentBesselLp.lean 60 declarations
- Mono.lean 2 declarations
- MultilinearPolynomial.lean 30 declarations
- NormIteratedFDerivCompLinear.lean 24 declarations
- NormIteratedFDerivScalarDirection.lean 28 declarations
- NormalChartWave.lean 11 declarations
- NormalCoordinateMap.lean 3 declarations
- NormalInverseVecNorm.lean 12 declarations
- NormalJetMapFirstPhase.lean 20 declarations
- PhaseDerivativeLipschitz.lean 2 declarations
- PinningTensorSpace.lean 4 declarations
- PiolaIdentity.lean 3 declarations
- PolynomialFiniteWave.lean 48 declarations
- ProbabilityBadJet.lean 2 declarations
- ProductSphereFstPower.lean 12 declarations
- ProfilePeriodizeEventuallyZero.lean 31 declarations
- PulledGradient.lean 71 declarations
- RepresentedWeightedQuinticSmooth.lean 1 declarations
- RoundPowerExteriorPerturbationJet.lean 4 declarations
- RoundPowerRadius.lean 8 declarations
- RoundPowerWeightedChartJets.lean 4 declarations
- SecondDerivNonposLocalMax.lean 4 declarations
- SelectedComplexJetMatrixScale.lean 2 declarations
- SmDualNorm.lean 17 declarations
- SmoothFiniteWaveSum.lean 52 declarations
- SmoothMul.lean 2 imports, no declarations
- SobolevRepresentativeOrderCongr.lean 33 declarations
- SourceSignBox.lean 12 declarations
- SphericalBaseProfileRadius.lean 44 declarations
- TestAsSmooth.lean 13 declarations
- TestDerivativeComm.lean 37 declarations
- ThreeCoupledCleanChartJets.lean 30 declarations
- ThreeFirstNormedSpace.lean 3 declarations
- ThreeRadiusNormedSpace.lean 22 declarations
- ThreeRankNormedSpace.lean 9 declarations
- TorusAmbient.lean 18 declarations
- TotallyBoundedCauchySubsequence.lean 2 declarations
- UniformJetBoundsFiberComp.lean 4 declarations
- UniformJetZeroDifference.lean 4 declarations
- WaveDeriv.lean 12 declarations
- WaveJetMatrix.lean 6 declarations
- WeightedPair.lean 12 declarations
- ZeroJetProd.lean 7 declarations