OAI/Analysis/CoulombIonization/RadialBounds/RotationIntegralBarrier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombAnalysis.rotation_spatial_integral line 20
2. lemma OAI.CoulombAnalysis.sphereMean_indicator line 39
3. theorem OAI.CoulombAnalysis.rotation_annular_L1 line 54
4. lemma OAI.CoulombAnalysis.compact_away_zero_annulus line 91
5. lemma OAI.CoulombAnalysis.compact_closed_annulus line 102
6. lemma OAI.CoulombAnalysis.screened_field_continuousOn line 109
7. lemma OAI.CoulombAnalysis.screened_field_measurable line 116
8. theorem OAI.CoulombAnalysis.screened_field_local_L1 line 123
9. theorem OAI.CoulombAnalysis.screened_field_normal_family line 160