Inverse Fourier integrals of weighted square-integrable fields

For the pointwise realization in thm:regularised (R2), a spatial field is represented by the inverse Fourier integral of its Fourier transform. When the transform is an inverse Bessel weight of order four times a square-integrable field, it is integrable against every polynomial weight of degree at most two. The inverse Fourier integral is then continuous, differentiable with the derivative given by multiplication in frequency, and represents the L² inverse Fourier transform.

theorem CKN.Leray.regR12_fourierInv_fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {h : Foundation.Parabolic.L2Vec3 → E} (hh : MeasureTheory.Integrable h MeasureTheory.volume) (hh1 : MeasureTheory.Integrable (fun (v : Foundation.Parabolic.L2Vec3) => ‖v‖ * ‖h v‖) MeasureTheory.volume) (x e : Foundation.Parabolic.L2Vec3) : HasFDerivAt (FourierTransformInv.fourierInv h) (fderiv ℝ (FourierTransformInv.fourierInv h) x) x ∧ (fderiv ℝ (FourierTransformInv.fourierInv h) x) e = FourierTransformInv.fourierInv (fun (v : Foundation.Parabolic.L2Vec3) => (↑(2 * Real.pi * inner ℝ v e) * Complex.I) • h v) x

The directional derivative of the inverse Fourier integral.

theorem CKN.Leray.regR12_norm_fourierInv_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (h : Foundation.Parabolic.L2Vec3 → E) (hh : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) (x : Foundation.Parabolic.L2Vec3) : ‖FourierTransformInv.fourierInv h x‖ ≤ (MeasureTheory.eLpNorm h 1 MeasureTheory.volume).toReal

The inverse Fourier integral is bounded by the L¹ norm.

theorem CKN.Leray.regR12_fourierInv_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (h₁ h₂ : Foundation.Parabolic.L2Vec3 → E) (hh₁ : MeasureTheory.Integrable h₁ MeasureTheory.volume) (hh₂ : MeasureTheory.Integrable h₂ MeasureTheory.volume) (x : Foundation.Parabolic.L2Vec3) : FourierTransformInv.fourierInv (fun (v : Foundation.Parabolic.L2Vec3) => h₁ v - h₂ v) x = FourierTransformInv.fourierInv h₁ x - FourierTransformInv.fourierInv h₂ x

The inverse Fourier integral is additive on integrable fields.

theorem CKN.Leray.regR12_fourierInv_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (h : Foundation.Parabolic.L2Vec3 → E) (hh : MeasureTheory.Integrable h MeasureTheory.volume) : Continuous (FourierTransformInv.fourierInv h)

The inverse Fourier integral of an integrable field is continuous.

theorem CKN.Leray.regR12_integral_smul_fourierInv {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (h : Foundation.Parabolic.L2Vec3 → E) (hh : MeasureTheory.Integrable h MeasureTheory.volume) (φ : SchwartzMap Foundation.Parabolic.L2Vec3 ℂ) : ∫ (x : Foundation.Parabolic.L2Vec3), φ x • FourierTransformInv.fourierInv h x = ∫ (ξ : Foundation.Parabolic.L2Vec3), FourierTransformInv.fourierInv (⇑φ) ξ • h ξ

The pairing of the inverse Fourier integral of an integrable field with a Schwartz function.

theorem CKN.Leray.regR12_fourierInv_ae_eq_L2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] (h : Foundation.Parabolic.L2Vec3 → E) (hh : MeasureTheory.Integrable h MeasureTheory.volume) (hh2 : MeasureTheory.MemLp h 2 MeasureTheory.volume) : FourierTransformInv.fourierInv h =ᵐ[MeasureTheory.volume] ↑↑(FourierTransformInv.fourierInv (MeasureTheory.MemLp.toLp h hh2))

The inverse Fourier integral of an integrable, square-integrable field represents its L² inverse Fourier transform.

noncomputable def CKN.Leray.regR12Kernel (ξ : Foundation.Parabolic.L2Vec3) : ℝ

The inverse Bessel weight (1 + |ξ|²)⁻¹ of order two, square integrable in three dimensions.

Equations

• CKN.Leray.regR12Kernel ξ = (1 + ‖ξ‖ ^ 2) ^ (-1)

theorem CKN.Leray.regR12Kernel_continuous : Continuous regR12Kernel

theorem CKN.Leray.regR12Kernel_memLp : MeasureTheory.MemLp regR12Kernel 2 MeasureTheory.volume

theorem CKN.Leray.regR12_weighted_eLpNorm_one_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : Foundation.Parabolic.L2Vec3 → E) (hG : MeasureTheory.AEStronglyMeasurable G MeasureTheory.volume) : MeasureTheory.eLpNorm (fun (ξ : Foundation.Parabolic.L2Vec3) => M ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • G ξ) 1 MeasureTheory.volume ≤ ENNReal.ofReal C * MeasureTheory.eLpNorm regR12Kernel 2 MeasureTheory.volume * MeasureTheory.eLpNorm G 2 MeasureTheory.volume

A multiplier of at most quadratic growth, times the inverse Bessel weight of order four, sends square-integrable fields to integrable fields.

theorem CKN.Leray.regR12_weighted_integrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : Foundation.Parabolic.L2Vec3 → E) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume) : MeasureTheory.Integrable (fun (ξ : Foundation.Parabolic.L2Vec3) => M ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • G ξ) MeasureTheory.volume

The multiplied weighted field is integrable.

noncomputable def CKN.Leray.regR12WeightedField {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (G : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (x : Foundation.Parabolic.L2Vec3) : E

The inverse Fourier integral of a square-integrable frequency field G, multiplied by M and the inverse Bessel weight of order four.

Equations

• CKN.Leray.regR12WeightedField M G x = FourierTransformInv.fourierInv (fun (ξ : CKN.Foundation.Parabolic.L2Vec3) => M ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • ↑↑G ξ) x

theorem CKN.Leray.regR12Weight_continuous : Continuous fun (ξ : Foundation.Parabolic.L2Vec3) => ↑((1 + ‖ξ‖ ^ 2) ^ (-2))

theorem CKN.Leray.regR12WeightedField_norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ 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.L2Vec3) : ‖regR12WeightedField M G x‖ ≤ C * (MeasureTheory.eLpNorm regR12Kernel 2 MeasureTheory.volume).toReal * ‖G‖

The weighted field is bounded by the L² norm of the frequency field.

theorem CKN.Leray.regR12WeightedField_sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G H : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (x : Foundation.Parabolic.L2Vec3) : regR12WeightedField M G x - regR12WeightedField M H x = regR12WeightedField M (G - H) x

The weighted field is linear in the frequency field.

theorem CKN.Leray.regR12WeightedField_continuous {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) : Continuous fun (p : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume) × Foundation.Parabolic.L2Vec3) => regR12WeightedField M p.1 p.2

The weighted field is jointly continuous in the frequency field and the spatial point.

noncomputable def CKN.Leray.regR12DirSymbol (e ξ : Foundation.Parabolic.L2Vec3) : ℂ

The frequency multiplier 2πi⟨ξ, e⟩ of the directional derivative along e.

Equations

• CKN.Leray.regR12DirSymbol e ξ = ↑(2 * Real.pi * inner ℝ ξ e) * Complex.I

theorem CKN.Leray.regR12DirSymbol_continuous (e : Foundation.Parabolic.L2Vec3) : Continuous (regR12DirSymbol e)

theorem CKN.Leray.regR12DirSymbol_norm_le (e ξ : Foundation.Parabolic.L2Vec3) : ‖regR12DirSymbol e ξ‖ ≤ 2 * Real.pi * ‖e‖ * ‖ξ‖

theorem CKN.Leray.regR12WeightedField_fderiv_apply {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (M : Foundation.Parabolic.L2Vec3 → ℂ) (hM : MeasureTheory.AEStronglyMeasurable M MeasureTheory.volume) (C : ℝ) (hC : 0 ≤ C) (hMC : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (hMC1 : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖ξ‖ * ‖M ξ‖ ≤ C * (1 + ‖ξ‖ ^ 2)) (G : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (x e : Foundation.Parabolic.L2Vec3) : HasFDerivAt (regR12WeightedField M G) (fderiv ℝ (regR12WeightedField M G) x) x ∧ (fderiv ℝ (regR12WeightedField M G) x) e = regR12WeightedField (fun (ξ : Foundation.Parabolic.L2Vec3) => regR12DirSymbol e ξ * M ξ) G x

The weighted field is differentiable when the multiplier grows at most linearly, and its directional derivative multiplies the frequency field by 2πi⟨ξ, e⟩.

theorem CKN.Leray.regR12WeightedField_ae_eq {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 H : ↥(MeasureTheory.Lp E 2 MeasureTheory.volume)) (hGH : ↑↑((MeasureTheory.Lp.fourierTransformₗᵢ Foundation.Parabolic.L2Vec3 E) H) =ᵐ[MeasureTheory.volume] fun (ξ : Foundation.Parabolic.L2Vec3) => M ξ • ↑((1 + ‖ξ‖ ^ 2) ^ (-2)) • ↑↑G ξ) : regR12WeightedField M G =ᵐ[MeasureTheory.volume] ↑↑H

The weighted field represents every L² field whose Fourier transform is the weighted frequency field.