OAI/Geometry/TamingCompatibility/Charts/LocalizedHnat.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_add line 22
2. lemma OAI.TamingCompatibility.HilbertSobolev.schwartzToH_real_smul line 27
3. theorem OAI.TamingCompatibility.HilbertSobolev.cutoff_source_Hnat line 32
4. theorem OAI.TamingCompatibility.HilbertSobolev.localized_normalized_source_Hnat line 90
5. theorem OAI.TamingCompatibility.HilbertSobolev.parameter_local_source_two_jet line 126