OAI/GroupTheory/SimpleAmenable/RandomFields/
364 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- AffineDensityDerivative.lean 6 declarations
- AffineGeneratorIntegrability.lean 9 declarations
- AffineNoiseEnergy.lean 20 declarations
- AlignedCovariance.lean 2 declarations
- AveragingAffinePairs.lean 14 declarations
- AveragingUniformCovariance.lean 9 declarations
- CanonicalPolygonCovariance.lean 3 declarations
- CompactSignalEnergy.lean 11 declarations
- CovarianceLimit.lean 7 declarations
- FieldHS.lean 14 declarations
- FieldSignalData.lean 7 declarations
- FiniteCovariance.lean 6 declarations
- FiniteFieldConcentration.lean 3 declarations
- FiniteLawDistance.lean 11 declarations
- FiniteOrthogonalEnergy.lean 25 declarations
- FlagAveragingMatrices.lean 19 declarations
- FlagSignalEnergy.lean 10 declarations
- FormalLawCovariance.lean 3 declarations
- HellingerDistance.lean 11 declarations
- JointBitField.lean 10 declarations
- MatrixDensityCalculus.lean 10 declarations
- NoiseContinuity.lean 18 declarations
- NoiseTensor.lean 13 declarations
- PeriodizationCovariance.lean 5 declarations
- PolygonApproxIdentity.lean 11 declarations
- PolygonCovarianceEnergy.lean 8 declarations
- PrimitiveCovariance.lean 16 declarations
- RecoveredConstantCovariance.lean 7 declarations
- SignalCutoff.lean 7 declarations
- SignalGoodRows.lean 11 declarations
- SignalRemainder.lean 9 declarations
- ThresholdField.lean 13 declarations
- TransportEstimate.lean 7 declarations
- UniformThresholdCDF.lean 14 declarations
- WeightedAveragingError.lean 15 declarations