OAI/Probability/StrongRayleigh/
929 declarations, 0 contain sorry, 0 declared as axioms; 133 files
Files
- AffineSlopeStability.lean 5 declarations
- AsymptoticReadout.lean 10 declarations
- Basic.lean 1 import, no declarations
- BinaryProjective.lean 4 declarations
- BivariateStability.lean 5 declarations
- BrownianBridge.lean 8 declarations
- BrownianBridgeSignal.lean 2 declarations
- BrownianContinuability.lean 2 declarations
- BrownianExistence.lean 7 declarations
- BrownianKolmogorov.lean 8 declarations
- BrownianObservationSufficiency.lean 6 declarations
- BrownianObservedEndpoints.lean 2 declarations
- BrownianPathLaw.lean 11 declarations
- BrownianReadout.lean 4 declarations
- BrownianStochasticContinuity.lean 4 declarations
- BrownianSublinear.lean 4 declarations
- CanonicalInnovationSampler.lean 4 declarations
- CantorProjective.lean 18 declarations
- CharacteristicLaw.lean 5 declarations
- CharacteristicTaylor.lean 3 declarations
- ConditionalCharacteristic.lean 2 declarations
- ConditionalTaylor.lean 4 declarations
- ContinuousModification.lean 4 declarations
- ContinuousPathInput.lean 6 declarations
- ContinuousPathLaw.lean 16 declarations
- CountableAssembly.lean 5 declarations
- CountableProjectiveReindex.lean 10 declarations
- CovarianceRow.lean 3 declarations
- CylindricalIndependence.lean 2 declarations
- DPPReindex.lean 6 declarations
- DecoderUniqueness.lean 7 declarations
- DensePathExtension.lean 22 declarations
- DensityBayes.lean 5 declarations
- DensityPosterior.lean 5 declarations
- DeterminantalUniqueness.lean 3 declarations
- DyadicTail.lean 8 declarations
- DyadicTimes.lean 11 declarations
- ElementaryResponse.lean 9 declarations
- FiniteDPPExistence.lean 1 declarations
- FiniteDPPGenerating.lean 6 declarations
- FiniteDPPStability.lean 2 declarations
- FiniteDPPWeights.lean 4 declarations
- FiniteEndpointPosterior.lean 15 declarations
- FiniteFieldTilt.lean 15 declarations
- FiniteGaussianCharacteristic.lean 3 declarations
- FiniteMarginal.lean 1 declarations
- FiniteMarginalObservation.lean 14 declarations
- FiniteResponseAssembly.lean 1 declarations
- GaussianAtomObservation.lean 3 declarations
- GaussianFieldCharacteristic.lean 1 declarations
- GaussianLinearCombination.lean 6 declarations
- GaussianMomentBounds.lean 16 declarations
- GaussianObservation.lean 10 declarations
- GaussianPerturbation.lean 3 declarations
- GaussianReindex.lean 7 declarations
- GeneratingSlice.lean 26 declarations
- GroupBrownianPosterior.lean 8 declarations
- GroupDrift.lean 8 declarations
- GroupDriftPosterior.lean 3 declarations
- GroupExhaustion.lean 15 declarations
- GroupFactorAssembly.lean 3 declarations
- GroupFactorProof.lean 2 declarations
- GroupInnovationInverse.lean 11 declarations
- GroupSampler.lean 2 declarations
- IIDAction.lean 13 declarations
- IIDNoiseIncrements.lean 8 declarations
- InclusionUniqueness.lean 9 declarations
- IndependentAtomLaw.lean 4 declarations
- IndependentAtomObservation.lean 5 declarations
- IndependentConditioning.lean 8 declarations
- InnovationAdapted.lean 11 declarations
- InnovationAnalysis.lean 16 imports, no declarations
- InnovationCharacteristic.lean 10 declarations
- InnovationCharacteristicProcess.lean 1 declarations
- InnovationContinuity.lean 2 declarations
- InnovationCorrection.lean 15 declarations
- InnovationErrorScale.lean 5 declarations
- InnovationFiniteLaw.lean 2 declarations
- InnovationInverse.lean 8 declarations
- InnovationMean.lean 9 declarations
- InnovationPathCriterion.lean 2 declarations
- InnovationProcessLaw.lean 7 declarations
- InnovationSampler.lean 2 declarations
- LimsupDrift.lean 8 declarations
- LocalCharacteristicBrownian.lean 2 declarations
- LocalDyadicContinuity.lean 25 declarations
- LocalInnovation.lean 3 declarations
- Main.lean 6 declarations
- MarginalBase.lean 5 declarations
- MarginalBridge.lean 3 declarations
- MatrixStability.lean 8 declarations
- MixedDeterminant.lean 6 declarations
- Model.lean 21 declarations
- NoisePastIndependence.lean 6 declarations
- ObservationHistory.lean 8 declarations
- ObservationNoise.lean 16 declarations
- ObservationNoiseReal.lean 10 declarations
- ObservationPastIndependence.lean 5 declarations
- PairCoefficients.lean 11 declarations
- PathRealization.lean 27 declarations
- PathSamplerTransfer.lean 5 declarations
- PerturbedMoments.lean 10 declarations
- PickSquareRoot.lean 6 declarations
- PolynomialPick.lean 5 declarations
- PosteriorAnalysis.lean 11 imports, no declarations
- PosteriorLimit.lean 9 declarations
- PreBrownianExistence.lean 3 declarations
- ProjectiveNatExtension.lean 2 declarations
- RationalBrownian.lean 19 declarations
- RayleighOffDiagonal.lean 1 declarations
- RayleighResponse.lean 1 declarations
- ReferenceEndpointLaw.lean 6 declarations
- ReferenceGroupPosterior.lean 3 declarations
- ReferenceInnovationLaw.lean 13 declarations
- ReferenceNoise.lean 12 declarations
- ReferenceObservation.lean 24 declarations
- ResponseDerivative.lean 4 declarations
- ResponseDirectional.lean 4 declarations
- ResponseLipschitz.lean 2 declarations
- RightHalfPlaneDerivative.lean 3 declarations
- StabilitySpecialization.lean 3 declarations
- StableUnivariate.lean 5 declarations
- StableWronskian.lean 2 declarations
- StandardBorelCountable.lean 3 declarations
- StandardBorelProjective.lean 4 declarations
- TiltContinuity.lean 8 declarations
- TiltPartition.lean 4 declarations
- TiltScaling.lean 5 declarations
- Translation.lean 5 declarations
- TranslationAssembly.lean 5 declarations
- TwoCoordinateCoefficients.lean 14 declarations
- UniformSource.lean 3 declarations
- WeightedLocalInnovation.lean 19 declarations