OAI/Probability/CriticalPercolation/LinearGroups/LocalFurstenbergBound.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.LocalProjective.equiv_operator_ne_zero line 15
2. lemma OAI.CriticalPercolation.LocalProjective.exists_shell_scalar line 26
3. def OAI.CriticalPercolation.LocalProjective.shellScalar line 31
4. lemma OAI.CriticalPercolation.LocalProjective.shellScalar_spec line 33
5. def OAI.CriticalPercolation.LocalProjective.normalized line 39
6. def OAI.CriticalPercolation.LocalProjective.shell line 42
7. lemma OAI.CriticalPercolation.LocalProjective.compact_shell line 45
8. lemma OAI.CriticalPercolation.LocalProjective.normalized_mem line 52
9. lemma OAI.CriticalPercolation.LocalProjective.normalizedClosure_compact line 57
10. lemma OAI.CriticalPercolation.LocalProjective.normalizedClosure_injective line 65
11. lemma OAI.CriticalPercolation.LocalProjective.projective_lower_bound_of_null_subspaces line 92
12. lemma OAI.CriticalPercolation.LocalProjective.sparse_local_furstenberg_alternative line 144