OAI/Probability/CriticalPercolation/LinearGroups/StrongDenseEigenvalues.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.LinearGrowth.eigenvector_transfer line 20
2. lemma OAI.CriticalPercolation.LinearGrowth.eigenvector_transfer_ne_zero line 33
3. lemma OAI.CriticalPercolation.LinearGrowth.matrix_local_ratio_bound line 41
4. lemma OAI.CriticalPercolation.LinearGrowth.eigenvalue_ratio_root_of_unity_of_strongFullMatrixSpan line 53