OAI/Geometry/TamingCompatibility/Elliptic/CriticalManifoldSobolev.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.pairLinear_compact line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.pair_energy_L4_bound line 31
3. lemma OAI.TamingCompatibility.GeometricHilbert.component_energy_L4_bound line 48
4. def OAI.TamingCompatibility.GeometricHilbert.energyToL4 line 64
5. lemma OAI.TamingCompatibility.GeometricHilbert.energyToL4_smooth line 70