OAI/Geometry/TamingCompatibility/DifferentialForms/RadialGeometricAssembly.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.ManifoldForms.smoothDdc line 18
2. lemma OAI.TamingCompatibility.ManifoldForms.smoothDdc_closed line 22
3. def OAI.TamingCompatibility.GeometricHilbert.correctedDdc line 37
4. lemma OAI.TamingCompatibility.GeometricHilbert.correctedDdc_closed line 43
5. lemma OAI.TamingCompatibility.GeometricHilbert.correctedDdc_invariant line 54
6. lemma OAI.TamingCompatibility.GeometricHilbert.smoothAnti_ddc_cutoffLog line 73
7. lemma OAI.TamingCompatibility.GeometricHilbert.smoothAnti_ddc_cutoffSqrt line 104
8. def OAI.TamingCompatibility.GeometricHilbert.nonharmonicCorrectionLM line 152
9. theorem OAI.TamingCompatibility.GeometricHilbert.nonharmonic_geometric_cutoffLog_estimate line 170
10. theorem OAI.TamingCompatibility.GeometricHilbert.nonharmonic_geometric_cutoffSqrt_estimate line 212