`OAI/Probability/BenjaminiSchramm/`

1310 declarations, 0 contain sorry, 0 declared as axioms; 291 files

Files

AntitoneSurvivalHeight.lean 1 declarations
Application.lean 7 declarations
AvoidanceCostProfile.lean 2 declarations
AvoidanceProduct.lean 6 declarations
BallSnapshot.lean 6 declarations
BandMomentSummability.lean 10 declarations
BlockExposure.lean 3 declarations
BoundaryMultiplicity.lean 4 declarations
BoundedLayerShift.lean 4 declarations
BoundedOrbitDescent.lean 2 declarations
Cayley.lean 14 declarations
CayleyCritical.lean 3 declarations
CayleyInputs.lean 7 declarations
CayleyTheorem.lean 1 declarations
CeilingBandTransport.lean 7 declarations
CeilingBandUniform.lean 4 declarations
CeilingDownCrudeProfile.lean 2 declarations
CeilingZeroBand.lean 1 declarations
ClusterExposure.lean 5 declarations
CombinatorialUnimodularOperator.lean 4 declarations
Consequences.lean 5 declarations
ConsistentLayers.lean 7 declarations
CriticalCeilingProfile.lean 1 declarations
CriticalEndpointProfiles.lean 1 declarations
CriticalFiniteness.lean 3 declarations
CriticalFractionalSlab.lean 2 declarations
CriticalFullspaceProfiles.lean 1 declarations
CriticalHalfspaceDecay.lean 1 declarations
CriticalHalfspaceProfiles.lean 1 declarations
CriticalHeightHit.lean 11 declarations
CriticalNormalizedCrossing.lean 1 declarations
CriticalPeakBand.lean 4 declarations
CriticalPeakComparison.lean 2 declarations
CriticalPeakSurvival.lean 4 declarations
CriticalQuarterMoment.lean 1 declarations
CriticalSlabProfiles.lean 1 declarations
CriticalSusceptibility.lean 4 declarations
CriticalUpwardDecay.lean 8 declarations
CrossingExponent.lean 1 declarations
CrossingExponentContinuity.lean 2 declarations
CrossingPositivity.lean 3 declarations
DeletionBound.lean 4 declarations
DeletionLoss.lean 8 declarations
DownLayerReciprocity.lean 2 declarations
DownwardHalfspaceFromContinuation.lean 1 declarations
EdgeClosing.lean 5 declarations
EntropyEvent.lean 3 declarations
EventLeftContinuity.lean 3 declarations
EventMeasurability.lean 8 declarations
ExponentialDecay.lean 10 declarations
ExteriorConnection.lean 6 declarations
ExteriorContact.lean 5 declarations
ExteriorEscape.lean 10 declarations
ExteriorExposure.lean 4 declarations
FiniteClusterSums.lean 1 declarations
FiniteEnergyModification.lean 7 declarations
FiniteEnergyObservable.lean 4 declarations
FiniteOrbitStationary.lean 5 declarations
FirstHeightPeakWalk.lean 2 declarations
FloorDownProfile.lean 3 declarations
FourArmGeometry.lean 7 declarations
FractionalBandEstimate.lean 2 declarations
FractionalBandGeometry.lean 3 declarations
FractionalBandTransport.lean 6 declarations
FractionalExponentBootstrap.lean 1 declarations
FractionalHolder.lean 1 declarations
FractionalInterpolation.lean 1 declarations
FractionalSlabEstimate.lean 2 declarations
FractionalSlabFromTruncation.lean 1 declarations
FractionalSlabGeometry.lean 11 declarations
FractionalSlabTransport.lean 5 declarations
FreshSlabConcatenation.lean 5 declarations
FreshSlabCrossing.lean 5 declarations
FreshWhiteExposure.lean 7 declarations
FullConclusion.lean 3 declarations
FullLayerProfile.lean 3 declarations
FullNegativeLayerProfile.lean 3 declarations
FullspaceFractionalRecurrence.lean 3 declarations
GeneralCriticalFiniteness.lean 1 declarations
GeometricIncrement.lean 2 declarations
GhostAvoidance.lean 3 declarations
GhostBondBK.lean 8 declarations
GhostCluster.lean 11 declarations
GhostCritical.lean 4 declarations
GhostDerivative.lean 2 declarations
GhostDifferentialAssembly.lean 2 declarations
GhostDoubleConnection.lean 1 declarations
GhostEntropy.lean 7 declarations
GhostFan.lean 14 declarations
GhostFanBK.lean 2 declarations
GhostField.lean 11 declarations
GhostMomentBound.lean 6 declarations
GhostMomentDischarge.lean 4 declarations
GhostPivotalBound.lean 2 declarations
GhostPivotalBoundary.lean 4 declarations
GhostPivotalGeometry.lean 6 declarations
GhostPivotalIncidence.lean 1 declarations
GhostPivotalProbability.lean 5 declarations
GhostPivotalSum.lean 3 declarations
GhostPivotalUnion.lean 1 declarations
GhostPivotalWeight.lean 4 declarations
GhostTail.lean 4 declarations
GhostTiltedTransport.lean 11 declarations
GhostVolume.lean 6 declarations
HalfspaceConcatenation.lean 9 declarations
HalfspaceFiniteShift.lean 3 declarations
HalfspaceFiniteShiftProfile.lean 4 declarations
HalfspaceFractionalRecurrence.lean 3 declarations
HalfspaceProfileBootstrap.lean 3 declarations
HalfspaceRootComparison.lean 2 declarations
HalfspaceUniformShift.lean 2 declarations
HarmonicHeightAscent.lean 4 declarations
HarmonicHeightDescent.lean 2 declarations
HeightMaximumSlices.lean 4 declarations
HeightOrbitConnection.lean 3 declarations
InputReduction.lean 3 declarations
IntegerFrontierCrossing.lean 3 declarations
IntegerLayerFirstVisit.lean 3 declarations
IntrinsicBallExposure.lean 7 declarations
IntrinsicBallGrowth.lean 12 declarations
IntrinsicBallisticity.lean 3 declarations
IntrinsicConnection.lean 8 declarations
IntrinsicConnectionAverage.lean 3 declarations
IntrinsicFreshPath.lean 3 declarations
IntrinsicRadiusLower.lean 4 declarations
IntrinsicRadiusUpper.lean 3 declarations
IntrinsicSphere.lean 7 declarations
KernelDeletionDiagram.lean 3 declarations
KernelDeletionOperator.lean 6 declarations
KernelExterior.lean 3 declarations
KernelExteriorBound.lean 7 declarations
LayerCrossingComparison.lean 3 declarations
LayerFirstMomentPositivity.lean 4 declarations
LayerFirstMomentRate.lean 1 declarations
LayerFirstMomentSubmultiplicative.lean 3 declarations
LayerFirstMoments.lean 9 declarations
LayerFreshSelection.lean 2 declarations
LayerFrontierExpectation.lean 9 declarations
LayerFrontierGeometry.lean 19 declarations
LayerFrontierLocalization.lean 4 declarations
LayerMaximumDecomposition.lean 5 declarations
LayerMomentCauchy.lean 3 declarations
LayerMomentDecomposition.lean 4 declarations
LayerMomentFekete.lean 1 declarations
LayerMonotoneLimit.lean 9 declarations
LayerPrefactorBootstrap.lean 2 declarations
LayerProfileAtRate.lean 2 declarations
LayerSecondMomentDecomposition.lean 1 declarations
Main.lean 4 declarations
MeanFieldReduction.lean 3 declarations
MinimumHeightHit.lean 5 declarations
MixedHeightMoment.lean 5 declarations
MixedRootPathComparison.lean 3 declarations
MixedRootSurgery.lean 2 declarations
ModularCrossingRate.lean 8 declarations
ModularSchur.lean 5 declarations
ModularSlabs.lean 11 declarations
NegativeMomentConvolution.lean 1 declarations
NeighborDegreeBound.lean 2 declarations
Nonunimodular.lean 3 declarations
NonunimodularMomentReduction.lean 2 declarations
NormalizedCrossingRate.lean 3 declarations
NormalizedEscapeRisk.lean 3 declarations
NormalizedExponentComparison.lean 5 declarations
NormalizedHalfspace.lean 12 declarations
NormalizedLayerTransport.lean 10 declarations
NormalizedPeakSurgery.lean 1 declarations
NormalizedQuarterMoment.lean 3 declarations
OpenTriangle.lean 3 declarations
OperatorGap.lean 3 declarations
OperatorMeanFieldReduction.lean 1 declarations
OperatorSusceptibility.lean 4 declarations
OrbitHeightComparison.lean 8 declarations
OrbitNeighborChain.lean 15 declarations
OrbitNormalization.lean 6 declarations
OrbitTransport.lean 14 declarations
PairedSprinkling.lean 19 declarations
PeakBandProbability.lean 5 declarations
PeakBandSecondMoment.lean 2 declarations
PeakBandTransport.lean 8 declarations
PeakClusterCorrelation.lean 11 declarations
PeakComparison.lean 5 declarations
PeakComparisonAveraging.lean 2 declarations
PeakComplementCorrelation.lean 2 declarations
PeakConditionalLayers.lean 6 declarations
PeakCorrelationAveraging.lean 4 declarations
PeakCostBound.lean 2 declarations
PeakCountComparison.lean 3 declarations
PeakExposureComparison.lean 4 declarations
PeakExposureGeometry.lean 5 declarations
PeakExtension.lean 3 declarations
PeakFiniteEnergy.lean 5 declarations
PeakFirstMoment.lean 7 declarations
PeakFrontierTruncation.lean 1 declarations
PeakHalfspaceGeometry.lean 8 declarations
PeakHalfspaceTransport.lean 9 declarations
PeakLayerCost.lean 6 declarations
PeakLayerEstimate.lean 14 declarations
PeakLayerTransport.lean 9 declarations
PeakOrbitComparison.lean 5 declarations
PeakRateCancellation.lean 1 declarations
PeakSlabComparison.lean 1 declarations
PeakSprinklingAverage.lean 3 declarations
PeakSprinklingCell.lean 6 declarations
PeakSprinklingCost.lean 4 declarations
PeakSprinklingSurvival.lean 1 declarations
PeakSurgeryAverage.lean 2 declarations
PeakSurgeryGeometry.lean 5 declarations
PeakSurgeryProbability.lean 3 declarations
PeakSurvivalCauchy.lean 3 declarations
PeakSurvivalRealHeight.lean 3 declarations
PeakUpperExposure.lean 4 declarations
PhaseInput.lean 8 declarations
PivotalExposure.lean 2 declarations
PrefixMaximumBootstrap.lean 5 declarations
ProbabilityLower.lean 8 declarations
ProbabilityUpper.lean 3 declarations
ProbeEntropy.lean 16 declarations
PublishedConsequences.lean 36 declarations
RadiusInputReduction.lean 1 declarations
RadiusTransfer.lean 8 declarations
ReciprocalDecay.lean 1 declarations
ReciprocalGrowth.lean 1 declarations
RestrictedMomentHolder.lean 1 declarations
RootGhostSums.lean 2 declarations
RootTiltedGhost.lean 6 declarations
SelectedLayerVertex.lean 5 declarations
SignedUpperConvolution.lean 1 declarations
SlabCountBasic.lean 5 declarations
SlabCrossing.lean 1 declarations
SlabExtensionGeometry.lean 4 declarations
SlabFirstVisit.lean 4 declarations
SlabFractionalProfileShift.lean 3 declarations
SlabFractionalRecurrence.lean 6 declarations
SlabHit.lean 5 declarations
SlabLastMaximum.lean 4 declarations
SlabRootShift.lean 1 declarations
SlabSecondMoment.lean 8 declarations
SmallWalkKernel.lean 1 declarations
SmallWitness.lean 2 declarations
SprinklingAvoidanceProfile.lean 2 declarations
SprinklingParameter.lean 1 declarations
SprinklingPeakGeometry.lean 3 declarations
SubcriticalCrossingBound.lean 1 declarations
SubcriticalFullLayerProfile.lean 2 declarations
SubcriticalLayerConvolution.lean 7 declarations
SubcriticalLayerPrefactor.lean 1 declarations
SubcriticalLayerSecondMoment.lean 1 declarations
SubcriticalPeakConditional.lean 2 declarations
SubcriticalPeakProbability.lean 1 declarations
SubcriticalPeakSurvival.lean 1 declarations
SubcriticalUpperSecondMoment.lean 1 declarations
SubcriticalUpward.lean 1 declarations
SubdivisionConsequences.lean 11 declarations
SubdivisionGeometry.lean 11 declarations
SubdivisionOperator.lean 11 declarations
SusceptibilityComparison.lean 1 declarations
SusceptibilityDerivative.lean 7 declarations
SusceptibilityDerivativeLower.lean 2 declarations
SusceptibilityLaw.lean 2 declarations
SusceptibilityUpper.lean 6 declarations
ThinSphere.lean 3 declarations
ThinSphereExposure.lean 4 declarations
ThinSphereProbability.lean 5 declarations
ThinSphereRecurrence.lean 2 declarations
ThinSphereStopping.lean 7 declarations
TiltedGhost.lean 18 declarations
TiltedGhostSusceptibility.lean 8 declarations
TiltedHit.lean 5 declarations
TiltedMagnetization.lean 1 declarations
TiltedMomentBridge.lean 3 declarations
TiltedMoments.lean 9 declarations
TiltedSusceptibility.lean 8 declarations
TruncatedFractionalSummation.lean 4 declarations
TruncatedSlabMoment.lean 1 declarations
TwoGhost.lean 4 declarations
UnconditionalInputs.lean 3 declarations
UniformHeightAscent.lean 2 declarations
UniformHeightDescent.lean 3 declarations
UpperLayerSecondMoment.lean 1 declarations
UpperMomentConvolution.lean 1 declarations
UpwardCeilingProfile.lean 3 declarations
UpwardFractionalSlabProfile.lean 2 declarations
UpwardFrontierProbability.lean 3 declarations
UpwardHalfspaceFromContinuation.lean 1 declarations
VolumeEntropy.lean 2 declarations
VolumeLower.lean 3 declarations
WeightedCostRetention.lean 4 declarations
WeightedGhostIncidence.lean 7 declarations
WeightedMomentCauchy.lean 2 declarations
WeightedPeakSlabComparison.lean 2 declarations