OAI/Geometry/TamingCompatibility/DifferentialForms/ParameterCoefficients.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.parameter_derivative_smooth line 19
2. lemma OAI.TamingCompatibility.HilbertSobolev.parameter_coefficientSize_continuous_family line 29
3. def OAI.TamingCompatibility.HilbertSobolev.movingFrozenCoefficient line 45
4. lemma OAI.TamingCompatibility.HilbertSobolev.movingFrozenCoefficient_apply line 52
5. lemma OAI.TamingCompatibility.HilbertSobolev.movingFrozenCoefficient_size_continuous line 56
6. lemma OAI.TamingCompatibility.HilbertSobolev.movingFrozenCoefficient_zero line 68
7. lemma OAI.TamingCompatibility.HilbertSobolev.movingFrozenCoefficient_size_tendsto_zero line 74
8. lemma OAI.TamingCompatibility.HilbertSobolev.moving_scaledCoefficient_size_continuous line 82
9. def OAI.TamingCompatibility.HilbertSobolev.movingFrozenPrincipal line 95
10. lemma OAI.TamingCompatibility.HilbertSobolev.moving_frozen_principal_size_tendsto line 101
11. theorem OAI.TamingCompatibility.HilbertSobolev.moving_frozen_perturbation_norm_tendsto line 115