HomogeneousDerivativeTesting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Schwartz testing of the completed physical derivatives

The bounded L² derivative on Y is the weak derivative of its faithful physical representative. The test derivative is written in reverse order, as required by transposition, and the sign is exactly (-1)^N.

theorem OAI.DefocusingNLS.cZero_point_norm_le line 21
theorem OAI.DefocusingNLS.integrable_cZero_test line 25
def OAI.DefocusingNLS.physicalSchwartzTest line 37
Source documentation
A Schwartz test acts continuously on the physical C0 realization.
```
noncomputable def physicalSchwartzTest (ψ : 𝓢(E, ℂ)) : C₀(E, ℂ) →L[ℝ] ℝ := by
…
```
theorem OAI.DefocusingNLS.physicalSchwartzTest_apply line 60

theorem OAI.DefocusingNLS.schwartz_iteratedDerivative_testing line 64

Source documentation

The transposed ordered derivative has the reversed list of directions.

theorem schwartz_iteratedDerivative_testing (N : ℕ) (v : Fin N → E)
    (ψ f : 𝓢(E, ℂ)) :
    (∫ x : E, inner ℝ (ψ x) ((∂^{v} f) x)) =
      (-1 : ℝ) ^ N * ∫ x : E, inner ℝ ((∂^{fun i => v (Fin.rev i)} ψ) x) (f x) := by
…

theorem OAI.DefocusingNLS.homogeneousPhysicalDerivative_testing line 90

Source documentation

Completed ordered derivatives satisfy the exact weak integration-by-parts identity against every Schwartz test.

theorem homogeneousPhysicalDerivative_testing (a : ℝ) (N : ℕ)
    (ha : 0 < a) (ha1 : a < 1) (hk : 8 < (N : ℝ))
    (j : Fin N → Fin 12) (ψ : 𝓢(E, ℂ)) (u : HomogeneousY a N) :
    inner ℝ (ψ.toLp 2 volume) (homogeneousPhysicalDerivative a N ha ha1 hk j u) =
      (-1 : ℝ) ^ N * ∫ x : E,
        inner ℝ ((∂^{fun i => (EuclideanSpace.basisFun (Fin 12) ℝ) (j (Fin.rev i))} ψ) x)
          (homogeneousPhysicalCLM a N ha ha1 hk u x) := by
…

Mentions: OAI.DefocusingNLS.HomogeneousY, OAI.DefocusingNLS.homogeneousPhysicalDerivative, OAI.DefocusingNLS.homogeneousPhysicalCLM