`OAI/Probability/Ballisticity/Estimates/`

2718 declarations, 0 contain sorry, 0 declared as axioms; 266 files

Files

AdaptiveFailureWeights.lean 14 declarations
AeMaximalSquare.lean 8 declarations
AlignedRecordPrefix.lean 31 declarations
AllIndexMarks.lean 4 declarations
AllLayerOccupation.lean 10 declarations
AllOffsetConsistency.lean 7 declarations
AnchorFrameReference.lean 7 declarations
AnchorMoments.lean 14 declarations
BadDropMoment.lean 2 declarations
BadOccupationLimit.lean 9 declarations
BadStageMoment.lean 4 declarations
BindIntegral.lean 1 declarations
BoundaryDecorrelation.lean 7 declarations
BoundaryGapReplacement.lean 3 declarations
BoundarySuffixIdentity.lean 8 declarations
BoundedAnchorAverage.lean 4 declarations
BudgetAdapted.lean 23 declarations
BudgetAlgebra.lean 11 declarations
BudgetClipping.lean 12 declarations
BudgetEndpoint.lean 17 declarations
BudgetLoss.lean 3 declarations
BudgetMeasurable.lean 21 declarations
BudgetNormalize.lean 13 declarations
BudgetThreat.lean 23 declarations
Buffer.lean 4 declarations
BufferChanceData.lean 7 declarations
BufferChildNode.lean 12 declarations
BufferExcess.lean 2 declarations
BufferFirstFailure.lean 10 declarations
BufferRestorationScript.lean 17 declarations
BufferRootRetention.lean 3 declarations
BufferStageCount.lean 7 declarations
BufferStagePacket.lean 4 declarations
BufferStageSuccess.lean 7 declarations
BufferTree.lean 16 declarations
CappedExp.lean 13 declarations
CappedLoss.lean 9 declarations
CappedMomentTransfer.lean 12 declarations
Cell.lean 7 declarations
CellAttempt.lean 10 declarations
CellBadEvent.lean 7 declarations
CellCertificates.lean 6 declarations
CellExhaustion.lean 4 declarations
CellFailure.lean 5 declarations
CellRadiusComparison.lean 11 declarations
CellSchedule.lean 28 declarations
CharacteristicProductLaw.lean 8 declarations
CharacteristicTaylor.lean 13 declarations
ClassFinset.lean 5 declarations
ClassMoment.lean 3 declarations
ClassSelection.lean 8 declarations
ClippedAbsThreeHalves.lean 8 declarations
ClippedInverse.lean 33 declarations
ClippedThreeHalves.lean 4 declarations
ClippingTime.lean 3 declarations
ClosedEmbeddingWeak.lean 1 declarations
CommonBoundaryRestart.lean 24 declarations
CommonLayer.lean 14 declarations
CommonOccupationBound.lean 5 declarations
CommonOffset.lean 11 declarations
CommonTrueRecord.lean 23 declarations
CommonWidthProcess.lean 19 declarations
CommonWordIncrement.lean 44 declarations
CommonWordWidth.lean 22 declarations
ConditionalLawTests.lean 9 declarations
ConfinementTemplates.lean 1 declarations
ConvolutionCentersClose.lean 4 declarations
CountableProdBind.lean 7 declarations
CurveCenter.lean 2 declarations
CurveEndpointLaw.lean 8 declarations
CurvePolicy.lean 13 declarations
CurvePolicyAlignment.lean 9 declarations
CurvePolicyAverageMoment.lean 8 declarations
CurvePolicyLateral.lean 9 declarations
CurvePolicyMaximal.lean 11 declarations
CurvePolicyPMF.lean 13 declarations
CurvePrefix.lean 17 declarations
CurveShortBlock.lean 3 declarations
CurveWordDisjoint.lean 5 declarations
DensityTransfer.lean 3 declarations
DescendingTrials.lean 6 declarations
DifferentiableExp.lean 6 declarations
DirectBridge.lean 12 declarations
DominatedTranslationBounded.lean 2 declarations
Dust.lean 15 declarations
EndpointPrefix.lean 10 declarations
EndpointPrefixConditionedReal.lean 6 declarations
EventRate.lean 2 declarations
FavorablePairFraction.lean 10 declarations
FiniteClasses.lean 3 declarations
FinitePastDecorrelation.lean 11 declarations
FinitePolicyFailure.lean 7 declarations
FinitePolicyPMF.lean 6 declarations
FiniteStage.lean 8 declarations
FirstBelow.lean 17 declarations
FirstHighRecord.lean 20 declarations
FirstWordEvent.lean 37 declarations
FixedPairSuffix.lean 28 declarations
FluctuationScaleUpperMultiple.lean 10 declarations
FullCapTransfer.lean 6 declarations
GaussianAbsTail.lean 7 declarations
GaussianPiReal.lean 5 declarations
GlobalContinuation.lean 4 declarations
GlobalProfile.lean 20 declarations
GlobalTuple.lean 6 declarations
GridLinear.lean 9 declarations
GridOccupation.lean 12 declarations
GridOscillation.lean 34 declarations
GridTrials.lean 16 declarations
HighRecordCount.lean 6 declarations
IidDifferenceCenteredHalf.lean 6 declarations
IidListProcess.lean 19 declarations
IndependentDyadic.lean 16 declarations
IndependentPairLaw.lean 26 declarations
IndependentRandomTestBound.lean 3 declarations
IndependentRecenterMap.lean 6 declarations
InputMarginal.lean 3 declarations
IntegerMedian.lean 23 declarations
InteriorPairMeasureExt.lean 4 declarations
JointMeshPhase.lean 4 declarations
JointPastMoments.lean 14 declarations
JointPastRestart.lean 15 declarations
LateMoment.lean 4 declarations
LayerPairTruthEventMono.lean 5 declarations
ListPrefixSum.lean 3 declarations
LocalRadiusOrder.lean 5 declarations
LocalStoppedSplice.lean 39 declarations
LowerClip.lean 19 declarations
MarkedObservables.lean 12 declarations
MartingaleExponentialSubmartingale.lean 5 declarations
MaxTailDecomposition.lean 5 declarations
MeasurableCountableSample.lean 9 declarations
MeasureAdd.lean 6 declarations
MedianAeConst.lean 7 declarations
MixtureSmallMassProbability.lean 6 declarations
MomentRescaling.lean 13 declarations
NaturalTailIntegrable.lean 2 declarations
NoDropApproxError.lean 13 declarations
NonCollapsedSums.lean 10 declarations
NormalLinearPast.lean 10 declarations
NormalizedRestrictionContact.lean 1 declarations
NormalizedSharedRestrict.lean 4 declarations
ObservedBudget.lean 10 declarations
ObservedCharges.lean 11 declarations
ObservedDrift.lean 11 declarations
ObservedPotential.lean 13 declarations
ObserverAlmostSure.lean 6 declarations
OccupationAlgebra.lean 8 declarations
OccupationLimit.lean 5 declarations
OccupationParameters.lean 2 declarations
OccupationSampling.lean 13 declarations
OperationalLengthMarks.lean 9 declarations
OperationalMarkBounds.lean 11 declarations
OrderedTimes.lean 32 declarations
OutwardCanonical.lean 6 declarations
OutwardCapL1.lean 5 declarations
OutwardCapLocality.lean 2 declarations
OwnMarginalOccupation.lean 6 declarations
PairPrefix.lean 28 declarations
PairUpwardRetention.lean 8 declarations
PairWeakUniqueness.lean 2 declarations
PastPhaseExtension.lean 12 declarations
PolicyGoodMass.lean 10 declarations
PrefixVariation.lean 8 declarations
PrefixVariationNonneg.lean 10 declarations
ProbabilityLowerTransfer.lean 1 declarations
ProductNormalJointPast.lean 16 declarations
ProductTruncationError.lean 4 declarations
ProfileMeasureUpdate.lean 9 declarations
ProperProfile.lean 22 declarations
ProtectionFirstFailure.lean 5 declarations
ProtectionLoss.lean 16 declarations
RadixBudget.lean 9 declarations
RapidDecay.lean 12 declarations
RapidDecaySubsequence.lean 2 declarations
RapidDecayTail.lean 2 declarations
RawConditionedWeight.lean 15 declarations
RawDropBounds.lean 7 declarations
RawPair.lean 9 declarations
RawPairEndpoint.lean 17 declarations
RawPairLocality.lean 15 declarations
RawPairMassComposition.lean 1 declarations
RawPairRetention.lean 18 declarations
RealJointPastRestart.lean 6 declarations
RecordIndexTime.lean 28 declarations
RecordMedianSlope.lean 5 declarations
RecordOrPrefixAdd.lean 2 declarations
RecordPairFuture.lean 5 declarations
RecordPrefixControl.lean 6 declarations
ReferenceContinuity.lean 8 declarations
ReferenceFeller.lean 8 declarations
RelativeBudget.lean 29 declarations
RestartLyapunov.lean 8 declarations
RestartSupportedBound.lean 1 declarations
RetainedComposition.lean 14 declarations
Sampling.lean 13 declarations
SamplingLaw.lean 12 declarations
SamplingLimit.lean 6 declarations
SamplingRearrangement.lean 1 declarations
ScaledMaxMoment.lean 7 declarations
ScaledMaxTail.lean 4 declarations
ScheduledCellSuccess.lean 7 declarations
SecondMomentConcentration.lean 4 declarations
SelectedBoundaryRestart.lean 30 declarations
SelectedEndpointMoment.lean 5 declarations
SharedConditionedContactBound.lean 1 declarations
SharedConditionedPairLawFst.lean 11 declarations
SharedEndpointOverlapRight.lean 2 declarations
SharedEndpointTests.lean 5 declarations
SharedLimitNormalPast.lean 4 declarations
SharedLimitOccupation.lean 4 declarations
SharedLimitPastIdentity.lean 1 declarations
SharedShrinking.lean 3 declarations
SharedWordCylinderLower.lean 5 declarations
ShiftedCurveConcatenation.lean 1 declarations
SignedPrefixComparison.lean 6 declarations
SingleAdjacentRadiusBound.lean 3 declarations
SingleCoverWord.lean 15 declarations
SingleThreat.lean 6 declarations
SmallScaleGaussianMass.lean 11 declarations
SmallScaleTailMoment.lean 3 declarations
SmallTimeExponentialError.lean 3 declarations
StageClassification.lean 6 declarations
StageExponentialScales.lean 6 declarations
StageInjection.lean 16 declarations
StageParameters.lean 5 declarations
StageRetention.lean 13 declarations
StageStopping.lean 10 declarations
StayUntil.lean 21 declarations
StoppedSplice.lean 20 declarations
StrictRecord.lean 32 declarations
SuccessfulAverage.lean 9 declarations
SuccessfulAverageBind.lean 3 declarations
SuccessfulScaledTail.lean 10 declarations
SuccessfulWords.lean 26 declarations
SurvivalConditional.lean 10 declarations
SurvivalLimit.lean 7 declarations
SurvivingLane.lean 15 declarations
SymmetricPrefixTail.lean 4 declarations
SymmetricTruncate.lean 39 declarations
SymmetrizedMgf.lean 10 declarations
TailProfile.lean 14 declarations
TailSampling.lean 16 declarations
TightIidDifferenceTranslations.lean 2 declarations
TripleTestPerturbation.lean 3 declarations
TruncatedVarianceDouble.lean 6 declarations
TupleClipping.lean 4 declarations
TupleEndpoint.lean 13 declarations
TwoStopSplice.lean 12 declarations
UniformLowerMass.lean 6 declarations
UniformRiemannMesh.lean 19 declarations
UniformSpreadSequences.lean 4 declarations
UpperPairPatch.lean 6 declarations
VarianceTailDifference.lean 7 declarations
VisibleFailure.lean 8 declarations
VisitTrials.lean 18 declarations
WeakAddTendsto.lean 3 declarations
WeakTailTransfer.lean 3 declarations
WeakVaryingParameter.lean 1 declarations
WeightedConditioned.lean 7 declarations
WeightedTestPerturbation.lean 6 declarations
WidthGridTail.lean 10 declarations
WordConcatenation.lean 15 declarations
WordDepartures.lean 46 declarations
WordPrefixes.lean 17 declarations
WordTemplate.lean 24 declarations