OAI/Geometry/WeakHessian/LocalBounds/
751 declarations, 0 contain sorry, 0 declared as axioms; 156 files
Files
- AbsGammaLipschitz.lean 3 declarations
- AbsolutelyContinuousDistDom.lean 2 declarations
- ActualCore.lean 1 declarations
- AffineTime.lean 22 declarations
- AscendingSlope.lean 16 declarations
- AverageConvergence.lean 1 declarations
- AverageLipschitz.lean 2 declarations
- AverageTest.lean 2 declarations
- AverageWeighted.lean 2 declarations
- BoundedCost.lean 2 declarations
- BoundedDriftFixedPoint.lean 2 declarations
- BoundedDriftRegularity.lean 1 declarations
- BoundedEndpointTube.lean 14 declarations
- BoundedGraphCore.lean 1 declarations
- BoundedLawDualPointwise.lean 2 declarations
- BoundedMulLp.lean 8 declarations
- BoundedMulLpTendsto.lean 1 declarations
- BoundedRnRestriction.lean 2 declarations
- CaccioppoliAlgebra.lean 2 declarations
- CappedExcess.lean 11 declarations
- ChangeLpLp.lean 7 declarations
- ClampTimeVal.lean 4 declarations
- ClosedQuadraticEnergy.lean 13 declarations
- ComplexifyReal.lean 4 declarations
- CompressionRate.lean 4 declarations
- Confinement.lean 3 declarations
- ConstLp.lean 8 declarations
- ConstMul.lean 4 declarations
- ContactUniqueness.lean 5 declarations
- ContinuousTimeMarginals.lean 4 declarations
- CoreAlgebra.lean 10 declarations
- CostContinuity.lean 3 declarations
- CostConvergence.lean 3 declarations
- CostExistence.lean 2 declarations
- CostMetric.lean 11 declarations
- DecayTimesNatTwo.lean 3 declarations
- DistDecayCover.lean 7 declarations
- Domain.lean 22 declarations
- DriftFixedBase.lean 1 declarations
- DriftPerturbation.lean 6 declarations
- DriftQuantitative.lean 2 declarations
- DuhamelAlgebra.lean 2 declarations
- DyadicTimes.lean 13 declarations
- EVICalculus.lean 4 declarations
- EnergyGammaPairing.lean 2 declarations
- EnergyIdentification.lean 6 declarations
- EulerStep.lean 11 declarations
- EvalRealCoe.lean 4 declarations
- ExcessRelocation.lean 6 declarations
- ExpMulLp.lean 7 declarations
- ExpNegQuadraticBound.lean 2 declarations
- ExponentialODE.lean 1 declarations
- ExtendLp.lean 4 declarations
- FormCoreDense.lean 1 declarations
- FormCorePairing.lean 1 declarations
- FormDualRegularity.lean 1 declarations
- FormGamma.lean 5 declarations
- GammaAddConstLeft.lean 4 declarations
- GammaNatMulLeft.lean 10 declarations
- GammaRepresentativePairing.lean 4 declarations
- GammaTimeDifferentiation.lean 3 declarations
- GammaVariableContinuity.lean 2 declarations
- GlobalMultiplierCore.lean 1 declarations
- GlobalTestAverage.lean 1 declarations
- GlobalTestCore.lean 2 declarations
- GraphFilter.lean 1 declarations
- GraphGammaPairing.lean 1 declarations
- GraphReuse.lean 18 declarations
- HalfTime.lean 6 declarations
- HopfEnergyComparison.lean 1 declarations
- HopfEnergyInitial.lean 1 declarations
- HopfEnergyLower.lean 3 declarations
- HopfInitialSlope.lean 6 declarations
- HopfWeightedEnergy.lean 3 declarations
- IdentifiedConservation.lean 11 declarations
- InclusionDoubleDualSurjective.lean 5 declarations
- IntegratedEVI.lean 2 declarations
- JoinCurve.lean 10 declarations
- L2SlopeGraph.lean 13 declarations
- Law.lean 20 declarations
- LipschitzMulDist.lean 2 declarations
- LocalOffset.lean 1 declarations
- LocalPairing.lean 2 declarations
- LocalizedCertificate.lean 7 declarations
- LocalizedScaling.lean 9 declarations
- LocalizedSlopeGraphMap.lean 9 declarations
- LpLipschitzClosed.lean 1 declarations
- MetricPlateau.lean 2 declarations
- MinNatTendsto.lean 3 declarations
- MulBounded.lean 4 declarations
- OneSidedBump.lean 3 declarations
- OneSidedKernel.lean 1 declarations
- OriginalCoreProducer.lean 1 declarations
- PositiveProbes.lean 9 declarations
- PotentialPairing.lean 3 declarations
- QuadraticContact.lean 3 declarations
- QuadraticCost.lean 5 declarations
- QuadraticPairing.lean 1 declarations
- QuadraticPotentials.lean 7 declarations
- QuadraticVariational.lean 3 declarations
- RadialCost.lean 6 declarations
- RadialRoots.lean 5 declarations
- ReLp.lean 40 declarations
- RealClip.lean 7 declarations
- RelaxedDomain.lean 3 declarations
- RelaxedProx.lean 10 declarations
- ReversePoincarePointwise.lean 2 declarations
- ReweightCost.lean 3 declarations
- RootApproximation.lean 15 declarations
- RunningMin.lean 7 declarations
- SetDensities.lean 7 declarations
- SharpPointwise.lean 1 declarations
- SigmaCoeffExpLower.lean 2 declarations
- SlopeApprox.lean 9 declarations
- SlopeApproxAntitone.lean 10 declarations
- SlopeApproxProduct.lean 2 declarations
- Smul.lean 6 declarations
- SpatialDual.lean 5 declarations
- SpeedApprox.lean 16 declarations
- SqrtWeighted.lean 2 declarations
- SquareControl.lean 7 declarations
- SquareTimePairing.lean 6 declarations
- StrongRoots.lean 2 declarations
- SubConst.lean 5 declarations
- Subdifferential.lean 4 declarations
- SuperpositionProper.lean 1 declarations
- TargetEVI.lean 2 declarations
- TestChain.lean 2 declarations
- TestLinear.lean 3 declarations
- TestProduct.lean 2 declarations
- TestScaling.lean 4 declarations
- TimeHalf.lean 10 declarations
- TriangularFold.lean 7 declarations
- TripleTimeContinuity.lean 2 declarations
- TripleTimePairing.lean 2 declarations
- UniformTestAverage.lean 2 declarations
- UniformWeightedCZero.lean 1 declarations
- VariableDissipationFullDomain.lean 1 declarations
- VariableDissipationTest.lean 1 declarations
- VariableDuhamelClosure.lean 3 declarations
- VariableEnergyClosure.lean 2 declarations
- VarianceContinuity.lean 1 declarations
- VolumeLower.lean 1 declarations
- WeightedBE.lean 1 declarations
- WeightedCZero.lean 2 declarations
- WeightedConservation.lean 3 declarations
- WeightedEVI.lean 1 declarations
- WeightedEnergyClosure.lean 5 declarations
- WeightedEnergySpace.lean 4 declarations
- WeightedGraphInequality.lean 1 declarations
- WeightedInitialLaw.lean 1 declarations
- WeightedPairing.lean 1 declarations
- WeightedPairing2.lean 2 declarations
- WeightedReversePoincare.lean 2 declarations
- WeightedTV.lean 1 declarations
- Young.lean 1 declarations