OAI/Geometry/TamingCompatibility/Elliptic/AntiChartH1.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.antiGraph_norm_sq line 20
2. def OAI.TamingCompatibility.GeometricHilbert.antiToEnergy line 32
3. lemma OAI.TamingCompatibility.GeometricHilbert.antiToEnergy_dense line 35
4. def OAI.TamingCompatibility.GeometricHilbert.antiToH1 line 38
5. lemma OAI.TamingCompatibility.GeometricHilbert.antiToH1_bound line 42
6. def OAI.TamingCompatibility.GeometricHilbert.energyToH1 line 73
7. lemma OAI.TamingCompatibility.GeometricHilbert.energyToH1_smooth line 77