OAI/Probability/CriticalPercolation/Criticality/BoundaryCount.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CriticalPercolation.Sharpness.expect_exposure_finiteRangeline 16 - lemma
OAI.CriticalPercolation.Sharpness.spatialMarkovline 33 - def
OAI.CriticalPercolation.Sharpness.boundaryCountline 46 - def
OAI.CriticalPercolation.Sharpness.boundaryFluxline 49 - lemma
OAI.CriticalPercolation.Sharpness.closedPivot_reachesTargetline 54 - lemma
OAI.CriticalPercolation.Sharpness.sum_closedPivot_eqline 66 - lemma
OAI.CriticalPercolation.Sharpness.exposedFlux_identityline 98 - theorem
OAI.CriticalPercolation.Sharpness.derivative_identityline 108 - theorem
OAI.CriticalPercolation.Sharpness.differential_inequalityline 118