OAI/Probability/FirstPassage/
971 declarations, 0 contain sorry, 0 declared as axioms; 141 files
Files
- ActualNoCorner.lean 3 declarations
- ActualTimeConstant.lean 9 declarations
- ActualWitnessScale.lean 2 declarations
- AttachmentGeometry.lean 8 declarations
- BKBinaryRanks.lean 10 declarations
- BKBitLaw.lean 8 declarations
- BKContinuous.lean 11 declarations
- BKDyadicPaths.lean 18 declarations
- BKExponentialQuantiles.lean 5 declarations
- BKFamilies.lean 11 declarations
- BKForcing.lean 4 declarations
- BKLimit.lean 1 declarations
- BKPathMeasurability.lean 9 declarations
- BKQuantization.lean 19 declarations
- BKRepeated.lean 13 declarations
- BallTravel.lean 5 declarations
- BoundaryCurve.lean 4 declarations
- BoundaryCycles.lean 2 declarations
- BoundaryGeometry.lean 24 declarations
- BoundaryWinding.lean 10 declarations
- CharacteristicLengths.lean 12 declarations
- CompanionModel.lean 15 declarations
- ConnectorEvents.lean 5 declarations
- ConnectorGeometry.lean 11 declarations
- ConnectorProbability.lean 6 declarations
- ContiguousWitnesses.lean 5 declarations
- ContourCounts.lean 2 declarations
- ContourEnumeration.lean 6 declarations
- ContourLocalization.lean 9 declarations
- ConvexC1.lean 2 declarations
- CoordinateTails.lean 14 declarations
- CrossingChain.lean 5 declarations
- CrossingEndpointBounds.lean 1 declarations
- CrossingTilt.lean 6 declarations
- CrossingTrialGeometry.lean 10 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
- EndpointEntrance.lean 2 declarations
- EndpointEvents.lean 9 declarations
- EndpointExit.lean 2 declarations
- EndpointExtensions.lean 3 declarations
- EndpointGeometry.lean 8 declarations
- EndpointLimit.lean 1 declarations
- EndpointMesh.lean 18 declarations
- EndpointNet.lean 4 declarations
- EndpointProbability.lean 2 declarations
- EndpointRecords.lean 2 declarations
- EndpointTail.lean 9 declarations
- EndpointTranslation.lean 6 declarations
- ExponentialTilt.lean 4 declarations
- ExponentialTiltLaw.lean 5 declarations
- ExtremeSlopes.lean 8 declarations
- FiniteEdgeEvents.lean 10 declarations
- FiniteEdgeTilt.lean 7 declarations
- FiniteNet.lean 1 declarations
- FiniteTiltLaw.lean 7 declarations
- GlobalDifferentiability.lean 3 declarations
- GoodSiteEvents.lean 10 declarations
- GoodSitePaths.lean 5 declarations
- GoodSiteProbability.lean 2 declarations
- GridConnectionGeometry.lean 10 declarations
- GridConnections.lean 7 declarations
- GridCounting.lean 10 declarations
- GridMeshes.lean 15 declarations
- GridProbability.lean 6 declarations
- GridTail.lean 8 declarations
- GridTrials.lean 8 declarations
- HighDensityOriented.lean 8 declarations
- IntervalTravel.lean 7 declarations
- LatticeGeometry.lean 11 declarations
- LatticeLimitExtension.lean 2 declarations
- LatticeSwap.lean 17 declarations
- LocalDifferentiability.lean 3 declarations
- LocalTravel.lean 8 declarations
- Localization.lean 7 declarations
- LocalizedEvents.lean 19 declarations
- Main.lean 3 declarations
- MainTheorem.lean 2 declarations
- NoCornerContradiction.lean 1 declarations
- NormBoundary.lean 4 declarations
- OrientedCompactness.lean 16 declarations
- OrientedProbability.lean 4 declarations
- PassageTime.lean 12 declarations
- PathColumnCrossing.lean 2 declarations
- PathConcatenation.lean 2 declarations
- PathSubpaths.lean 7 declarations
- PathWitnesses.lean 8 declarations
- Paths.lean 23 declarations
- PlaneGeometry.lean 12 declarations
- PositiveMoment.lean 5 declarations
- ProbabilityFoundations.lean 10 declarations
- RareFast.lean 4 declarations
- RareFastEvents.lean 12 declarations
- RareFastGeometry.lean 9 declarations
- RealScaleConnections.lean 12 declarations
- RecordScales.lean 5 declarations
- Reversal.lean 6 declarations
- SeparatedSelection.lean 7 declarations
- ShapeDeficit.lean 2 declarations
- ShapeProbability.lean 6 declarations
- ShortCrossingGeometry.lean 6 declarations
- ShortCrossingProbability.lean 3 declarations
- SimplePathApproximation.lean 3 declarations
- SourceTilt.lean 4 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 7 declarations
- SpatialPositiveChunk.lean 2 declarations
- SpatialRareEvents.lean 3 declarations
- SpatialWitnessCounts.lean 2 declarations
- SpatialWitnesses.lean 11 declarations
- SphereCharts.lean 11 declarations
- SquareLoops.lean 8 declarations
- SupportContactEstimate.lean 5 declarations
- Supports.lean 5 declarations
- Target.lean 10 declarations
- TiltComparison.lean 3 declarations
- TiltPath.lean 2 declarations
- TiltRegionCount.lean 5 declarations
- TiltedRegions.lean 5 declarations
- TimeConstantObligation.lean 3 declarations
- Translation.lean 8 declarations
- UniformShape.lean 10 declarations
- UniqueSupports.lean 4 declarations
- UnitSphereC1.lean 5 declarations
- VerticalIntervals.lean 7 declarations
- Waypoints.lean 11 declarations
- WitnessBorelCantelli.lean 3 declarations
- WitnessDecomposition.lean 11 declarations
- WitnessEntropy.lean 13 declarations
- WitnessSelection.lean 8 declarations