OAI/Geometry/TamingCompatibility/Charts/LocalInverse.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.LocalRellich.localInverse line 22
2. lemma OAI.TamingCompatibility.LocalRellich.localInverse_norm_le line 29
3. theorem OAI.TamingCompatibility.LocalRellich.localInverse_compact_of_support line 38
4. def OAI.TamingCompatibility.RellichTail.cutoff line 85
5. lemma OAI.TamingCompatibility.RellichTail.cutoff_memLp_top line 87
6. lemma OAI.TamingCompatibility.RellichTail.cutoff_memLp_two line 91
7. lemma OAI.TamingCompatibility.RellichTail.cutoff_support line 99
8. lemma OAI.TamingCompatibility.RellichTail.cutoff_lp_eq line 105
9. lemma OAI.TamingCompatibility.RellichTail.tail_norm_le line 110
10. lemma OAI.TamingCompatibility.LocalRellich.localInverse_sub line 141
11. lemma OAI.TamingCompatibility.LocalRellich.localInverse_sub_norm_le line 152
12. theorem OAI.TamingCompatibility.LocalRellich.localInverse_compact_of_decay line 158