OAI/Geometry/TamingCompatibility/Hodge/HodgeScaleSmoothing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.hodgeScaleInput line 19
2. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeScaleInput_spec line 27
3. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeScaleInput_bound line 55
4. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_uniform_local_H5 line 112
5. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_factor line 154
6. theorem OAI.TamingCompatibility.GeometricHilbert.hodgeInclusion_compact line 168
7. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeEnergyToH1_injective line 174
8. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeResolvent_compact line 183
9. lemma OAI.TamingCompatibility.GeometricHilbert.hodgeRegularization_compact line 190