OAI/Geometry/TamingCompatibility/Charts/ChartEnergyIntegral.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricChart.cutoffForm line 21
2. lemma OAI.TamingCompatibility.GeometricChart.cutoffForm_smooth line 24
3. lemma OAI.TamingCompatibility.GeometricChart.cutoffForm_anti line 27
4. lemma OAI.TamingCompatibility.GeometricChart.pairing_chart line 45
5. lemma OAI.TamingCompatibility.GeometricChart.localizedPairing_eq_coordinateIntegrand line 68
6. lemma OAI.TamingCompatibility.GeometricChart.cutoff_square_tsupport line 83
7. lemma OAI.TamingCompatibility.GeometricChart.localizedPairing_integrable line 92
8. lemma OAI.TamingCompatibility.GeometricChart.integral_localizedPairing line 107
9. lemma OAI.TamingCompatibility.GeometricChart.localizedFunction_anti line 143
10. lemma OAI.TamingCompatibility.GeometricChart.scalar_expansion line 173