OAI/Analysis/FreeEntropy/
1606 declarations, 0 contain sorry, 0 declared as axioms; 153 files
Files
- ActualTuple.lean 36 declarations
- Basic.lean 186 declarations
- BilinearNet.lean 4 declarations
- BlockEnsembleLower.lean 3 declarations
- BlockEvent.lean 7 declarations
- BlockEventLower.lean 5 declarations
- BlockGaussianQuantitative.lean 9 declarations
- CompactIntegration.lean 2 declarations
- ComplexPolynomialFunctions.lean 23 declarations
- CoordinateIBP.lean 1 declarations
- CoordinateMask.lean 7 declarations
- CumulantBound.lean 1 declarations
- CumulantResidual.lean 8 declarations
- CumulantSeries.lean 33 declarations
- CutoffSeparation.lean 3 declarations
- CyclicSeries.lean 26 declarations
- EmbeddedSeries.lean 15 declarations
- EntropyDeficit.lean 6 declarations
- EntropyFiniteness.lean 7 declarations
- EntropyIntegral.lean 6 declarations
- EntropyReal.lean 8 declarations
- EquidiscreteSignal.lean 17 declarations
- FatouFlow.lean 2 declarations
- FisherDeficit.lean 6 declarations
- FisherLaw.lean 9 declarations
- FisherLiminf.lean 3 declarations
- FisherResidual.lean 5 declarations
- FisherTestLimit.lean 6 declarations
- FisherVariational.lean 15 declarations
- FlowSeparation.lean 5 declarations
- FreeEntropyFlow.lean 7 declarations
- FreeMatrixModels.lean 2 declarations
- GUEBounds.lean 8 declarations
- GUEConcentration.lean 5 declarations
- GUECovariance.lean 3 declarations
- GUEDerivative.lean 7 declarations
- GUEFock.lean 4 declarations
- GUEFreeLaw.lean 5 declarations
- GUEGradient.lean 3 declarations
- GUELimit.lean 8 declarations
- GUEMoments.lean 6 declarations
- GUEOperatorTail.lean 4 declarations
- GUESelection.lean 5 declarations
- GUEStein.lean 5 declarations
- GaussianAffineVolume.lean 1 declarations
- GaussianBlockTail.lean 10 declarations
- GaussianConvolution.lean 15 declarations
- GaussianConvolutionBounds.lean 6 declarations
- GaussianCorrection.lean 5 declarations
- GaussianCrossEntropy.lean 7 declarations
- GaussianDeBruijn.lean 7 declarations
- GaussianDecay.lean 3 declarations
- GaussianDensity.lean 7 declarations
- GaussianDifferential.lean 9 declarations
- GaussianEntropyEvent.lean 5 declarations
- GaussianEntropyIntegrability.lean 7 declarations
- GaussianFlow.lean 6 declarations
- GaussianHermite.lean 21 declarations
- GaussianIBP.lean 6 declarations
- GaussianKernel.lean 10 declarations
- GaussianL2Limit.lean 5 declarations
- GaussianLinearTail.lean 6 declarations
- GaussianMvStein.lean 6 declarations
- GaussianProjectionMoments.lean 4 declarations
- GaussianRegularity.lean 8 declarations
- GaussianScore.lean 3 declarations
- GaussianVolume.lean 5 declarations
- GeometricTail.lean 7 declarations
- HeatAnalysis.lean 10 declarations
- HeatCumulants.lean 7 declarations
- HeatTensor.lean 8 declarations
- L2Convergence.lean 7 declarations
- LinearSeries.lean 19 declarations
- Main.lean 1 declarations
- MatrixBasis.lean 6 declarations
- MatrixBasisChart.lean 1 declarations
- MatrixBilinear.lean 9 declarations
- MatrixBlockEnergy.lean 6 declarations
- MatrixBlocks.lean 8 declarations
- MatrixBounds.lean 7 declarations
- MatrixChart.lean 9 declarations
- MatrixChartInverse.lean 2 declarations
- MatrixFisherLiminf.lean 5 declarations
- MatrixFisherTest.lean 7 declarations
- MatrixFlow.lean 8 declarations
- MatrixHeatLaw.lean 4 declarations
- MatrixHeatLawMoments.lean 6 declarations
- MatrixHeatLimit.lean 2 declarations
- MatrixHilbertSchmidt.lean 17 declarations
- MatrixOperator.lean 15 declarations
- MatrixParseval.lean 4 declarations
- MatrixPolynomial.lean 13 declarations
- MatrixPolynomialNorm.lean 6 declarations
- MatrixReparam.lean 5 declarations
- MatrixRotationBounds.lean 5 declarations
- MatrixScoreWords.lean 10 declarations
- MatrixSpectralMoments.lean 9 declarations
- MatrixTestPolynomial.lean 5 declarations
- MatrixWordDerivative.lean 12 declarations
- MicrostatesHeat.lean 5 declarations
- MicrostatesLogLower.lean 1 declarations
- MicrostatesLower.lean 3 declarations
- MicrostatesSelection.lean 9 declarations
- MixedGaussianSeries.lean 20 declarations
- Model.lean 19 declarations
- ModelFlowLimit.lean 3 declarations
- MonomialSeries.lean 14 declarations
- NoiseRotation.lean 5 declarations
- NoiseTensor.lean 16 declarations
- NormalLaw.lean 7 declarations
- OptionSeries.lean 10 declarations
- OrthogonalExpansion.lean 8 declarations
- PolynomialFunctions.lean 18 declarations
- PolynomialGrowth.lean 5 declarations
- RandomHeatConvergence.lean 3 declarations
- RandomHeatMoments.lean 5 declarations
- RandomMatrixConvergence.lean 4 declarations
- RealTail.lean 4 declarations
- SemicircularSeries.lean 18 declarations
- SeriesAnalytic.lean 18 declarations
- SeriesNorm.lean 17 declarations
- SeriesSummability.lean 5 declarations
- SeriesWeights.lean 14 declarations
- Signal.lean 20 declarations
- SignalCovariance.lean 16 declarations
- SignalSeries.lean 9 declarations
- SpectralBlockMask.lean 5 declarations
- SpectralClustering.lean 6 declarations
- SpectralMatrixProducer.lean 1 declarations
- SpectralParameters.lean 12 declarations
- SpectralTestFunctions.lean 18 declarations
- TensorConcat.lean 30 declarations
- TensorFreeness.lean 38 declarations
- TensorGradient.lean 8 declarations
- TensorHermite.lean 17 declarations
- TensorLaw.lean 13 declarations
- TensorMatrices.lean 7 declarations
- TensorMatrixModels.lean 1 declarations
- TensorPoincare.lean 10 declarations
- TerminalGaussian.lean 2 declarations
- TotalSecond.lean 9 declarations
- TracialRealization.lean 84 declarations
- TwoNoiseFisher.lean 22 declarations
- UniformConvergence.lean 2 declarations
- UniformMicrostateTests.lean 1 declarations
- VectorSeries.lean 30 declarations
- VolumetricNet.lean 2 declarations
- WickBound.lean 3 declarations
- WickCoefficients.lean 10 declarations
- WickSeries.lean 8 declarations
- WickTensor.lean 5 declarations
- WordLinearLaw.lean 7 declarations
- WordSeries.lean 41 declarations