OAI/Analysis/CoulombRadii/FieldAnalysis/CubeMeasure.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Coulomb.tensorPair_inner line 16
  2. lemma OAI.Coulomb.neumann_tensor_coefficient_derivative line 31
  3. theorem OAI.Coulomb.neumann_tensor_smooth_spectral_lower line 55
  4. def OAI.Coulomb.cubeMeasure line 91
  5. instance OAI.Coulomb.cubeMeasure_isFiniteMeasure line 94
  6. def OAI.Coulomb.cubeMode line 98
  7. def OAI.Coulomb.splitCube line 101
  8. lemma OAI.Coulomb.splitCube_measurePreserving line 106
  9. lemma OAI.Coulomb.splitCube_symm_apply line 111
  10. lemma OAI.Coulomb.splitCube_apply line 114
  11. lemma OAI.Coulomb.cubeMode_insertNth line 117
  12. theorem OAI.Coulomb.cube_smooth_axis_spectral_lower line 124
  13. lemma OAI.Coulomb.inner_toLp_real line 167
  14. lemma OAI.Coulomb.norm_toLp_sq_real line 175
  15. lemma OAI.Coulomb.integral_mul_sq_le line 181
  16. lemma OAI.Coulomb.integral_norm_sq_le_measure line 188
  17. lemma OAI.Coulomb.unifIntegrable_of_sq_bound line 195
  18. lemma OAI.Coulomb.integral_le_of_ae_tendsto_of_frequently_le line 230
  19. theorem OAI.Coulomb.tendsto_integral_sq_sub_of_ae_of_sq_le line 256
  20. lemma OAI.Coulomb.euclidean_convolution_sq_le line 298
  21. lemma OAI.Coulomb.euclidean_convolution_sq_integral_le line 331
  22. lemma OAI.Coulomb.euclidean_real_convolution_comm line 356
  23. lemma OAI.Coulomb.euclidean_fderiv_const_sub_comp line 363
  24. lemma OAI.Coulomb.euclidean_weak_convolution_partial line 372
  25. def OAI.Coulomb.euclideanMollifier line 393
  26. lemma OAI.Coulomb.euclideanMollifier_tendsto line 399
  27. def OAI.Coulomb.realMollify line 404
  28. lemma OAI.Coulomb.realMollify_contDiff line 408
  29. lemma OAI.Coulomb.realMollify_memLp line 414
  30. lemma OAI.Coulomb.realMollify_sq_integral_le line 424
  31. lemma OAI.Coulomb.realMollify_ae_tendsto line 433