OAI/MathematicalPhysics/ContinuumCoulomb/OneParticle/SplitFormIntegrals.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Integrability of the actual sliced forms. These lemmas justify applying Fubini and integrating the published one-dimensional and planar estimates.

  1. theorem OAI.ContinuumCoulomb.split_square_integrable line 13
  2. theorem OAI.ContinuumCoulomb.split_potential_integrable line 18
  3. theorem OAI.ContinuumCoulomb.split_planar_slice_contDiff line 26
  4. theorem OAI.ContinuumCoulomb.split_vertical_slice_contDiff line 30
  5. theorem OAI.ContinuumCoulomb.split_planar_mass_integral line 34
  6. theorem OAI.ContinuumCoulomb.split_vertical_mass_integral line 42
  7. theorem OAI.ContinuumCoulomb.split_planar_form_integrable line 50
  8. theorem OAI.ContinuumCoulomb.split_vertical_form_integrable line 74