OAI/Probability/GammaPassage/
1205 declarations, 0 contain sorry, 0 declared as axioms; 183 files
Files
- ASMeanBridge.lean 3 declarations
- ActualNoCorner.lean 3 declarations
- ActualTimeConstant.lean 1 declarations
- ActualWitnessScale.lean 2 declarations
- AnalyticCore.lean 24 declarations
- AnalyticEndgame.lean 10 declarations
- AnalyticSpecialization.lean 4 declarations
- BKBitLaw.lean 6 declarations
- BKContinuous.lean 8 declarations
- BKDyadic.lean 11 declarations
- BKFamilies.lean 11 declarations
- BKForcing.lean 4 declarations
- BKLimit.lean 1 declarations
- BKPathMeasurability.lean 11 declarations
- BKPrimitives.lean 18 declarations
- BKRepeated.lean 13 declarations
- BKRounded.lean 11 declarations
- BallTravel.lean 9 declarations
- BallTravelGeometry.lean 5 declarations
- BoundaryCycles.lean 2 declarations
- BoundaryGeometry.lean 24 declarations
- BoundaryWinding.lean 10 declarations
- CDF.lean 7 declarations
- CharacteristicLengths.lean 12 declarations
- CheapLongTrails.lean 5 declarations
- CheapPath.lean 6 declarations
- CheapPathCounting.lean 9 declarations
- CheapPathDecay.lean 8 declarations
- ConcentrationScale.lean 2 declarations
- ConnectorContact.lean 1 declarations
- ConnectorEvents.lean 5 declarations
- ConnectorGeometry.lean 11 declarations
- ContiguousWitnesses.lean 5 declarations
- ContourCounts.lean 2 declarations
- ContourEnumeration.lean 6 declarations
- ContourLocalization.lean 9 declarations
- CoordinateTails.lean 9 declarations
- CrossingChain.lean 5 declarations
- CrossingEndpointBounds.lean 1 declarations
- CrossingEvents.lean 13 declarations
- CrossingLocalized.lean 22 declarations
- CrossingTilt.lean 3 declarations
- Differentiability.lean 1 declarations
- DyadicDerivativeBound.lean 1 declarations
- DyadicRanks.lean 8 declarations
- EnclosingContour.lean 4 declarations
- EndpointAsymptotics.lean 3 declarations
- EndpointBlocks.lean 1 declarations
- EndpointBounds.lean 5 declarations
- EndpointCoarse.lean 3 declarations
- EndpointCoarseGeometry.lean 5 declarations
- EndpointConnection.lean 5 declarations
- EndpointCost.lean 2 declarations
- EndpointEntrance.lean 2 declarations
- EndpointEvents.lean 9 declarations
- EndpointExit.lean 2 declarations
- EndpointExtensions.lean 3 declarations
- EndpointGeometry.lean 9 declarations
- EndpointLimit.lean 1 declarations
- EndpointMesh.lean 18 declarations
- EndpointNet.lean 12 declarations
- EndpointProbability.lean 2 declarations
- EndpointRecords.lean 1 declarations
- EndpointTail.lean 9 declarations
- EndpointTranslationProbability.lean 2 declarations
- Environment.lean 9 declarations
- EnvironmentScaling.lean 3 declarations
- ExponentialIncrement.lean 4 declarations
- FiniteEdgeTilt.lean 5 declarations
- FiniteMoments.lean 7 declarations
- FiniteSumIntegrability.lean 4 declarations
- FiniteTails.lean 5 declarations
- FiniteTilt.lean 10 declarations
- FiniteWaypoints.lean 2 declarations
- FirstMoment.lean 5 declarations
- GlobalCenteredConcentration.lean 4 declarations
- GlobalConcentration.lean 4 declarations
- GoodSiteBlocks.lean 13 declarations
- GoodSiteEvents.lean 10 declarations
- GoodSitePaths.lean 5 declarations
- GoodSiteProbability.lean 2 declarations
- GoodSiteTrials.lean 10 declarations
- GridAttachments.lean 11 declarations
- GridConnection.lean 5 declarations
- GridCounting.lean 10 declarations
- GridEvents.lean 5 declarations
- GridGeometry.lean 7 declarations
- GridIndependence.lean 10 declarations
- GridMeshes.lean 15 declarations
- GridTail.lean 8 declarations
- GridVerticalPaths.lean 5 declarations
- HighDensityOriented.lean 8 declarations
- LocalCenteredCGF.lean 2 declarations
- LocalCenteredConcentration.lean 1 declarations
- LocalCoordinateDomination.lean 4 declarations
- LocalExponentialEnergy.lean 3 declarations
- LocalGlobalEquality.lean 6 declarations
- LocalIntegrability.lean 3 declarations
- LocalLawTransfer.lean 5 declarations
- LocalMeanGap.lean 3 declarations
- LocalPassageMGF.lean 3 declarations
- LocalRegularity.lean 11 declarations
- LocalResamplingExponential.lean 5 declarations
- LocalResamplingModel.lean 12 declarations
- LocalTrailCandidates.lean 6 declarations
- LocalTrailPassage.lean 9 declarations
- LocalizationProbability.lean 2 declarations
- LoopErasure.lean 26 declarations
- MGF.lean 4 declarations
- MGFDerivative.lean 3 declarations
- Main.lean 182 imports, no declarations
- MeanAlgebra.lean 7 declarations
- MeanLimit.lean 10 declarations
- MeanLipschitz.lean 4 declarations
- MeanNorm.lean 6 declarations
- MeanNormSwap.lean 4 declarations
- MeanPairSeminorm.lean 2 declarations
- MeanPositive.lean 3 declarations
- MeanSwap.lean 16 declarations
- MovingOrigin.lean 6 declarations
- NoCornerContradiction.lean 1 declarations
- OrientedCompactness.lean 16 declarations
- OrientedProbability.lean 4 declarations
- OrientedSelection.lean 9 declarations
- OriginEscape.lean 6 declarations
- OriginEscapeLower.lean 3 declarations
- PassageLowerBound.lean 5 declarations
- PathChain.lean 2 declarations
- PathColumnCrossing.lean 2 declarations
- PathIntegrability.lean 6 declarations
- PathSecondMoment.lean 11 declarations
- PathSubpaths.lean 7 declarations
- Quantile.lean 14 declarations
- RareFast.lean 4 declarations
- RareFastEvents.lean 11 declarations
- RationalMean.lean 10 declarations
- RationalMeanAlgebra.lean 11 declarations
- RealDirectionBridge.lean 4 declarations
- RealDirectionGeometry.lean 20 declarations
- RealMeanExtension.lean 15 declarations
- RecordGridProbability.lean 3 declarations
- RecordScales.lean 5 declarations
- ResamplingEnergyIdentity.lean 3 declarations
- Scaling.lean 4 declarations
- ScalingLaw.lean 4 declarations
- SequenceSummability.lean 9 declarations
- ShapeDeficit.lean 3 declarations
- ShortCrossingGeometry.lean 6 declarations
- ShortCrossingProbability.lean 4 declarations
- SourceConnector.lean 8 declarations
- SourceTilt.lean 6 declarations
- SpatialBadPathCover.lean 2 declarations
- SpatialChunkGeometry.lean 8 declarations
- SpatialChunkWitness.lean 3 declarations
- SpatialChunks.lean 6 declarations
- SpatialCrossingGeometry.lean 4 declarations
- SpatialEntropyProbability.lean 1 declarations
- SpatialFirstExit.lean 10 declarations
- SpatialModulus.lean 5 declarations
- SpatialPositiveChunk.lean 2 declarations
- SpatialRareProbability.lean 1 declarations
- SpatialWitnessCounts.lean 2 declarations
- SpatialWitnessProbability.lean 2 declarations
- SpatialWitnesses.lean 15 declarations
- SquareLoops.lean 8 declarations
- Stationarity.lean 12 declarations
- SurvivalQuantile.lean 15 declarations
- SurvivalRank.lean 12 declarations
- SurvivalRounding.lean 9 declarations
- Target.lean 2 declarations
- TiltComparison.lean 2 declarations
- TiltDensity.lean 6 declarations
- TiltEnvelope.lean 2 declarations
- TiltMoment.lean 8 declarations
- TiltRegionCount.lean 5 declarations
- TubeDeterministic.lean 3 declarations
- TubeTravel.lean 2 declarations
- UniformShape.lean 6 declarations
- UniformShapeGeometry.lean 9 declarations
- Waypoints.lean 11 declarations
- WitnessBorelCantelli.lean 3 declarations
- WitnessEntropy.lean 13 declarations
- WitnessSelection.lean 8 declarations