HomogeneousRadialMeasure.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Exact radial Jacobian and Schwartz radial tests in dimension twelve

theorem OAI.DefocusingNLS.integral_physicalRadiusMeasure line 14
Source documentation
The polar radial measure is precisely r¹¹ dr, with no normalization factor.
```
theorem integral_physicalRadiusMeasure (F : ℝ → ℂ) :
    (∫ r : PhysicalPositiveRadius, F r ∂physicalRadiusMeasure) =
      ∫ r in Ioi (0 : ℝ), (r ^ (11 : ℕ) : ℝ) • F r := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure
theorem OAI.DefocusingNLS.memLp_radialSchwartz line 30
Source documentation
Schwartz radial tests remain square-integrable against the polar Jacobian.
```
theorem memLp_radialSchwartz (ψ : 𝓢(ℝ, ℂ)) :
    MemLp (fun r : PhysicalPositiveRadius => ψ r) 2 physicalRadiusMeasure := by
…
```
Mentions: OAI.DefocusingNLS.PhysicalPositiveRadius, OAI.DefocusingNLS.physicalRadiusMeasure
theorem OAI.DefocusingNLS.integral_Ioi_eq_of_zero_nonpositive line 61
Source documentation
A test supported on the positive half-line has the same full-line integral.
```
theorem integral_Ioi_eq_of_zero_nonpositive (F : ℝ → ℂ)
    (hF : ∀ r, r ≤ 0 → F r = 0) :
    (∫ r in Ioi (0 : ℝ), F r) = ∫ r, F r := by
…
```
def OAI.DefocusingNLS.radialWeightedSchwartzTest line 72
Source documentation
Absorb the twelve-dimensional radial Jacobian into a Schwartz test.
```
noncomputable def radialWeightedSchwartzTest (ψ : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) :=
…
```
theorem OAI.DefocusingNLS.radialWeightedSchwartzTest_apply line 75
def OAI.DefocusingNLS.radialTransposedTest line 81
Source documentation
The transposed radial derivative includes the exact Jacobian.
```
noncomputable def radialTransposedTest (N : ℕ) (ψ : 𝓢(ℝ, ℂ)) : 𝓢(ℝ, ℂ) :=
…
```
theorem OAI.DefocusingNLS.tsupport_radialWeightedSchwartzTest_subset line 84
theorem OAI.DefocusingNLS.tsupport_radialTransposedTest_subset line 92