OAI/Geometry/TamingCompatibility/DifferentialForms/UniformInterior.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.HilbertSobolev.norm_comp_three line 16
2. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerH_norm_le line 22
3. lemma OAI.TamingCompatibility.HilbertSobolev.localizationErrorH_norm_le line 39
4. def OAI.TamingCompatibility.HilbertSobolev.scaledCoefficient line 64
5. lemma OAI.TamingCompatibility.HilbertSobolev.scaledCoefficient_size_continuous line 71
6. lemma OAI.TamingCompatibility.HilbertSobolev.matrixLowerH_eventually_bounded line 83
7. lemma OAI.TamingCompatibility.HilbertSobolev.localizationErrorH_eventually_bounded line 110