OAI/Analysis/AncientFlat/Profile/CompactificationCoeff.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ParabolicAnnular.compactArgument line 8
2. def OAI.ParabolicAnnular.compactPrincipal line 9
3. def OAI.ParabolicAnnular.compactPotential line 10
4. lemma OAI.ParabolicAnnular.compactArgument_smooth line 12
5. lemma OAI.ParabolicAnnular.compactArgument_nonneg line 16
6. lemma OAI.ParabolicAnnular.compactification_pos line 18
7. lemma OAI.ParabolicAnnular.compactPrincipal_smooth line 25
8. lemma OAI.ParabolicAnnular.compactPotential_smooth line 29