`OAI/Probability/SLE/Gauge/`

1096 declarations, 0 contain sorry, 0 declared as axioms; 229 files

Files

ActualDenseConditional.lean 1 declarations
ActualDenseCoverProbability.lean 1 declarations
ActualDenseExtended.lean 1 declarations
ActualDenseGoodState.lean 3 declarations
ActualDenseIntegration.lean 1 declarations
ActualDenseWindow.lean 5 declarations
ActualMissedCell.lean 3 declarations
ActualPastThreshold.lean 2 declarations
ActualRibbonHistory.lean 1 declarations
ActualRibbonIteration.lean 4 declarations
ActualRibbonMass.lean 2 declarations
ActualRibbonPrefixBound.lean 1 declarations
ActualRibbonStep.lean 5 declarations
ActualRibbonStoppedMass.lean 2 declarations
ActualSequencePassage.lean 2 declarations
ActualSequencePassageRegions.lean 1 declarations
BatchAdaptedFailure.lean 3 declarations
BatchEntryOrder.lean 6 declarations
BatchProbability.lean 3 declarations
BatchRadiusGaps.lean 3 declarations
CanonicalBatchFailure.lean 2 declarations
CanonicalBatchSuccess.lean 1 declarations
CanonicalCoverExpectation.lean 1 declarations
CanonicalDenseIntegration.lean 1 declarations
CanonicalDenseSections.lean 9 declarations
CanonicalDiskMomentTails.lean 7 declarations
CanonicalGaugeTails.lean 2 declarations
CanonicalGridLower.lean 2 declarations
CanonicalLateGridLower.lean 2 declarations
CanonicalPrescribedUpper.lean 1 declarations
CenteredMomentJensen.lean 4 declarations
ConditionalRibbonStep.lean 2 declarations
ConformalCompactSausage.lean 3 declarations
ConformalDenseExperiment.lean 3 declarations
ConformalSausageTransfer.lean 6 declarations
CoverChangeOfLaw.lean 6 declarations
CoverEvents.lean 5 declarations
CoverGaugeBounds.lean 11 declarations
CoverGrid.lean 11 declarations
CoverLimits.lean 5 declarations
CoverMesh.lean 13 declarations
CoverNumerics.lean 6 declarations
CoverRadiusLevels.lean 6 declarations
CoverSchedule.lean 9 declarations
DenseCandidateCover.lean 22 declarations
DenseCoverAdaptedTests.lean 4 declarations
DenseCoverCore.lean 3 declarations
DenseCoverExpectation.lean 3 declarations
DenseCoverUpperReduction.lean 1 declarations
DenseInfinityCriterion.lean 4 declarations
DenseRadiusGap.lean 1 declarations
DenseRibbonNumerics.lean 2 declarations
DenseVisitNumerics.lean 9 declarations
DensityWeightedMoments.lean 1 declarations
DiskCanonicalMoments.lean 1 declarations
DiskIntegratedMoments.lean 2 declarations
EarlyPassageLocalization.lean 8 declarations
ExactGaugeComparison.lean 8 declarations
ExactMomentGauge.lean 5 declarations
ExpectedBadGrid.lean 2 declarations
ExpectedCoverCharge.lean 1 declarations
ExperimentChangeOfLaw.lean 2 declarations
ExperimentClearance.lean 6 declarations
ExtendedExperimentStop.lean 7 declarations
ExtendedRibbonStep.lean 4 declarations
FiniteCoverAssembly.lean 6 declarations
FiniteMomentBounds.lean 2 declarations
FiniteMomentIdentification.lean 5 declarations
FiniteMomentMonotonicity.lean 4 declarations
FiniteStoppedThreshold.lean 2 declarations
FirstFrontPassage.lean 7 declarations
GaugeBoundaryDischarge.lean 1 declarations
GaugeCompletion.lean 27 declarations
GaugeConformalReduction.lean 3 declarations
GaugeCrosscutDischarge.lean 1 declarations
GaugeEntrySmallness.lean 3 declarations
GaugeExitDischarge.lean 1 declarations
GaugeGrowthDischarge.lean 3 declarations
GaugeTailSum.lean 3 declarations
GaugeTraceDischarge.lean 3 declarations
GoodGridRestriction.lean 9 declarations
LargerGaugeMain.lean 4 declarations
LocalAffinePassage.lean 5 declarations
MissedCellCleanup.lean 2 declarations
MomentBatches.lean 28 declarations
MomentCoefficientConvergence.lean 4 declarations
MomentUnclipping.lean 3 declarations
NormalRibbonInjectivity.lean 1 declarations
NormalRibbonPatch.lean 3 declarations
PassageRetention.lean 32 declarations
PassageSuccess.lean 3 declarations
PassageSuccessRegions.lean 1 declarations
PrescribedAdaptedBatch.lean 1 declarations
PrescribedAngleMain.lean 1 declarations
PrescribedApproachTransfer.lean 1 declarations
PrescribedBatchClock.lean 5 declarations
PrescribedBatchMixing.lean 1 declarations
PrescribedCandidateCover.lean 3 declarations
PrescribedCanonicalMixing.lean 1 declarations
PrescribedCanonicalTests.lean 5 declarations
PrescribedCanonicalTransfer.lean 1 declarations
PrescribedCellNormalization.lean 3 declarations
PrescribedCostConvergence.lean 2 declarations
PrescribedCoverEvents.lean 3 declarations
PrescribedCoverExpectation.lean 2 declarations
PrescribedCoverGrid.lean 8 declarations
PrescribedCoverLimits.lean 5 declarations
PrescribedDiskConditional.lean 1 declarations
PrescribedDiskTestKernel.lean 1 declarations
PrescribedEntryKernel.lean 2 declarations
PrescribedGaugeCost.lean 5 declarations
PrescribedGridError.lean 3 declarations
PrescribedGridHeightSum.lean 2 declarations
PrescribedGridLower.lean 3 declarations
PrescribedGridStripSum.lean 2 declarations
PrescribedHeightSum.lean 2 declarations
PrescribedInteriorCost.lean 1 declarations
PrescribedLowerAngle.lean 2 declarations
PrescribedMissedExpectation.lean 2 declarations
PrescribedOrdinaryTransfer.lean 2 declarations
PrescribedPublishedMain.lean 2 declarations
PrescribedRadiusFinalLaw.lean 1 declarations
PrescribedRadiusLevels.lean 5 declarations
PrescribedRadiusTest.lean 1 declarations
PrescribedRowSum.lean 1 declarations
PrescribedTestPast.lean 6 declarations
PrescribedUniformGeometry.lean 1 declarations
PrescribedUpperAngle.lean 1 declarations
PrescribedVisitBound.lean 1 declarations
ProperRibbonCoordinates.lean 5 declarations
PublishedRibbonIteration.lean 1 declarations
RandomBadGrid.lean 6 declarations
RandomPassageBounds.lean 5 declarations
RecenteredRibbonPassage.lean 1 declarations
RestartDenseWeight.lean 1 declarations
RestrictedConformalSausage.lean 2 declarations
RetainedPassageExtraction.lean 2 declarations
RetainedRegionMargins.lean 3 declarations
RetainedTubeSausage.lean 5 declarations
RibbonAccessGuide.lean 1 declarations
RibbonConcatenation.lean 4 declarations
RibbonCoordinateCompactness.lean 19 declarations
RibbonCoordinateGeometry.lean 30 declarations
RibbonCoordinateLimit.lean 6 declarations
RibbonExperimentAssembly.lean 3 declarations
RibbonFrontFreshness.lean 2 declarations
RibbonFrontStops.lean 5 declarations
RibbonGoodPrefix.lean 8 declarations
RibbonHistoryAdvance.lean 8 declarations
RibbonLimitPassageGeometry.lean 7 declarations
RibbonLimitSplice.lean 3 declarations
RibbonMiddleMass.lean 10 declarations
RibbonPassageMass.lean 3 declarations
RibbonPassageNeighborhood.lean 3 declarations
RibbonPassageScaling.lean 10 declarations
RibbonPrefixTransport.lean 2 declarations
RibbonRouteLifting.lean 6 declarations
RibbonSequenceCompactness.lean 4 declarations
RibbonSideCorridors.lean 3 declarations
RibbonStepPatch.lean 11 declarations
RibbonStepSuccess.lean 4 declarations
RibbonStepTranslation.lean 8 declarations
RibbonStoppedMassLaw.lean 1 declarations
RibbonStoppedMassTransport.lean 5 declarations
RibbonSurvival.lean 6 declarations
SequencePassage.lean 2 declarations
SequencePassageRegions.lean 2 declarations
SequencePassageSuccess.lean 2 declarations
SerpentineActualAngle.lean 1 declarations
SerpentineActualAngleReflection.lean 1 declarations
SerpentineActualGuide.lean 2 declarations
SerpentineActualRadius.lean 6 declarations
SerpentineArrayEmbedding.lean 11 declarations
SerpentineArrayRegion.lean 1 declarations
SerpentineAttachments.lean 2 declarations
SerpentineCenteredMass.lean 4 declarations
SerpentineCompleteCurve.lean 11 declarations
SerpentineCompleteEmbedding.lean 4 declarations
SerpentineConformalGeometry.lean 10 declarations
SerpentineCurve.lean 9 declarations
SerpentineEmbedding.lean 10 declarations
SerpentineEscape.lean 6 declarations
SerpentineExperimentGeometry.lean 17 declarations
SerpentineExponentialMass.lean 1 declarations
SerpentineExteriorBounds.lean 1 declarations
SerpentineFiniteHeight.lean 4 declarations
SerpentineFittedChart.lean 12 declarations
SerpentineFittedRegion.lean 5 declarations
SerpentineFittedShadow.lean 6 declarations
SerpentineHorizontalBound.lean 3 declarations
SerpentineInfiniteArray.lean 3 declarations
SerpentineInitialPrefix.lean 8 declarations
SerpentineLayout.lean 37 declarations
SerpentineMarkedClearance.lean 1 declarations
SerpentineMarkedGuide.lean 9 declarations
SerpentineMarkedLocal.lean 4 declarations
SerpentineMarkedReflection.lean 19 declarations
SerpentineMarkedRegion.lean 3 declarations
SerpentineMarkedRouteClearance.lean 2 declarations
SerpentineNormalizedMass.lean 5 declarations
SerpentineParameters.lean 20 declarations
SerpentinePhysicalGeometry.lean 2 declarations
SerpentinePhysicalMass.lean 4 declarations
SerpentinePieces.lean 15 declarations
SerpentineReflection.lean 10 declarations
SerpentineRetainedStrips.lean 5 declarations
SerpentineRetentionCount.lean 3 declarations
SerpentineShadow.lean 7 declarations
SerpentineStepCount.lean 12 declarations
SerpentineTerminal.lean 3 declarations
SerpentineTerminalGuide.lean 15 declarations
SerpentineUpperHalfPlane.lean 2 declarations
ShrinkingCoverAtoms.lean 4 declarations
StoppedSplicePassage.lean 4 declarations
StoppedTubePassage.lean 3 declarations
StrictPastCountable.lean 2 declarations
StrictPastExpectation.lean 2 declarations
StrictPastSpatial.lean 2 declarations
StrictPastTilted.lean 2 declarations
UniformActualRibbonPassage.lean 4 declarations
UniformFrontPassage.lean 8 declarations
UniformPassageThreshold.lean 1 declarations
UniformRecenteredPassage.lean 1 declarations
UniformRibbonStep.lean 9 declarations
VaryingPassageEvents.lean 1 declarations
WaypointBrownianPassages.lean 3 declarations
WeightedMomentIntegration.lean 1 declarations
WholeSausageScaling.lean 4 declarations
WindowDenseTests.lean 1 declarations