OAI/Geometry/TamingCompatibility/Concentration/ConcentrationChart.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCompact line 22
2. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCompact_compact line 26
3. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCompact_target line 30
4. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCompact_center line 37
5. structure OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.ConcentrationCutoff line 45
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCutoff_nonempty line 52
7. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.concentrationCutoff line 56
8. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.ConcentrationCutoff.bump line 62
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.ParametrixData.ConcentrationCutoff.reflected_support line 65
10. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.localConcentration line 86
11. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.localConcentration_smooth line 91
12. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch line 97
13. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_smooth line 101
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationPatch_apply line 109
15. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration line 118
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_smooth line 121
17. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.localConcentration_nonneg line 127
18. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalConcentration_nonneg line 134
19. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationDensity line 161
20. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationDensity_integrable line 167
21. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationDensity_nonneg line 176
22. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.localConcentration_integral line 185
23. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partition_center_ball line 194
24. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.concentrationDensity_near line 202