OAI/Probability/CriticalPercolation/Harmonic/GramGrowthScales.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CriticalPercolation.HarmonicAnalysis.functionCombination_eq_linearCombination line 18
2. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.exists_posDef_functionGram line 26
3. lemma OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.gram_sparse_product_growth line 43
4. theorem OAI.CriticalPercolation.HarmonicAnalysis.WordGeometry.function_gram_paired_scales line 91