OAI/Probability/CriticalPercolation/ProductMeasure/CompactInvariantMeasure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.SparseGrowth.orbit_wordBall_nonempty line 16
2. def OAI.CriticalPercolation.SparseGrowth.orbitAverage line 19
3. lemma OAI.CriticalPercolation.SparseGrowth.integral_orbitAverage line 27
4. lemma OAI.CriticalPercolation.SparseGrowth.orbitAverage_translate_bound line 36
5. lemma OAI.CriticalPercolation.SparseGrowth.exists_invariant_probability_measure_generators line 49
6. def OAI.CriticalPercolation.SparseGrowth.integralInvariantSubgroup line 96
7. lemma OAI.CriticalPercolation.SparseGrowth.exists_invariant_probability_measure line 112