OAI/MathematicalPhysics/DefocusingNLS/Linear/HomogeneousClassicalGreen.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Compact-test Green identity for the actual CĀ² physical realization

The physical function need not decay or have globally integrable derivatives: every integrand is localized by the compactly supported smooth test.

  1. theorem OAI.DefocusingNLS.continuous_laplacian_of_contDiff_two line 20
  2. theorem OAI.DefocusingNLS.hasCompactSupport_laplacian line 28
  3. theorem OAI.DefocusingNLS.compactSchwartz_mul_continuous line 39
  4. theorem OAI.DefocusingNLS.compactTest_second_directional_green line 44
  5. theorem OAI.DefocusingNLS.compactTest_laplacian_green line 92

    Source documentation

    Green's identity against a compact smooth test, for a globally CĀ² physical function with no additional integrability hypothesis.

    theorem compactTest_laplacian_green (Ļˆ : š“¢(E, ā„‚))
    (hc : HasCompactSupport Ļˆ) (F : E ā†’ ā„‚) (hF : ContDiff ā„ 2 F) :
    (āˆ« x : E, Ļˆ x * Ī” F x) = āˆ« x : E, Ī” (fun y => Ļˆ y) x * F x := by
ā€¦