OAI/Geometry/NodalSets/Elliptic/RealCompactL2MapLemmas.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Yau.real_compact_mul_ae line 11
2. def OAI.Yau.realCompactL2Linear line 21
3. theorem OAI.Yau.realCompactL2Linear_bound line 49
4. def OAI.Yau.realCompactL2Map line 69
5. theorem OAI.Yau.realCompactL2Map_ae line 76
6. theorem OAI.Yau.real_indicator_weighted_bound line 82