OAI/Geometry/TamingCompatibility/Charts/GeometricCutoff.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.MetricForms.pairing_sub_self_le line 17
2. lemma OAI.TamingCompatibility.antiInvariant_fun_smul line 32
3. lemma OAI.TamingCompatibility.codifferential_fun_smul_anti line 44
4. lemma OAI.TamingCompatibility.pairing_star_wedge_anti line 64
5. lemma OAI.TamingCompatibility.cutoff_delta_pointwise line 88
6. def OAI.TamingCompatibility.GeometricChart.localDelta line 119
7. lemma OAI.TamingCompatibility.GeometricChart.localizedFunction_eq_cutoff line 124
8. lemma OAI.TamingCompatibility.GeometricChart.localDelta_eq line 132
9. lemma OAI.TamingCompatibility.GeometricChart.cutoffDelta_zero_off line 145
10. lemma OAI.TamingCompatibility.GeometricChart.localDelta_zero_off line 157
11. lemma OAI.TamingCompatibility.GeometricChart.cutoffDelta_pairing_tsupport line 169
12. lemma OAI.TamingCompatibility.GeometricChart.localDelta_density_integrable line 184
13. lemma OAI.TamingCompatibility.GeometricChart.integral_localDelta_density line 196