Square integrability of the space-time fields on slabs #
Each spatial slice of a weighted field is the inverse Fourier transform of a
square-integrable frequency field, so its L² norm is bounded by the norm of
the frequency field. Integrating over time, a space-time field whose frequency
path is bounded on [δ,T] is square integrable on the slab ℝ³ × (δ,T), as
required by thm:regularised (R2).
theorem
CKN.Leray.regR12WeightedField_slice_lintegral_le
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
[CompleteSpace E]
(M : Foundation.Parabolic.L2Vec3 → ℂ)
(hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume)
(C : ℝ)
(hC : 0 ≤ C)
(hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2))
(G : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))
:
∫⁻ (x : Foundation.Parabolic.Vec3), ‖regR12WeightedField M G (WithLp.toLp 2 x)‖ₑ ^ 2 ≤ ENNReal.ofReal (C * ‖G‖) ^ 2
The slice of a weighted field is square integrable, with norm at most
C ‖G‖.
theorem
CKN.Leray.regR12SpaceTimeField_memLp_slab
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℂ E]
[CompleteSpace E]
(c : E →L[ℝ] ℝ)
(M : Foundation.Parabolic.L2Vec3 → ℂ)
(hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume)
(C : ℝ)
(hC : 0 ≤ C)
(hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2))
(G : ℝ → ↥(MeasureTheory.Lp E 2 MeasureTheory.volume))
(hG : Continuous G)
(δ T B : ℝ)
(hB : ∀ t ∈ Set.Ioo δ T, ‖G t‖ ≤ B)
:
MeasureTheory.MemLp (regR12SpaceTimeField c M G) 2 (MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo δ T)))
A space-time field whose frequency path is bounded on (δ,T) is square
integrable on the slab ℝ³ × (δ,T).