OAI/Geometry/WeakHessian/Entropy/
339 declarations, 0 contain sorry, 0 declared as axioms; 54 files
Files
- AcBoundedRenyiGaps.lean 8 declarations
- AveragedDensity.lean 7 declarations
- BoundedLipschitzDensity.lean 1 declarations
- CdEntropyBoundFinite.lean 1 declarations
- CenteredMulLogDeriv.lean 8 declarations
- ClosedEntropyAlong.lean 1 declarations
- CompressedDensity.lean 3 declarations
- CostTopology.lean 2 declarations
- DensityConvergence.lean 5 declarations
- DensityCurve.lean 4 declarations
- DensityHamiltonJacobi.lean 1 declarations
- EntropyCell.lean 26 declarations
- EntropyContact.lean 26 declarations
- EntropyDensityBounds.lean 3 declarations
- EntropyDrop.lean 1 declarations
- EntropyLimits.lean 3 declarations
- EntropyPairingLimits.lean 2 declarations
- EntropyRealContinuousSupport.lean 2 declarations
- EntropySlope.lean 5 declarations
- EntropyStability.lean 2 declarations
- ExplicitDensityNorm.lean 4 declarations
- FiniteEntropy.lean 14 declarations
- FiniteEntropyBoundedSupported.lean 2 declarations
- FisherDensity.lean 9 declarations
- FisherEpsilon.lean 17 declarations
- FisherRoot.lean 11 declarations
- GradientParallelogramDefect.lean 5 declarations
- IntegralDensityMeasureLp'.lean 3 declarations
- IntegralDensityMeasureLp.lean 4 declarations
- IntervalEntropyDual.lean 2 declarations
- LinearDensity.lean 6 declarations
- LocalGradientParallelogram.lean 13 declarations
- LocalGradientParallelogramCheeger.lean 4 declarations
- LocalizedFisher.lean 2 declarations
- LogAddTwoSqrt.lean 6 declarations
- MulLogFenchel.lean 5 declarations
- NonnegativeParallelogram.lean 12 declarations
- PolarAddFourParallelograms.lean 1 declarations
- QuadraticEntropyPairing.lean 3 declarations
- RadialEntropy.lean 5 declarations
- ReducedEntropy.lean 8 declarations
- ReducedEntropyDual.lean 4 declarations
- RegularizedEntropyIntegrable.lean 3 declarations
- RenormalizedEntropy.lean 5 declarations
- RenyiKernel.lean 12 declarations
- ScalarEntropyLog.lean 4 declarations
- SmoothDensity.lean 10 declarations
- SobolevFisher.lean 2 declarations
- StrongEntropyConfinement.lean 1 declarations
- TauDensityLinearLower.lean 6 declarations
- TendstoRenyiGap.lean 2 declarations
- TruncatedLog.lean 21 declarations
- WeightedParallelogramIntegral.lean 1 declarations
- ZeroDensity.lean 21 declarations