OAI/Geometry/WeakHessian/Sobolev/
185 declarations, 0 contain sorry, 0 declared as axioms; 58 files
Files
- AddConst.lean 6 declarations
- AeAcRepresentativeMeasurable.lean 2 declarations
- AeEndpointGlobal.lean 2 declarations
- AnySubgradient.lean 1 declarations
- BochnerConvex.lean 4 declarations
- CDSobolevLipschitz.lean 1 declarations
- CheegerClosedQuadraticEnergy.lean 2 declarations
- CheegerEnergyComparable.lean 1 declarations
- CheegerEnergyCongrAe.lean 5 declarations
- CheegerEnergyConst.lean 5 declarations
- CheegerEnergyMinimal.lean 3 declarations
- CheegerEnergySlope.lean 5 declarations
- CheegerEnergyWeakBounded.lean 2 declarations
- CompContDiff.lean 2 declarations
- CompContDiff2.lean 9 declarations
- CompContDiffLipschitz.lean 3 declarations
- CongrAeLeft.lean 4 declarations
- CutoffCheegerEnergy.lean 1 declarations
- DaviesGradient.lean 1 declarations
- EndpointPairingBound.lean 1 declarations
- EndpointPairingBoundGlobal.lean 1 declarations
- GlobalCheegerEnergyMinimal.lean 3 declarations
- GlobalCheegerEnergyReal.lean 6 declarations
- GlobalCheegerEnergyWeak.lean 1 declarations
- GradientPairSum.lean 11 declarations
- GradientProbes.lean 4 declarations
- GradientSquare.lean 1 declarations
- HessianMonotone.lean 2 declarations
- Integral.lean 1 declarations
- L2GradientGraph.lean 7 declarations
- LaplacianChain.lean 1 declarations
- LaplacianLocality.lean 3 declarations
- LipschitzBochnerIntegral.lean 1 declarations
- LocalMeasureGradient.lean 5 declarations
- LocalSobolevLipschitz.lean 4 declarations
- LocalizedGradient.lean 2 declarations
- Minimal.lean 11 declarations
- MulBounded.lean 6 declarations
- NoncompactSubgradient.lean 1 declarations
- NormMinimalRelaxedGradient.lean 2 declarations
- OriginalBochner.lean 2 declarations
- Piecewise.lean 3 declarations
- QuadraticCheegerEnergyComparable.lean 1 declarations
- QuadraticGradient.lean 9 declarations
- RadialGradientBound.lean 1 declarations
- SobolevBochner.lean 1 declarations
- SobolevCheegerEnergyTop.lean 4 declarations
- SobolevLipschitz.lean 4 declarations
- SobolevPairing.lean 2 declarations
- SobolevSubdifferential.lean 1 declarations
- SquareSobolev.lean 4 declarations
- TestBochner.lean 3 declarations
- UpperGradientNormTendsto.lean 2 declarations
- UpperGradientTendstoNorm.lean 5 declarations
- VariableDissipationSobolev.lean 1 declarations
- WeakGradientContactDistance.lean 2 declarations
- WeakGradientMul.lean 5 declarations
- WeightedGradientLoss.lean 2 declarations