OAI/Analysis/CoulombRadii/FormDomain/L2MultiplierContinuity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.real_multiplier_inner line 15
2. lemma OAI.Coulomb.real_multiplier_quadratic line 24
3. lemma OAI.Coulomb.real_multiplier_quadratic_diff_bound line 37
4. lemma OAI.Coulomb.real_multiplier_quadratic_tendsto line 51
5. lemma OAI.Coulomb.H1Vector.hardy_multiplier_memLp line 78
6. def OAI.Coulomb.H1Vector.hardyMultiplier line 88
7. lemma OAI.Coulomb.H1Vector.hardyMultiplier_ae line 91
8. lemma OAI.Coulomb.H1Vector.hardyMultiplier_norm_sq line 94
9. lemma OAI.Coulomb.H1Vector.hardyMultiplier_norm_le line 112
10. lemma OAI.Coulomb.hardy_form_strong_tendsto line 118
11. lemma OAI.Coulomb.h1_bounded_tight_compact line 143