OAI/Probability/CriticalPercolation/Modular/
662 declarations, 0 contain sorry, 0 declared as axioms; 80 files
Files
- ActionMassTransport.lean 6 declarations
- ActionOrbitTransport.lean 18 declarations
- ActionUnimodularRoot.lean 1 declarations
- CappedDiscrepancy.lean 12 declarations
- ClusterDiscrepancy.lean 12 declarations
- ClusterMassEndpoint.lean 5 declarations
- ClusterMassEndpointFinite.lean 7 declarations
- ClusterMassFinite.lean 6 declarations
- ClusterMassInfinite.lean 30 declarations
- ClusterMassRestriction.lean 12 declarations
- ClusterTransportFinite.lean 17 declarations
- ClusterTransportGeometry.lean 12 declarations
- ClusterTransportLimit.lean 6 declarations
- ClusterTransportSums.lean 15 declarations
- CriticalHeavyDrop.lean 5 declarations
- CriticalHeavyIdentity.lean 6 declarations
- CriticalHeavyNull.lean 7 declarations
- CriticalHeavyUniqueness.lean 3 declarations
- DensityModular.lean 2 declarations
- DiscrepancyTail.lean 6 declarations
- ExpectedIncidenceTransport.lean 8 declarations
- FiniteClusterTransport.lean 8 declarations
- GeometricPeakBand.lean 3 declarations
- GraphModular.lean 19 declarations
- HeavyClusterNumber.lean 14 declarations
- HeavyDiscrepancy.lean 5 declarations
- HeavyFiniteGeometry.lean 7 declarations
- HeavyHarris.lean 8 declarations
- HeavyPeaks.lean 6 declarations
- HeavyThinning.lean 14 declarations
- InputMass.lean 14 declarations
- LightCeiling.lean 8 declarations
- LightClusterNumber.lean 15 declarations
- LightSliceFrontier.lean 6 declarations
- LightTwoPointDecay.lean 12 declarations
- MainAllLightBoundary.lean 2 declarations
- MainInfiniteLightBoundary.lean 1 declarations
- MainLightBoundary.lean 2 declarations
- MarkedTiltedTransport.lean 3 declarations
- Mass.lean 5 declarations
- ModularCharacter.lean 15 declarations
- ModularClusterCount.lean 16 declarations
- ModularClusterMass.lean 19 declarations
- ModularGrowth.lean 8 declarations
- ModularIncidence.lean 9 declarations
- ModularLevelGeometry.lean 7 declarations
- ModularSuperlevels.lean 7 declarations
- MoveTransport.lean 4 declarations
- NormalizedDiscrepancy.lean 11 declarations
- NormalizedIncidenceTransport.lean 12 declarations
- ObjectAvoidMass.lean 14 declarations
- OrbitalMassTransport.lean 9 declarations
- OrderMass.lean 16 declarations
- PeakClusters.lean 11 declarations
- PeakRatioTransport.lean 10 declarations
- PeakReturn.lean 11 declarations
- PeakVolumeBand.lean 6 declarations
- PushMass.lean 7 declarations
- RandomTiltedTransport.lean 3 declarations
- RelativeModular.lean 5 declarations
- SignedDiscrepancyContinuity.lean 13 declarations
- SignedIncidenceTransport.lean 3 declarations
- TiltedMassTransport.lean 2 declarations
- TiltedTransportENNReal.lean 5 declarations
- UnimodularAdjacent.lean 4 declarations
- UnimodularAverages.lean 4 declarations
- UnimodularGeometric.lean 3 declarations
- UnimodularUnique.lean 5 declarations
- Unimodularity.lean 16 declarations
- WeightedCauchy.lean 3 declarations
- WeightedDiscrepancy.lean 11 declarations
- WeightedDiscrepancyLimit.lean 6 declarations
- WeightedExplorationCost.lean 4 declarations
- WeightedIncidenceSearch.lean 5 declarations
- WeightedIntegralBand.lean 1 declarations
- WeightedPeakBand.lean 2 declarations
- WeightedPeakTransport.lean 12 declarations
- WeightedQuery.lean 10 declarations
- WeightedQueryBand.lean 2 declarations
- WeightedQueryLaw.lean 3 declarations