`OAI/Probability/SLE/Geometry/`

1444 declarations, 0 contain sorry, 0 declared as axioms; 353 files

Files

AccessGuideCollapse.lean 2 declarations
ActualCompactAvoidance.lean 3 declarations
ActualConformalExitLaw.lean 2 declarations
ActualCrosscutStraightening.lean 1 declarations
ActualExplicitMain.lean 3 declarations
ActualExplicitTransfer.lean 9 declarations
ActualFiniteBoundaryExtension.lean 2 declarations
ActualFirstHeightSupport.lean 5 declarations
ActualGeometricTubeSupport.lean 1 declarations
ActualGuideCompactness.lean 2 declarations
ActualMarkedCell.lean 2 declarations
ActualMarkedStraightening.lean 1 declarations
ActualStoppedTubeSupport.lean 3 declarations
ActualWaypointAngle.lean 1 declarations
ActualWaypointStraightening.lean 7 declarations
ActualWienerSupport.lean 5 declarations
AnalyticCircleSquare.lean 2 declarations
AnalyticFluxEnergy.lean 2 declarations
AnnulusPolarIntegral.lean 3 declarations
ApproachIntervalEndpoint.lean 3 declarations
ArbitraryDiskTail.lean 3 declarations
ArcBoundaryReplacement.lean 5 declarations
ArcHeightExtension.lean 1 declarations
ArcRealRetraction.lean 1 declarations
BoundaryNull.lean 3 declarations
BoundaryRadialDistance.lean 1 declarations
BoundaryScaleLaw.lean 11 declarations
BoundarySeparationRectangle.lean 1 declarations
BoundedSpliceProbability.lean 3 declarations
BoundedTerminalMean.lean 2 declarations
CanonicalBoundaryLimit.lean 1 declarations
CanonicalCoefficientIntegrability.lean 2 declarations
CanonicalCompactPotential.lean 3 declarations
CanonicalDiskPositive.lean 3 declarations
CanonicalDiskPotential.lean 4 declarations
CanonicalDiskTails.lean 5 declarations
CanonicalGreenPast.lean 6 declarations
CanonicalInteriorBound.lean 2 declarations
CanonicalJointDisk.lean 6 declarations
CanonicalLowerSegments.lean 2 declarations
CanonicalNormalizedPotential.lean 3 declarations
CanonicalRawMean.lean 3 declarations
CanonicalRawTerminal.lean 6 declarations
CanonicalRestartDischarge.lean 2 declarations
CanonicalRestartWitness.lean 5 declarations
CenteredCellTail.lean 2 declarations
CenteredDiskCoefficient.lean 3 declarations
CenteredDiskLaw.lean 6 declarations
CenteredFutureSlit.lean 5 declarations
CenteredStoppedMonotonicity.lean 1 declarations
CenteredStoppedTails.lean 2 declarations
CircleRadialFlux.lean 5 declarations
ClosedArcCrossing.lean 2 declarations
ClosedComplexPair.lean 1 declarations
ClosedComplexUnion.lean 1 declarations
ClosedHalfPlaneCayley.lean 1 declarations
ClosedHalfPlaneExtension.lean 1 declarations
CoefficientAngularBound.lean 1 declarations
CompactCellTail.lean 1 declarations
CompactConnectedNeighborhoods.lean 2 declarations
CompactDerivativeIntegral.lean 2 declarations
CompactLaplacianIntegral.lean 2 declarations
CompactPathNeighborhoods.lean 3 declarations
CompactPlanarGaussian.lean 3 declarations
CompactSmoothExtension.lean 1 declarations
CompactTubeProbability.lean 3 declarations
CompactifiedCrosscut.lean 9 declarations
CompleteAccessGuide.lean 2 declarations
ComplexAngularEnergy.lean 2 declarations
ComplexDirichletSlices.lean 2 declarations
ComplexDissipation.lean 2 declarations
ComplexEndpointCluster.lean 2 declarations
ComplexEndpointLimit.lean 2 declarations
ComplexHarmonicGenerator.lean 3 declarations
ComplexJordanExtension.lean 3 declarations
ComplexJordanRegions.lean 5 declarations
ComplexLipschitzExtension.lean 1 declarations
ConcatenatedSlitGeometry.lean 5 declarations
ConditionalStopExtension.lean 1 declarations
ConformalDiskExit.lean 2 declarations
ConformalLaplacian.lean 3 declarations
ConformalLaplacianIntegral.lean 3 declarations
ConformalRestartTransport.lean 5 declarations
ConjugateInversionChart.lean 4 declarations
ContinuousRangeCompletion.lean 6 declarations
CountableInteriorIntervals.lean 5 declarations
CountablePastBound.lean 3 declarations
CountableRemainderKernels.lean 1 declarations
CrosscutExitSides.lean 4 declarations
CrosscutParameterInverse.lean 5 declarations
CurveJoin.lean 6 declarations
DiagonalComplexLimit.lean 1 declarations
DiskBoundaryRegion.lean 15 declarations
DiskCrosscutBoundary.lean 10 declarations
DiskCrosscutClosedRegions.lean 3 declarations
DiskCrosscutHomeomorph.lean 1 declarations
DiskCrosscutPartition.lean 2 declarations
DiskGrowthFromSecondCoefficient.lean 1 declarations
DiskKernelRemainder.lean 2 declarations
DiskLowerStraightening.lean 2 declarations
DiskPoissonPeaks.lean 8 declarations
DiskQuarterDistortion.lean 3 declarations
DiskQuarterGeometry.lean 5 declarations
DiskRecentering.lean 11 declarations
DiskSemicircleGeometry.lean 6 declarations
DiskSideRegionImages.lean 4 declarations
DiskTwoSideGlue.lean 3 declarations
DiskUpperStraightening.lean 5 declarations
EndpointClusterInterval.lean 2 declarations
EndpointClusterLimit.lean 1 declarations
EndpointDerivativeBound.lean 1 declarations
EndpointMonotonicity.lean 1 declarations
ExplicitInputDischarge.lean 1 declarations
ExplicitPublishedMain.lean 1 declarations
ExtendedDiskAngle.lean 3 declarations
ExtendedMarkedAngle.lean 7 declarations
ExtendedStopLocalization.lean 15 declarations
ExteriorCapacityRemainder.lean 1 declarations
ExteriorCompactFlux.lean 1 declarations
ExteriorFirstCoefficient.lean 1 declarations
ExteriorHerglotzAnalytic.lean 3 declarations
ExteriorHerglotzPositive.lean 2 declarations
ExteriorHerglotzTransform.lean 6 declarations
ExteriorJoukowski.lean 9 declarations
ExteriorLaplacianTest.lean 4 declarations
ExteriorLaurent.lean 7 declarations
FiniteBoundaryRestart.lean 4 declarations
FiniteCellTailKernel.lean 4 declarations
FiniteCenteredAngleKernel.lean 1 declarations
FiniteCenteredConsistency.lean 6 declarations
FiniteCenteredPast.lean 2 declarations
FiniteDensityAtPast.lean 1 declarations
FiniteDensityAtRadiusState.lean 1 declarations
FiniteEnergyArcExtension.lean 2 declarations
FiniteExitArcAt.lean 1 declarations
FiniteLawTailBounds.lean 3 declarations
FiniteLawTailENN.lean 4 declarations
FiniteParameterProjection.lean 3 declarations
FinitePastCellTail.lean 1 declarations
FinitePastEvents.lean 5 declarations
FinitePastKernel.lean 2 declarations
FinitePastTrivialBound.lean 2 declarations
FiniteSimpleSlit.lean 1 declarations
FiniteStopSorting.lean 20 declarations
FiniteStoppedScalar.lean 4 declarations
FiniteTraceTopology.lean 4 declarations
FirstDomainExit.lean 5 declarations
FirstHeightBounded.lean 21 declarations
FirstHeightScaling.lean 3 declarations
FirstHeightSupport.lean 15 declarations
FirstSuccessfulPast.lean 8 declarations
FixedCanonicalRestart.lean 1 declarations
FrontClockChange.lean 6 declarations
FrontSuccessMeasurability.lean 12 declarations
FrontSuccessStopped.lean 9 declarations
GeometricTubeSupport.lean 5 declarations
GoodPrefixCoordinates.lean 1 declarations
GreenCompactDecay.lean 2 declarations
GreenMeanDecay.lean 5 declarations
GuideCompactness.lean 6 declarations
GuideInteriorSeparation.lean 1 declarations
GuideLimitIdentification.lean 8 declarations
GuideSplice.lean 42 declarations
GuideTipCollapse.lean 5 declarations
GuideTube.lean 17 declarations
HalfDiskGeometry.lean 12 declarations
HalfPlaneBoundaryDerivative.lean 4 declarations
HalfPlaneBoundaryExtension.lean 3 declarations
HalfPlaneBoundaryIdentity.lean 1 declarations
HalfPlaneCayleyCompactification.lean 10 declarations
HalfPlaneCayleyInverse.lean 8 declarations
HalfPlaneChartBoundary.lean 4 declarations
HalfPlaneCompactnessBloch.lean 1 declarations
HalfPlaneCompactnessFromGrowth.lean 1 declarations
HalfPlaneDiskTransport.lean 3 declarations
HalfPlaneExteriorConnected.lean 5 declarations
HalfPlaneJulia.lean 3 declarations
HalfPlaneNormalizedUniqueness.lean 1 declarations
HalfPlaneSchwarzPick.lean 3 declarations
HalfPlaneUnivalentBounds.lean 5 declarations
HarmonicExitLimit.lean 1 declarations
HarmonicExitProbability.lean 2 declarations
HarmonicLimitData.lean 1 declarations
HarmonicMaximal.lean 2 declarations
HarmonicPathMaximum.lean 2 declarations
HarmonicStopSamples.lean 3 declarations
HarmonicTailMaximum.lean 2 declarations
HarmonicUniformTails.lean 2 declarations
HolomorphicAcrossReal.lean 3 declarations
HolomorphicAreaAverage.lean 3 declarations
HolomorphicBoundaryAtoms.lean 2 declarations
HolomorphicDiskInterior.lean 1 declarations
HolomorphicExitLimit.lean 1 declarations
HolomorphicFamilyCompactness.lean 1 declarations
HolomorphicFamilyEquicontinuity.lean 1 declarations
HolomorphicRadialFlux.lean 1 declarations
HolomorphicStripSections.lean 2 declarations
HyperbolicGuideCompactness.lean 14 declarations
InteriorFluxBound.lean 1 declarations
InteriorVisit.lean 2 declarations
InvertedArcComponents.lean 5 declarations
InvertedExterior.lean 6 declarations
JointRadiusKernel.lean 15 declarations
LipschitzGuideConfinement.lean 10 declarations
LocalCrosscutSides.lean 3 declarations
LocalLogObstruction.lean 2 declarations
LocallyUniformEvaluation.lean 2 declarations
LongitudinalCrossing.lean 4 declarations
MarkedAccessAngle.lean 1 declarations
MarkedAccessHook.lean 19 declarations
MarkedCornerBounds.lean 9 declarations
MarkedCornerChart.lean 9 declarations
MarkedHookLocal.lean 5 declarations
MarkedRouteClearance.lean 13 declarations
MarkedRouteEarlyClearance.lean 4 declarations
MarkedRouteSides.lean 2 declarations
MarkedRoutes.lean 18 declarations
MarkedSurvivingBall.lean 2 declarations
MarkedTubeLocalSides.lean 7 declarations
MarkedWindowEarly.lean 2 declarations
MarkedWindowRoutes.lean 6 declarations
MarkedWitnessReflection.lean 6 declarations
MeasurableBoundaryRestart.lean 1 declarations
MonotoneRationalLimit.lean 1 declarations
NoBoundaryAtoms.lean 1 declarations
NormalizedAccessGuide.lean 1 declarations
NormalizedCanonicalRestart.lean 4 declarations
NormalizedCellAllTimes.lean 1 declarations
NormalizedCoefficientLimit.lean 3 declarations
NormalizedConformalBounds.lean 8 declarations
NormalizedDiskAngle.lean 6 declarations
NormalizedDiskDensity.lean 2 declarations
NormalizedLoewnerCharts.lean 3 declarations
NormalizedMarkedState.lean 6 declarations
NormalizedPotentialIncrement.lean 2 declarations
NormalizedRadiusCell.lean 2 declarations
NormalizedRadiusRestart.lean 3 declarations
NormalizedRawAllTimes.lean 2 declarations
NormalizedRawRestart.lean 2 declarations
NormalizedReflectedSlit.lean 1 declarations
NormalizedRestartDensity.lean 1 declarations
NormalizedRestartGoodSet.lean 1 declarations
NormalizedRestartKernel.lean 4 declarations
NormalizedRiemannChart.lean 1 declarations
NormalizedRiemannUniqueness.lean 2 declarations
NormalizedStoppedDisk.lean 3 declarations
OpenBoundaryTrace.lean 1 declarations
OuterCoefficientLimit.lean 5 declarations
OutwardRealBarrier.lean 2 declarations
PastDensityIntegral.lean 1 declarations
PhysicalCellDisk.lean 1 declarations
PhysicalCenteredWeights.lean 3 declarations
PhysicalGuideCompactness.lean 4 declarations
PhysicalRouteProbability.lean 4 declarations
PolarBoundarySeparation.lean 3 declarations
PolarLaplacianFlux.lean 8 declarations
PositiveKernelTests.lean 3 declarations
PositiveRealDiskEstimate.lean 2 declarations
ProductDensity.lean 1 declarations
PublishedBoundaryExtension.lean 2 declarations
PublishedConformalCompactness.lean 1 declarations
PublishedConformalExitLaw.lean 3 declarations
PublishedCrosscutStraightening.lean 3 declarations
PublishedFiniteBoundaryExtension.lean 6 declarations
PublishedInputs.lean 2 declarations
PublishedPlanarDiskOpenness.lean 1 declarations
PublishedWienerSupport.lean 4 declarations
PuncturedDiskHomeomorph.lean 2 declarations
RadiusCellTail.lean 1 declarations
RandomBoundaryTubes.lean 12 declarations
RandomKernelSupport.lean 3 declarations
RandomRawScaleTests.lean 2 declarations
RandomRestartEvents.lean 4 declarations
RandomSpatialTesting.lean 9 declarations
RandomSpatialTestingAE.lean 3 declarations
RationalTestPath.lean 5 declarations
RealSymmetricDiskMapSign.lean 3 declarations
RecenteredGuideCompactness.lean 1 declarations
ReciprocalInverseLimit.lean 5 declarations
RectangleCauchyBoundary.lean 3 declarations
RectangleCrossing.lean 7 declarations
RectangleLogBoundary.lean 2 declarations
RectangleWedgeSplit.lean 1 declarations
ReflectedInvertedUpperConnected.lean 5 declarations
ReflectedRealSeparation.lean 1 declarations
ReflectedRiemannSymmetry.lean 3 declarations
ReflectedSimpleArc.lean 3 declarations
RegularSlitTube.lean 5 declarations
RemainderKernelCancellation.lean 3 declarations
RestartAE.lean 1 declarations
RestartCellBounds.lean 2 declarations
RestartConformalRadius.lean 5 declarations
RestartContinuationKernel.lean 11 declarations
RestartDerivativeMeasurability.lean 4 declarations
RestartFutureGreen.lean 1 declarations
RestartGreenCovariance.lean 3 declarations
RestartGreenIntegral.lean 1 declarations
RestartGreenKernel.lean 6 declarations
RestartHalfPlaneGreen.lean 6 declarations
RestartInitialGreenIntegral.lean 2 declarations
RestartSectionUpper.lean 1 declarations
RestartWeightedKernel.lean 2 declarations
RightLimitMeasurability.lean 4 declarations
RobustTransverseCrossing.lean 3 declarations
RootCoefficientBound.lean 1 declarations
RootExteriorChart.lean 3 declarations
RootExteriorCompact.lean 3 declarations
RootExteriorFlux.lean 1 declarations
RootExteriorRadius.lean 4 declarations
RoundedConnector.lean 21 declarations
RoundedConnectorBands.lean 7 declarations
RoundedConnectorCurve.lean 16 declarations
RoundedConnectorGeometry.lean 9 declarations
RoundedConnectorRegion.lean 1 declarations
ScaledMarkedKernel.lean 5 declarations
SchoenfliesInsideTransport.lean 5 declarations
ShrinkingPhysicalSegments.lean 1 declarations
ShrinkingStripEnergy.lean 2 declarations
SimpleArcComplement.lean 1 declarations
SimpleArcPlaneComplement.lean 4 declarations
SimplePathConcatenation.lean 1 declarations
SimpleSlitConnected.lean 3 declarations
SimpleSlitRiemann.lean 2 declarations
SingleCrossingObstruction.lean 11 declarations
SmallImageSector.lean 7 declarations
SmallImageSemicircle.lean 14 declarations
SmallLoopCrossing.lean 1 declarations
SpatialExhaustion.lean 9 declarations
SpatialPastKernels.lean 4 declarations
StableTraceAvoidance.lean 4 declarations
StoppedBoundaryMeasurability.lean 9 declarations
StoppedBoundaryRestart.lean 12 declarations
StoppedFutureGreen.lean 1 declarations
StoppedMarkedStateMeasurability.lean 21 declarations
StrictRealLocalChart.lean 1 declarations
SubarcParameter.lean 5 declarations
SymmetricChartUpperBijective.lean 1 declarations
SymmetricSlope.lean 3 declarations
ThinCrossingEnergy.lean 1 declarations
TransportCrosscutPartition.lean 2 declarations
TransverseCurveDifference.lean 3 declarations
UniformAccessLocalization.lean 2 declarations
UniformGuideCompactness.lean 1 declarations
UnitWindowPlanarExit.lean 7 declarations
WaypointAngleNumerics.lean 2 declarations
WaypointCrosscutSides.lean 3 declarations
WaypointDerivativeBounds.lean 2 declarations
WaypointRouteAvoidance.lean 4 declarations
WaypointRouteProbability.lean 9 declarations
WaypointRoutes.lean 17 declarations
WaypointTubeGeometry.lean 1 declarations
WeightedCompactKernel.lean 2 declarations
WeightedCompactTerminal.lean 10 declarations