OAI/Probability/BenjaminiSchramm/FiniteEnergyObservable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Percolation.BenjaminiSchramm.finite_forcing_measure_bound line 15
2. lemma OAI.Percolation.BenjaminiSchramm.lintegral_finite_forcing_bound line 28
3. lemma OAI.Percolation.BenjaminiSchramm.rooted_forced_layer_count_le line 38
4. theorem OAI.Percolation.BenjaminiSchramm.forced_path_fractional_layer_comparison line 65