OAI/Analysis/CoulombRadii/FieldAnalysis/ComplexMollify.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Coulomb.realMollify_L2_tendsto line 18
2. def OAI.Coulomb.complexMollify line 24
3. lemma OAI.Coulomb.complexMollify_contDiff line 29
4. lemma OAI.Coulomb.complexMollify_memLp line 37
5. lemma OAI.Coulomb.complexMollify_sq_sub line 44
6. theorem OAI.Coulomb.complexMollify_L2_tendsto line 51
7. lemma OAI.Coulomb.toLp_tendsto_of_integral_sq_sub line 65
8. lemma OAI.Coulomb.integral_norm_sq_tendsto_of_L2 line 80
9. lemma OAI.Coulomb.integral_coefficient_tendsto_of_L2 line 87
10. lemma OAI.Coulomb.integral_sq_sub_restrict_tendsto line 97
11. lemma OAI.Coulomb.mollify_realCLM_mul_ofReal line 107
12. lemma OAI.Coulomb.euclidean_weak_complex_component line 112
13. lemma OAI.Coulomb.realMollify_fderiv line 132
14. lemma OAI.Coulomb.complexMollify_fderiv line 142
15. lemma OAI.Coulomb.cubeMeasure_le_volume line 165
16. lemma OAI.Coulomb.insertNth_path_hasDerivAt line 171
17. lemma OAI.Coulomb.euclidean_hasDerivAt_insertNth line 186
18. theorem OAI.Coulomb.cube_weak_axis_spectral_lower line 192
19. theorem OAI.Coulomb.cube_weak_axis_all_frequencies line 251
20. theorem OAI.Coulomb.cube_weak_spectral_lower line 299
21. def OAI.Coulomb.latticeRadius line 317
22. def OAI.Coulomb.integerCell line 320
23. lemma OAI.Coulomb.integerCell_measurable line 323
24. lemma OAI.Coulomb.integerCell_volume line 326
25. lemma OAI.Coulomb.integerCell_disjoint line 329
26. lemma OAI.Coulomb.piEuclidean_closedBall_volume line 342
27. lemma OAI.Coulomb.integerCell_card_le_ball_volume line 353
28. def OAI.Coulomb.signedCoordinate line 366
29. lemma OAI.Coulomb.signedCoordinate_injective line 368
30. def OAI.Coulomb.signedLattice line 372
31. lemma OAI.Coulomb.signedLattice_injective line 375
32. lemma OAI.Coulomb.signedCell_abs_le line 383
33. lemma OAI.Coulomb.signedCell_radius_le line 395
34. theorem OAI.Coulomb.spin_two_lattice_count line 417