OAI/Probability/SKFluctuations/
5750 declarations, 0 contain sorry, 0 declared as axioms; 151 files
Files
- AbsTiltedMeanLe.lean 52 declarations
- ActualConditionalHierarchy.lean 30 declarations
- ActualPairCut.lean 22 declarations
- ActualPathScore.lean 41 declarations
- ActualSpinMartingale.lean 36 declarations
- BackwardClockDerivative.lean 36 declarations
- BoundaryCostCongr.lean 46 declarations
- Bounds.lean 62 declarations
- CavityActualEndpoint.lean 69 declarations
- CavityClockZero.lean 31 declarations
- CavityFactorization.lean 43 declarations
- CavityFrozenJet.lean 40 declarations
- CavityGraphParity.lean 45 declarations
- CavityMixedInsertion.lean 43 declarations
- CavityRow.lean 59 declarations
- CenteredMonotoneIntegral.lean 64 declarations
- Chain.lean 44 declarations
- ClockDerivativeContinuous.lean 43 declarations
- ClockFlattenSchedule.lean 41 declarations
- ClockForkCost.lean 36 declarations
- ClockMassIntegral.lean 41 declarations
- ClockPairForkLedger.lean 36 declarations
- ClockPairRepresentation.lean 30 declarations
- ClockPathPairMeasurable.lean 34 declarations
- ClockPathPressureSup.lean 32 declarations
- ClockPowerPathLimit.lean 21 declarations
- ClockRetainTwo.lean 27 declarations
- ClockRetainedSamples.lean 43 declarations
- ClockRootMarginal.lean 30 declarations
- ClockSampledRate.lean 31 declarations
- ClockSplitSteps.lean 55 declarations
- ClockTestAbsLeMul.lean 24 declarations
- ClockZeroRefinement.lean 51 declarations
- CompContDiff.lean 61 declarations
- ComparisonCapTravel.lean 27 declarations
- ComparisonMinimumMassCenter.lean 27 declarations
- ComparisonMinimumRealOverlapConclusion.lean 15 declarations
- ComparisonMinimumRegularRawMoment.lean 7 declarations
- ComparisonMinimumRegularRawRatio.lean 27 declarations
- ComparisonPolynomialRoom.lean 15 declarations
- CompletedFeatureKernel.lean 47 declarations
- CompletedIndex.lean 62 declarations
- Cumulative.lean 56 declarations
- CumulativeIncrements.lean 39 declarations
- Diagonal.lean 39 declarations
- EvalStep.lean 36 declarations
- EventuallyNatPos.lean 37 declarations
- FeatureClockResponse.lean 44 declarations
- FilledSquare.lean 52 declarations
- FinitePrefixRoot.lean 30 declarations
- FiniteRetainedGridReady.lean 34 declarations
- GaussianRootTransversality.lean 52 declarations
- GaussianSmallScale.lean 32 declarations
- Graft.lean 55 declarations
- HasDerivAtDynamicVarianceContinuation.lean 33 declarations
- HasDerivWithinAtVectorHeatContinuation.lean 27 declarations
- HierarchyPenalty.lean 32 declarations
- InvariantPropagation.lean 39 declarations
- InverseConstraintNonempty.lean 35 declarations
- InverseConstraintQuantile.lean 42 declarations
- InverseControlMeasureCalculus.lean 27 declarations
- InverseMomentIntegrability.lean 28 declarations
- LineDerivatives.lean 37 declarations
- LineDerivativesSignEquivVolume.lean 58 declarations
- LinearClockMassDifference.lean 34 declarations
- LowerOnInterval.lean 52 declarations
- MapCLM.lean 37 declarations
- MarkedAttachPreserves.lean 50 declarations
- MarkedPairExpectation.lean 36 declarations
- MartingaleCompensatorLp.lean 26 declarations
- MassResponseJet.lean 46 declarations
- MomentNorm.lean 55 declarations
- NonnegativeProfileValueStep.lean 58 declarations
- OrderedSKCumulativeChord.lean 34 declarations
- OrderedSKRateDirection.lean 22 declarations
- ParametricTestLimit.lean 39 declarations
- PhysicalCommonCutSwap.lean 28 declarations
- PhysicalDyadicClock.lean 28 declarations
- PhysicalFarPair.lean 26 declarations
- PhysicalFiniteRawCover.lean 17 declarations
- PhysicalForkSumMoments.lean 21 declarations
- PhysicalIncrementMoment.lean 33 declarations
- PhysicalLayerSum.lean 60 declarations
- PhysicalMomentOrder.lean 34 declarations
- PhysicalNearPairIntegral.lean 34 declarations
- PhysicalOverlapClockSchedule.lean 18 declarations
- PhysicalPinnedTransport.lean 32 declarations
- PhysicalPinnedWindow.lean 34 declarations
- PhysicalProjection.lean 41 declarations
- PhysicalQuantileSampling.lean 29 declarations
- PhysicalRetainedCut.lean 29 declarations
- PhysicalSusceptibility.lean 31 declarations
- PhysicalTerminalPairLaw.lean 16 declarations
- PositiveMass.lean 33 declarations
- PotentialHeatTrace.lean 48 declarations
- PowerTraceRelativeAbsLe.lean 38 declarations
- Projection.lean 36 declarations
- ProjectionResidual.lean 31 declarations
- ProjectionRootEstimate.lean 47 declarations
- RadiusGridCount.lean 19 declarations
- RawLossLogarithms.lean 33 declarations
- RealSKPressureL1.lean 30 declarations
- ReplicaCovarianceVariation.lean 40 declarations
- ReplicaMixedInsertion.lean 41 declarations
- ReplicaProfileDifferentiation.lean 36 declarations
- ReplicaProfilePairRecursion.lean 37 declarations
- ReplicaProfileStepIdentification.lean 39 declarations
- RescaledProfileTestContinuity.lean 40 declarations
- ResidualGradientBound.lean 26 declarations
- ResidualRootMoment.lean 19 declarations
- ResidualUniformCurvature.lean 31 declarations
- RootSquareConvex.lean 30 declarations
- RootedIncrements.lean 52 declarations
- RootedVariancePressure.lean 38 declarations
- ScalarArbitraryConcat.lean 44 declarations
- ScalarClockRegularity.lean 57 declarations
- ScalarCurvatureLower.lean 50 declarations
- ScalarFiniteInvariant.lean 37 declarations
- ScalarFlattenCurvature.lean 29 declarations
- ScalarFlattenedContinuity.lean 30 declarations
- ScalarFullOriginMarginality.lean 30 declarations
- ScalarGapFourth.lean 43 declarations
- ScalarGapWeighted.lean 53 declarations
- ScalarGeneralHeadBalance.lean 32 declarations
- ScalarIntervalPenalty.lean 26 declarations
- ScalarIntervalStrictArea.lean 26 declarations
- ScalarJetPowerTests.lean 29 declarations
- ScalarParisiValueDiracDyadic.lean 29 declarations
- ScalarPlantedEnergy.lean 35 declarations
- ScalarProfileConcat.lean 42 declarations
- ScalarSlopeInvariant.lean 47 declarations
- ScalarSourceJet.lean 60 declarations
- ScalarTwoClockPressure.lean 32 declarations
- ScalarVaryingFlattenedContinuity.lean 22 declarations
- ScalarWeightedJet.lean 37 declarations
- ScalarZeroPlateau.lean 28 declarations
- ScoreMGF.lean 24 declarations
- SegmentTest.lean 34 declarations
- Spin.lean 80 declarations
- StandardCompletedLawIsOpenPos.lean 71 declarations
- Terminal.lean 45 declarations
- TransformedDensityShape.lean 52 declarations
- TreeRootVariation.lean 52 declarations
- UniformActualLaterProjection.lean 35 declarations
- UniformGridConvergence.lean 51 declarations
- VariableMassClock.lean 38 declarations
- VarianceJet.lean 41 declarations
- VarianceTestZeroRoot.lean 31 declarations
- WeightCongrAt.lean 39 declarations
- WeightedClockPDE.lean 65 declarations
- WeightedFeatureTraceTelescope.lean 40 declarations