`OAI/Probability/SLE/Loewner/`

900 declarations, 0 contain sorry, 0 declared as axioms; 295 files

Files

ActualApproach.lean 2 declarations
ActualApproachAtRadius.lean 2 declarations
ActualDiskGrowth.lean 1 declarations
ActualRadiusStops.lean 8 declarations
ActualRadiusStopsRegular.lean 2 declarations
CanonicalApproach.lean 1 declarations
CanonicalCapacityWitness.lean 1 declarations
CanonicalFlowEvolution.lean 2 declarations
CanonicalHydrodynamic.lean 2 declarations
CanonicalInverseAngle.lean 19 declarations
CanonicalInverseHolomorphic.lean 7 declarations
CanonicalInverseNonzero.lean 2 declarations
CanonicalRadiusKernel.lean 22 declarations
CanonicalSurvival.lean 1 declarations
CanonicalTraceCandidate.lean 4 declarations
CanonicalTraceDischarge.lean 1 declarations
CapacityDriverContinuity.lean 2 declarations
CapacityForwardDerivative.lean 5 declarations
CapacityForwardLipschitz.lean 6 declarations
CapacityLoewnerDerivative.lean 4 declarations
CapacityLoewnerIntegral.lean 2 declarations
CapacityParameterContinuity.lean 6 declarations
CapacityPointwiseLoewner.lean 1 declarations
CapacityRadiusBound.lean 2 declarations
CapacityRightLoewner.lean 3 declarations
FillEndpoint.lean 1 declarations
ForwardCapacityError.lean 1 declarations
ForwardHeightSquareIncrement.lean 2 declarations
ForwardInfinityBounds.lean 2 declarations
FreshCapacityWitness.lean 1 declarations
FreshTipMapOut.lean 3 declarations
FutureArcThinCrossing.lean 1 declarations
FutureCapacityAdditive.lean 4 declarations
FutureComposedCharts.lean 3 declarations
FutureSlitDomain.lean 4 declarations
FutureSlitHeight.lean 1 declarations
FutureSlitRadius.lean 2 declarations
HalfPlaneDisplacementBound.lean 2 declarations
HalfPlaneExitBounds.lean 2 declarations
HalfPlaneExitWeights.lean 5 declarations
HalfPlaneFiniteExit.lean 1 declarations
HydrodynamicAsymptotics.lean 2 declarations
HydrodynamicCoefficient.lean 2 declarations
HydrodynamicComposition.lean 5 declarations
HydrodynamicHeight.lean 5 declarations
InitialCapacity.lean 9 declarations
InitialCapacityAtZero.lean 1 declarations
InitialCapacityClock.lean 4 declarations
InitialCapacityContinuity.lean 3 declarations
InitialCapacityStrict.lean 2 declarations
InitialCapacityTerminal.lean 3 declarations
InitialChartIdentities.lean 2 declarations
InitialChartNormalization.lean 4 declarations
InitialConeFromInterval.lean 1 declarations
InitialDrivingBound.lean 1 declarations
InitialDrivingContinuity.lean 3 declarations
InitialDrivingIncrement.lean 1 declarations
InitialDrivingLimit.lean 4 declarations
InitialDrivingRightContinuity.lean 3 declarations
InitialDrivingTip.lean 1 declarations
InitialForwardBaseBounds.lean 2 declarations
InitialForwardChart.lean 8 declarations
InitialForwardComparison.lean 2 declarations
InitialForwardIncrement.lean 2 declarations
InitialForwardJointContinuity.lean 2 declarations
InitialForwardKernel.lean 1 declarations
InitialForwardKernelLimit.lean 1 declarations
InitialForwardLimit.lean 1 declarations
InitialForwardNormalFamily.lean 1 declarations
InitialForwardRecovery.lean 1 declarations
InitialForwardTimeContinuity.lean 1 declarations
InitialHeightCapacityIncrement.lean 1 declarations
InitialInverseChart.lean 6 declarations
InitialInverseCommonDomain.lean 1 declarations
InitialInverseEnergyBound.lean 1 declarations
InitialInverseEnergyIntegral.lean 2 declarations
InitialInverseJointContinuity.lean 2 declarations
InitialInverseLimit.lean 5 declarations
InitialInverseLimitAt.lean 1 declarations
InitialInverseNormalFamily.lean 2 declarations
InitialInversePartialDomain.lean 3 declarations
InitialInverseRange.lean 5 declarations
InitialInverseRangeAt.lean 3 declarations
InitialInverseTimeContinuity.lean 1 declarations
InitialLimitInverse.lean 4 declarations
InitialReflectedForward.lean 8 declarations
InitialSlitFuture.lean 6 declarations
InitialSubarc.lean 7 declarations
InitialSubarcReparam.lean 3 declarations
InitialTipHeightBound.lean 1 declarations
InverseBoundaryArc.lean 2 declarations
InverseBoundaryBound.lean 2 declarations
InverseBoundaryClosingPath.lean 1 declarations
InverseBoundaryCluster.lean 2 declarations
InverseBoundaryShrink.lean 4 declarations
InverseCircleArea.lean 2 declarations
InverseDirichletEnergy.lean 1 declarations
InverseRectangleEnergy.lean 1 declarations
InverseSmallSemicircles.lean 2 declarations
InverseStripEnergy.lean 1 declarations
InverseThinCollapse.lean 1 declarations
InverseVerticalDifferentiation.lean 2 declarations
InverseVerticalEnergy.lean 2 declarations
LinearReverseTrajectory.lean 11 declarations
LocalReverseCone.lean 1 declarations
LoewnerCompactDriverNeighborhood.lean 1 declarations
LoewnerCompactSurvival.lean 1 declarations
LoewnerDriverBounds.lean 4 declarations
LoewnerHeightClearance.lean 2 declarations
LoewnerInverseCompactness.lean 2 declarations
LoewnerInverseDriverContinuity.lean 2 declarations
LoewnerInverseStability.lean 3 declarations
LoewnerKernelContinuity.lean 1 declarations
LoewnerSmallDriverHeight.lean 1 declarations
LoewnerTipHullApproximation.lean 2 declarations
LoewnerTipVisit.lean 3 declarations
LoewnerTraceHeight.lean 2 declarations
LoewnerVerticalLimit.lean 5 declarations
MappedFutureArc.lean 8 declarations
MappedFutureRange.lean 4 declarations
MappedFutureSimple.lean 2 declarations
MovingForwardBoundaryHeight.lean 2 declarations
OpenSurvivalLifetime.lean 1 declarations
PositiveReverseUniqueness.lean 1 declarations
PositiveSlitCapacity.lean 1 declarations
RadiusHalfPlaneHull.lean 7 declarations
RadiusHullInverse.lean 7 declarations
RawBoundaryReverseTrace.lean 1 declarations
RawBoundaryTraceIdentification.lean 1 declarations
RawConstantTailInverse.lean 1 declarations
RawConstantTailTrace.lean 1 declarations
RawDiskAngleTail.lean 3 declarations
RawDiskRadiusLaw.lean 8 declarations
RawFixedRestart.lean 1 declarations
RawForwardCoordinates.lean 2 declarations
RawForwardHeight.lean 2 declarations
RawForwardInfinity.lean 1 declarations
RawHeightContinuation.lean 1 declarations
RawInverseDriverApproximation.lean 2 declarations
RawInverseHolomorphic.lean 4 declarations
RawLifetimeFlowLimit.lean 2 declarations
RawLifetimeHeightLimit.lean 1 declarations
RawLifetimeTrace.lean 1 declarations
RawRadialTipBoundary.lean 1 declarations
RawRestartAdaptation.lean 6 declarations
RawRestartCanonical.lean 1 declarations
RawRestartGreenKernel.lean 3 declarations
RawRestartRandomTests.lean 1 declarations
RawReverseComposition.lean 2 declarations
RawScaleTests.lean 2 declarations
RawScaledGreenKernel.lean 1 declarations
RawSurvivingAnalytic.lean 4 declarations
RawSurvivingDerivative.lean 1 declarations
RawSurvivingMonotone.lean 1 declarations
RawTerminalExhaustion.lean 6 declarations
RawTipTimeContinuity.lean 3 declarations
RealBoundaryDriverNeighborhood.lean 2 declarations
RealBoundaryTraceAvoidance.lean 1 declarations
RealCharacteristicAvoidance.lean 3 declarations
ReflectedCapacityChart.lean 2 declarations
ReflectedChartLocalBound.lean 5 declarations
ReflectedExteriorAnalytic.lean 4 declarations
ReflectedExteriorHeight.lean 2 declarations
ReflectedForwardContinuity.lean 3 declarations
ReflectedSlitRiemann.lean 2 declarations
RestartDomainEquality.lean 3 declarations
RestartDriverScaling.lean 5 declarations
ReverseBoundaryCone.lean 1 declarations
ReverseBoundarySquare.lean 2 declarations
ReverseConeContraction.lean 2 declarations
ReverseFlowStability.lean 2 declarations
ReverseHeightUpper.lean 2 declarations
ReverseLongContraction.lean 2 declarations
ReverseSmoothBounds.lean 3 declarations
ReverseTrajectoryExistence.lean 1 declarations
RightFieldDriverStability.lean 3 declarations
ScaleTraceLaw.lean 5 declarations
ShiftedHydrodynamicComposition.lean 6 declarations
SlitBoundaryBarrier.lean 6 declarations
SlitBoundaryFiber.lean 2 declarations
SlitBoundaryIntegralLimit.lean 5 declarations
SlitBoundaryTip.lean 1 declarations
SlitCapacityChart.lean 1 declarations
SlitCapacityQuotient.lean 1 declarations
SlitCapacityRemainder.lean 2 declarations
SlitChartBoundaryBasics.lean 4 declarations
SlitChartBoundaryExtension.lean 2 declarations
SlitChartBoundaryShrink.lean 2 declarations
SlitChartClosingPath.lean 1 declarations
SlitChartDisplacement.lean 3 declarations
SlitChartExteriorComparison.lean 2 declarations
SlitChartFarHeight.lean 3 declarations
SlitChartLimitUniqueness.lean 2 declarations
SlitChartProper.lean 1 declarations
SlitChartRangeUniqueness.lean 1 declarations
SlitChartSmallSemicircles.lean 2 declarations
SlitChartStripEnergy.lean 1 declarations
SlitChartUniqueness.lean 1 declarations
SlitChartVerticalBounds.lean 2 declarations
SlitClockRestriction.lean 5 declarations
SlitConstantDriverTail.lean 2 declarations
SlitExtendedTrace.lean 2 declarations
SlitExteriorChart.lean 6 declarations
SlitForwardBoundaryHeight.lean 2 declarations
SlitForwardEndpoint.lean 1 declarations
SlitHydrodynamicChart.lean 4 declarations
SlitInitialEvolution.lean 1 declarations
SlitInverseAtInfinity.lean 2 declarations
SlitInverseGerm.lean 2 declarations
SlitPhysicalClock.lean 9 declarations
SlitPhysicalEvolution.lean 3 declarations
SlitPhysicalTrace.lean 7 declarations
SlitRadialLimits.lean 2 declarations
SlitRawCapacity.lean 1 declarations
SlitRawForward.lean 1 declarations
SlitRawInverse.lean 2 declarations
SlitRawTrace.lean 1 declarations
SlitRealBoundaryFlow.lean 6 declarations
SlitRealCharacteristics.lean 1 declarations
SlitReciprocalChart.lean 7 declarations
SlitReflectedInterior.lean 6 declarations
SlitSegmentParameter.lean 7 declarations
SlitSupport.lean 2 declarations
SlitTailDomain.lean 3 declarations
SlitTimeGluing.lean 1 declarations
SlitUniformForwardBound.lean 5 declarations
SlitUniformInverseBound.lean 3 declarations
SmallDriverRise.lean 1 declarations
SmoothDomainExhaustion.lean 2 declarations
SmoothDriverLipschitz.lean 1 declarations
SmoothRawDomain.lean 3 declarations
SmoothRawFreshness.lean 1 declarations
SmoothRawGeometry.lean 2 declarations
SmoothRawInverse.lean 2 declarations
SmoothRawReverseEstimates.lean 1 declarations
SmoothRawSimple.lean 2 declarations
SmoothRawTipGlobal.lean 4 declarations
SmoothRawTipLimit.lean 2 declarations
SmoothRawTrace.lean 2 declarations
SmoothRawTraceBounds.lean 2 declarations
SmoothRawTraceContinuity.lean 2 declarations
SmoothRawTraceContinuous.lean 3 declarations
SmoothRawTraceInterior.lean 3 declarations
SmoothReverseContraction.lean 1 declarations
SmoothReverseLoewner.lean 4 declarations
StoppedDriverConcatenation.lean 12 declarations
StoppedInverseExhaustion.lean 4 declarations
StoppedInverseGreenMean.lean 4 declarations
StoppedInverseKernel.lean 3 declarations
StoppedInverseMeans.lean 4 declarations
StoppedInversePaths.lean 11 declarations
StoppedInverseTerminalBound.lean 4 declarations
StoppedInverseTerminalUniqueness.lean 2 declarations
StoppedInverseTestUniqueness.lean 2 declarations
TargetBoundaryLimit.lean 8 declarations
TargetContinuationPullback.lean 3 declarations
TargetCutoffField.lean 6 declarations
TargetCutoffMeasurability.lean 8 declarations
TargetCutoffTrajectory.lean 8 declarations
TargetDensityBound.lean 1 declarations
TargetDriverContinuation.lean 14 declarations
TargetEulerBridge.lean 2 declarations
TargetEulerConvergence.lean 6 declarations
TargetEulerInterpolation.lean 11 declarations
TargetForwardAnalytic.lean 1 declarations
TargetInverseContinuity.lean 3 declarations
TargetInverseExistence.lean 3 declarations
TargetInverseMeasurability.lean 7 declarations
TargetInverseProperties.lean 7 declarations
TargetJointMeasurability.lean 11 declarations
TargetOuterMeasurability.lean 6 declarations
TargetSurvivalExtension.lean 1 declarations
TargetSurvivalLifetime.lean 2 declarations
TargetTraceCandidate.lean 7 declarations
TraceBoundaryBarrier.lean 6 declarations
TraceDomainBoundary.lean 1 declarations
TraceRestrictionContinuity.lean 1 declarations
TraceWitnessUniqueness.lean 3 declarations
UnivalentArcRayCrossing.lean 4 declarations
UnivalentFamilyPropagation.lean 5 declarations
UnivalentInverseAnalytic.lean 6 declarations
UnivalentKoebeTransform.lean 4 declarations
UnivalentLocalBound.lean 3 declarations
UnivalentLocallyUniformLimit.lean 2 declarations
UnivalentMovingNormalization.lean 1 declarations
UnivalentOddRoot.lean 4 declarations
UnivalentRadialDerivative.lean 2 declarations
UnivalentRootFactor.lean 1 declarations
UnivalentSecondCoefficient.lean 3 declarations
VanishingHeightRealBounds.lean 3 declarations
VanishingHeightRealLimit.lean 1 declarations
VerticalDisplacementLimit.lean 2 declarations
VerticalHalfPlaneUniqueness.lean 2 declarations
VerticalIntervalEnergy.lean 2 declarations
VerticalMapDerivative.lean 1 declarations