HomogeneousLocalRadialTesting.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local radial integration by parts with a smooth test

Only derivatives on the support of the test are used. This is the local classical side of the distributional identification; exterior solutions need no artificial extension through the origin.

theorem OAI.DefocusingNLS.integrable_compactTest_mul line 18
def OAI.DefocusingNLS.scalarSchwartzJet line 28
theorem OAI.DefocusingNLS.scalarSchwartzJet_apply line 31

theorem OAI.DefocusingNLS.local_radial_iterated_integration_by_parts line 43

Source documentation

Classical local jets satisfy the full transposed identity against each smooth compactly supported test in their domain.

theorem local_radial_iterated_integration_by_parts (U : Set ℝ)
    (F : ℕ → ℝ → ℂ)
    (hF : ∀ j r, r ∈ U → HasDerivAt (F j) (F (j + 1) r) r)
    (N : ℕ) (ψ : 𝓢(ℝ, ℂ)) (hc : HasCompactSupport ψ) (hs : tsupport ψ ⊆ U) :
    (∫ r : ℝ, ψ r * F N r) =
      (-1 : ℂ) ^ N * ∫ r : ℝ, scalarSchwartzJet N ψ r * F 0 r := by
…

Mentions: OAI.DefocusingNLS.scalarSchwartzJet