OAI/Analysis/LpDimension/HeatLocalization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SubpolynomialLp.graphHeat_entry_hasDerivAt line 15
2. lemma OAI.SubpolynomialLp.graphHeat_mass line 30
3. lemma OAI.SubpolynomialLp.graphHeat_tendsto line 54
4. lemma OAI.SubpolynomialLp.graphHeat_entropy_integral line 88
5. lemma OAI.SubpolynomialLp.sum_abs_outer_le line 125
6. lemma OAI.SubpolynomialLp.localization_integral_bound line 158