OAI/NumberTheory/Jacobsthal/Probability/
1065 declarations, 0 contain sorry, 0 declared as axioms; 74 files
Files
- ActualCouplingError.lean 1 declarations
- ActualCouplingUpdates.lean 109 declarations
- ActualUnlistedEvent.lean 1 declarations
- ArrivalKernelGeometry.lean 69 declarations
- CanonicalPairHitEvents.lean 13 declarations
- CanonicalPairVisitLaw.lean 9 declarations
- CemeteryHistoryLaw.lean 37 declarations
- CompletedMarkEvents.lean 13 declarations
- CouplingEvent.lean 6 declarations
- CouplingLabelEvents.lean 17 declarations
- EvenThresholdEvent.lean 14 declarations
- FallingFactorialProbability.lean 4 declarations
- FiniteHistoryPairLaw.lean 7 declarations
- FiniteKernelResolvent.lean 4 declarations
- FirstHitKernels.lean 80 declarations
- FullBoxVarianceGeometry.lean 2 declarations
- FullPatternVariance.lean 8 declarations
- GenuineMarkedVisit.lean 6 declarations
- GeometricCostLaws.lean 17 declarations
- HarmonicPrefixKernel.lean 23 declarations
- HighPrefixKernel.lean 11 declarations
- HorizontalBoundaryMarks.lean 4 declarations
- JointMarkedWord.lean 3 declarations
- KloostermanFourthMoment.lean 3 declarations
- MarkedBeginningKernel.lean 19 declarations
- MarkedCostHitReduction.lean 58 declarations
- MarkedCostSublaws.lean 20 declarations
- MarkedOccurrenceProbability.lean 1 declarations
- MarkedReturnKernel.lean 32 declarations
- MarkedStripTotal.lean 9 declarations
- MarkedVisitGeometry.lean 68 declarations
- MomentIndicators.lean 4 declarations
- MovingMarkedWindow.lean 40 declarations
- OrderedAffineMoment.lean 11 declarations
- OrderedWindowKernel.lean 9 declarations
- OrdinaryMarkedWindow.lean 37 declarations
- PairedDrift.lean 8 declarations
- PaperSubsetTagEvent.lean 3 declarations
- PaperTagEventInclusion.lean 4 declarations
- PhysicalMarkedRecord.lean 9 declarations
- PreciseIncidenceMoment.lean 2 declarations
- RawEvenMarkedHit.lean 9 declarations
- RawFirstPrefixLaw.lean 7 declarations
- RawMarkedVisitGeometry.lean 12 declarations
- RawMarkedWords.lean 5 declarations
- RealExceptionalMarks.lean 5 declarations
- RegularStoppedEvent.lean 4 declarations
- RepeatedPairEvents.lean 6 declarations
- RepeatedPairProbability.lean 9 declarations
- RepeatedWordEvents.lean 4 declarations
- RetainedCompactEvent.lean 1 declarations
- RieszKernelBounds.lean 6 declarations
- SecondLossKernel.lean 5 declarations
- SigmaFamilyKernel.lean 7 declarations
- SingletonEventMass.lean 3 declarations
- SourceCompactCoupling.lean 15 declarations
- SourceFullEventCount.lean 7 declarations
- SourceIsolatedProbability.lean 1 declarations
- SourceMarkedStopping.lean 10 declarations
- SourceMarkedWords.lean 11 declarations
- SourceThresholdCoupling.lean 14 declarations
- SourceTransitionSupport.lean 3 declarations
- StableFiniteVariance.lean 6 declarations
- StableModelMoments.lean 2 declarations
- StableSourceVariance.lean 7 declarations
- StandardDeficitMoments.lean 4 declarations
- StateKernelInvariance.lean 26 declarations
- SubMarkovFlagPowers.lean 10 declarations
- SuccessfulMarkedCoordinates.lean 4 declarations
- ThirdInnerKernel.lean 19 declarations
- TransitionKernels.lean 30 declarations
- TwoSidedThresholdKernel.lean 8 declarations
- UncappedCompactEvent.lean 1 declarations
- UniformMoment.lean 9 declarations