OAI/Analysis/CoulombIonization/FieldAnalysis/WeightedAverage.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CoulombNeumann.bounded_average_section_integrable line 17
2. lemma OAI.CoulombNeumann.bounded_average_joint_integrable line 26
3. theorem OAI.CoulombNeumann.weighted_average_fubini line 47
4. theorem OAI.CoulombNeumann.weighted_average_bound line 54
5. abbrev OAI.CoulombNeumann.CubePartition line 72
6. def OAI.CoulombNeumann.cubePartitionMeasure line 73
7. instance OAI.CoulombNeumann.cubePartition_probability line 74
8. lemma OAI.CoulombNeumann.physicalGridPressure_partition_integrable line 78
9. lemma OAI.CoulombNeumann.physicalPressureAverage_partition line 87
10. lemma OAI.CoulombNeumann.physicalPressureAverage_value_integrable line 94
11. lemma OAI.CoulombNeumann.physicalPressure_value_integrable line 101
12. theorem OAI.CoulombAtom.SobolevFermion.neumann_averaged_pressure line 113
13. theorem OAI.CoulombAtom.SobolevFermion.neumann_radial_smear line 125
14. theorem OAI.CoulombAtom.FormAdmissible.neumann_radial_smear line 134