OAI/Probability/FreeIsing/Posterior/
642 declarations, 0 contain sorry, 0 declared as axioms; 82 files
Files
- ArrayPosteriorCovarianceStationarity.lean 9 declarations
- ArrayPosteriorStationarity.lean 17 declarations
- BranchObservationRegression.lean 9 declarations
- ChildObservationRegression.lean 1 declarations
- CompensatorStopping.lean 16 declarations
- ComponentObservationDecomposition.lean 1 declarations
- ComponentObservationIndependence.lean 3 declarations
- ComponentObservationRegression.lean 2 declarations
- ComponentPosteriorStationarity.lean 6 declarations
- ComponentPosteriorTilt.lean 3 declarations
- ConePosteriorRegression.lean 1 declarations
- ContinuousObservationHistory.lean 14 declarations
- ContinuousPosteriorInterior.lean 4 declarations
- ContinuousPosteriorNaturality.lean 2 declarations
- ContinuousPosteriorStopping.lean 1 declarations
- CopyBounds.lean 7 declarations
- DerivativeBounds.lean 16 declarations
- FieldCalculus.lean 33 declarations
- FieldL2Limit.lean 8 declarations
- FieldMoments.lean 9 declarations
- Fields.lean 13 declarations
- FilteringArrayCrossLimit.lean 2 declarations
- FilteringCrossEnergy.lean 10 declarations
- FilteringCrossLimit.lean 1 declarations
- FilteringRepresentationClosure.lean 16 declarations
- FilteringSimpleCrossEnergy.lean 3 declarations
- FiniteIsingFilteringRepresentation.lean 20 declarations
- FinitePosterior.lean 24 declarations
- FinitePosteriorVarianceInverse.lean 12 declarations
- FusionSup.lean 1 declarations
- GaussianEnergy.lean 11 declarations
- GaussianEnergyIntegral.lean 1 declarations
- GaussianGradient.lean 11 declarations
- GaussianTesting.lean 5 declarations
- GaussianTimeDerivative.lean 10 declarations
- InfinitePosteriorField.lean 10 declarations
- InteriorLocalization.lean 20 declarations
- LatentObservationIndependence.lean 2 declarations
- Limit.lean 5 declarations
- LipschitzObservationDerivative.lean 5 declarations
- MixedFilteringCrossLimit.lean 1 declarations
- NormalizedObservationRowConvergence.lean 9 declarations
- NormalizedPosteriorLimit.lean 8 declarations
- NormalizedPosteriorRowConvergence.lean 5 declarations
- ObservationFactorRecovery.lean 4 declarations
- ObservationLawSpectral.lean 8 declarations
- ObservationMoments.lean 13 declarations
- ObservationStepApproximation.lean 9 declarations
- PathPosteriorResponse.lean 17 declarations
- PlantedArrayCrossEnergy.lean 2 declarations
- PlantedBridge.lean 2 declarations
- PlantedBridgeInfinite.lean 3 declarations
- PlantedBridgeVector.lean 4 declarations
- PlantedEdgeRegression.lean 3 declarations
- PlantedStationarity.lean 9 declarations
- PlantedSufficiency.lean 1 declarations
- PlantedSufficiencyVector.lean 4 declarations
- PlantedSymmetry.lean 15 declarations
- ProgressiveIsingPosterior.lean 11 declarations
- ProjectedObservationRecovery.lean 7 declarations
- ResponseCapRate.lean 5 declarations
- ResponseTruncation.lean 10 declarations
- SelectedPosteriorChannels.lean 3 declarations
- SelectedPosteriorField.lean 4 declarations
- SelectedPosteriorLimit.lean 5 declarations
- SelectedPosteriorStationarity.lean 11 declarations
- SelectedPosteriorSymmetry.lean 8 declarations
- Smooth.lean 5 declarations
- SqrtObservationDerivative.lean 4 declarations
- Stationarity.lean 8 declarations
- StatisticTilt.lean 3 declarations
- StoppingTimes.lean 27 declarations
- StrictPosteriorIncrements.lean 5 declarations
- SubsetPosteriorSymmetry.lean 4 declarations
- Symmetry.lean 11 declarations
- TimeL2Continuity.lean 5 declarations
- UniformTimeApproximation.lean 8 declarations
- VarianceInverse.lean 15 declarations
- VarianceInverseLimit.lean 4 declarations
- VarianceInverseTimeLimit.lean 3 declarations
- VarianceTimeIntegral.lean 6 declarations
- VarianceTruncation.lean 9 declarations