OAI/Geometry/TamingCompatibility/Elliptic/FrozenCoefficient.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.continuous_bounded_family line 17
2. lemma OAI.TamingCompatibility.HilbertSobolev.family_derivative_smooth line 40
3. lemma OAI.TamingCompatibility.HilbertSobolev.coefficientSize_continuous_family line 50
4. def OAI.TamingCompatibility.HilbertSobolev.frozenCoefficient line 66
5. lemma OAI.TamingCompatibility.HilbertSobolev.frozenCoefficient_apply line 73
6. lemma OAI.TamingCompatibility.HilbertSobolev.frozenCoefficient_zero line 78
7. lemma OAI.TamingCompatibility.HilbertSobolev.coefficientSize_zero line 84
8. theorem OAI.TamingCompatibility.HilbertSobolev.frozenCoefficient_size_tendsto_zero line 92
9. def OAI.TamingCompatibility.HilbertSobolev.frozenPrincipal line 112
10. lemma OAI.TamingCompatibility.HilbertSobolev.frozen_principal_size_tendsto line 118
11. lemma OAI.TamingCompatibility.HilbertSobolev.frozen_weak_size_tendsto line 132
12. theorem OAI.TamingCompatibility.HilbertSobolev.frozen_perturbation_norm_tendsto line 146
13. theorem OAI.TamingCompatibility.HilbertSobolev.frozen_weak_norm_tendsto line 156
14. theorem OAI.TamingCompatibility.HilbertSobolev.frozen_eventually_H1_regular line 166