OAI/Probability/BenjaminiSchramm/PeakOrbitComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.BondGraph.mixedHeightLayerMoment_eq_of_orbit line 17
2. lemma OAI.CriticalPercolation.BondGraph.mixedHeight_continuation_at_boundary line 27
3. def OAI.CriticalPercolation.BondGraph.fullPeakDownHit line 105
4. lemma OAI.CriticalPercolation.BondGraph.measurableSet_fullPeakDownHit line 109
5. lemma OAI.CriticalPercolation.BondGraph.fullPeakDownHit_subset_exposed line 115