OAI/Probability/SKGap/Localization/PrimaryQuenched.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGapCutoff.Primary.formalOpBound line 15
2. lemma OAI.SKGapCutoff.Primary.formalOpBound_nonneg line 20
3. lemma OAI.SKGapCutoff.Primary.primaryMatrix_opNorm line 27
4. def OAI.SKGapCutoff.Primary.primaryWordTail line 60
5. def OAI.SKGapCutoff.Primary.primaryNormTail line 65
6. theorem OAI.SKGapCutoff.Primary.primary_uniform_actual_derivatives line 69