OAI/Probability/Perceptron/Variational/
2224 declarations, 0 contain sorry, 0 declared as axioms; 189 files
Files
- AmplitudeConvex.lean 19 declarations
- AnnealedIBP.lean 5 declarations
- AtomicBranches.lean 7 declarations
- AtomicPairVisitLaw.lean 12 declarations
- BackwardScore.lean 28 declarations
- BcfEvalRingHom.lean 18 declarations
- BlockFocus.lean 10 declarations
- BoundaryEstimate.lean 7 declarations
- BoundedC1.lean 29 declarations
- BoundedGibbsDerivative.lean 4 declarations
- BoundedLeafRestoration.lean 3 declarations
- CappedAContinuity.lean 6 declarations
- CompactEnvelope.lean 5 declarations
- CompactGGDensity.lean 8 declarations
- CompactGGEvents.lean 14 declarations
- CompactGGFiniteCode.lean 12 declarations
- CompactJointMonomials.lean 10 declarations
- CompactRestorationWitness.lean 11 declarations
- CompactScalarGG.lean 5 declarations
- CompactTripleGG.lean 11 declarations
- Contact.lean 7 declarations
- ContactDensity.lean 1 declarations
- ContactFatou.lean 9 declarations
- ContactGGRate.lean 13 declarations
- ContactTail.lean 2 declarations
- ConvexUniform.lean 11 declarations
- CountMixtureVariance.lean 2 declarations
- CountableGaussianFullIBP.lean 1 declarations
- CountableGaussianIBP.lean 3 declarations
- CountableGaussianResampling.lean 3 declarations
- CountableMarkedDiagonal.lean 15 declarations
- CountableSingleRestoration.lean 4 declarations
- CoupledDual.lean 10 declarations
- CouplingAffine.lean 7 declarations
- CouplingDerivative.lean 2 declarations
- CouplingKernel.lean 30 declarations
- CovarianceMatrix.lean 40 declarations
- DecoratedFocus.lean 7 declarations
- DecoratedShapeLaw.lean 9 declarations
- DecoratedTiltTotal.lean 12 declarations
- DensityDerivative.lean 7 declarations
- DensityLipschitz.lean 13 declarations
- DepthBlock.lean 7 declarations
- DepthGG.lean 5 declarations
- DepthLaw.lean 18 declarations
- DiagonalDeviation.lean 10 declarations
- DilationExpansion.lean 7 declarations
- EnergyMean.lean 4 declarations
- EnrichedMoments.lean 9 declarations
- EnrichedUniformBounds.lean 20 declarations
- EnrichedVarianceBound.lean 17 declarations
- EntropicHeat.lean 15 declarations
- EntropicParameter.lean 14 declarations
- Entropy.lean 4 declarations
- Field.lean 9 declarations
- FieldContinuity.lean 16 declarations
- FieldDerivative.lean 11 declarations
- FieldRounding.lean 25 declarations
- FieldWord.lean 20 declarations
- FiniteFieldModel.lean 15 declarations
- FiniteGaussianRow.lean 18 declarations
- FixedCount.lean 19 declarations
- FocusedRootProbability.lean 4 declarations
- FocusedSampleLaw.lean 9 declarations
- FocusedShapeProbability.lean 26 declarations
- FocusedVisit.lean 3 declarations
- GaussianAbsoluteEnergyBound.lean 3 declarations
- GaussianAverage.lean 33 declarations
- GaussianBackward.lean 10 declarations
- GaussianBlock.lean 5 declarations
- GaussianBoltzmann.lean 19 declarations
- GaussianComparison.lean 10 declarations
- GaussianCoupling.lean 13 declarations
- GaussianCovarianceDerivative.lean 13 declarations
- GaussianEnergyMoments.lean 13 declarations
- GaussianGibbsContinuity.lean 7 declarations
- GaussianGibbsEnergy.lean 8 declarations
- GaussianLinearStability.lean 2 declarations
- GaussianLinearVariance.lean 3 declarations
- GaussianMarkRecursion.lean 15 declarations
- GaussianWordStability.lean 2 declarations
- GibbsRestoration.lean 4 declarations
- GlobalContact.lean 11 declarations
- GlobalContactLimit.lean 12 declarations
- GridGap.lean 4 declarations
- HeatGrid.lean 24 declarations
- HeatLogBCF.lean 30 declarations
- HeatTilt.lean 38 declarations
- HeightWord.lean 17 declarations
- IndexedAncestry.lean 18 declarations
- IndexedChildLaw.lean 3 declarations
- IndexedDiagonalField.lean 14 declarations
- IndexedFractionalLog.lean 4 declarations
- IndexedGaussianCovariance.lean 12 declarations
- IndexedGaussianCovarianceLaw.lean 12 declarations
- IndexedGaussianMarks.lean 12 declarations
- IndexedLeafTotal.lean 8 declarations
- IndexedMarkProduct.lean 6 declarations
- IndexedObservableTransport.lean 8 declarations
- IndexedPathCorrelation.lean 1 declarations
- IndexedTiltedRegular.lean 6 declarations
- IndexedTwoShape.lean 5 declarations
- IndexedVisit.lean 21 declarations
- InfinitePiSplit.lean 2 declarations
- IntegrableGibbs.lean 13 declarations
- IntegrableProdConditionalSquare.lean 4 declarations
- IntegratedConvex.lean 15 declarations
- IntegratedThermal.lean 4 declarations
- KernelProductIntegral.lean 1 declarations
- LabelPairTestValue.lean 15 declarations
- LabelProfilePairReference.lean 3 declarations
- LabelProfileReference.lean 15 declarations
- LabelProfileReferenceFull.lean 6 declarations
- LabelProfileSingleReference.lean 8 declarations
- LabelReference.lean 6 declarations
- LabelReferenceValue.lean 5 declarations
- LabelResponse.lean 7 declarations
- LabelRestorationKernel.lean 24 declarations
- LabelRestorationMoments.lean 15 declarations
- LabelRestorationMoments2.lean 17 declarations
- LabelRestorationPair.lean 15 declarations
- LabelRestorationSingle.lean 5 declarations
- LabelRestoredValue.lean 10 declarations
- LabelSingleRestoredValue.lean 14 declarations
- LabelThermalLaw.lean 10 declarations
- LabelValue.lean 11 declarations
- LeafGibbsMarginal.lean 3 declarations
- LeafMarginalLaw.lean 2 declarations
- LevelTrialApprox.lean 13 declarations
- LocalMaxSecondDerivNonpos.lean 18 declarations
- MarkTiltKernel.lean 5 declarations
- MarkedBlockParameter.lean 11 declarations
- MarkedGraphLaw.lean 4 declarations
- MarkedTangentCanonical.lean 7 declarations
- MarkedTotalBiasedLaw.lean 21 declarations
- MarkedVariance.lean 3 declarations
- MeasurableVariance.lean 1 declarations
- NonlinearDirectionIBP.lean 1 declarations
- NormSquareBand.lean 37 declarations
- OrderedCode.lean 14 declarations
- ParameterResampling.lean 7 declarations
- PiMarkLaw.lean 27 declarations
- PointedShape.lean 5 declarations
- ProbabilityMaps.lean 10 declarations
- ProductMarkLaw.lean 35 declarations
- PureLabel.lean 14 declarations
- QuadraticContactRemainders.lean 3 declarations
- QuantileLimit.lean 10 declarations
- QuantileReference.lean 6 declarations
- QuantileSingleReference.lean 1 declarations
- QuantileUpperTail.lean 22 declarations
- QuantitativeGG.lean 4 declarations
- RestorationMoments.lean 5 declarations
- RightDerivativeIntegral.lean 7 declarations
- RoundedCoupling.lean 7 declarations
- RoundedLaw.lean 9 declarations
- RoundedMarkedReference.lean 6 declarations
- RoundedMarkedSelection.lean 20 declarations
- RoundedPairCoefficients.lean 7 declarations
- Shape.lean 10 declarations
- ShapeProbability.lean 9 declarations
- ShapeSampleLaw.lean 17 declarations
- ShellBridge.lean 13 declarations
- SingleRestorationLaw.lean 4 declarations
- StableLaplaceConstant.lean 33 declarations
- StableLogIntensity.lean 30 declarations
- StableMassKernel.lean 24 declarations
- StableTotalBiasedLaw.lean 40 declarations
- StationaryExistence.lean 22 declarations
- StepDual.lean 9 declarations
- StepEntropy.lean 30 declarations
- StepStationary.lean 7 declarations
- SynchronizedLimit.lean 11 declarations
- TangentConsistency.lean 5 declarations
- TensorFeatures.lean 23 declarations
- TiltMeanCenteredAbsSq.lean 6 declarations
- TiltedPathDiagonal.lean 20 declarations
- TiltedPathProduct.lean 4 declarations
- TiltedVisitKernel.lean 22 declarations
- TiltedVisitKernelLaw.lean 13 declarations
- Trial.lean 41 declarations
- TripleIndex.lean 35 declarations
- TripleRootRegroup.lean 2 declarations
- UnboundedContact.lean 8 declarations
- UniformGrid.lean 16 declarations
- UniformQuantileCells.lean 23 declarations
- UniformUncapLimit.lean 1 declarations
- UpperContact.lean 4 declarations
- VarianceProdMemLp.lean 9 declarations