Fourier algebra for the vector potential

These coordinate identities encode the curl-inverse-Laplacian symbol in eq:J-vector-potential.

@[reducible, inline]

abbrev CKN.FourierVec3 : Type

Complex-valued Euclidean three-vectors used as Fourier transform values.

Equations

• CKN.FourierVec3 = PiLp 2 fun (x : Fin 3) => ℂ

def CKN.complexifyVec3 (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Foundation.Parabolic.L2Vec3 → FourierVec3

A real spatial field, viewed on the Euclidean spatial carrier with complex-valued vector components.

Equations

• CKN.complexifyVec3 a x = WithLp.toLp 2 fun (i : Fin 3) => ↑(a x.ofLp i)

theorem CKN.complexifyVec3_memLp {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} (ha : MeasureTheory.MemLp a 2 MeasureTheory.volume) : MeasureTheory.MemLp (complexifyVec3 a) 2 MeasureTheory.volume

Complexification preserves square integrability on the Euclidean spatial carrier.

def CKN.frequencyL2Coord (i : Fin 3) : Foundation.Parabolic.L2Vec3 →L[ℝ] ℝ

The coordinate of a frequency vector when it is regarded as a point of the native Euclidean spatial carrier.

Equations

• CKN.frequencyL2Coord i = PiLp.proj 2 (fun (x : Fin 3) => ℝ) i

noncomputable def CKN.regularizedFrequencyCoord (δ : ℝ) (i : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : ℝ

A frequency coordinate rescaled by a positive regularization length.

Equations

• CKN.regularizedFrequencyCoord δ i ξ = δ⁻¹ * (CKN.frequencyL2Coord i) ξ

noncomputable def CKN.regularizedFrequencyWeight (δ : ℝ) (ξ : Foundation.Parabolic.L2Vec3) : ℝ

The regularized inverse of 1 + |ξ/δ|² used to remove the singularity at zero frequency from the potential multiplier.

Equations

• CKN.regularizedFrequencyWeight δ ξ = (1 + ‖δ⁻¹ • ξ‖ ^ 2) ^ (-1)

noncomputable def CKN.regularizedPotentialEntry (δ : ℝ) (i : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : ℂ

An entry of the regularized curl-inverse-Laplacian multiplier.

Equations

• CKN.regularizedPotentialEntry δ i ξ = Complex.I / (2 * ↑Real.pi * ↑δ) * ↑(CKN.regularizedFrequencyCoord δ i ξ) * ↑(CKN.regularizedFrequencyWeight δ ξ)

theorem CKN.regularizedFrequencyWeight_hasTemperateGrowth (δ : ℝ) : Function.HasTemperateGrowth (regularizedFrequencyWeight δ)

The regularized frequency weight is a smooth multiplier of temperate growth.

theorem CKN.regularizedFrequencyCoord_hasTemperateGrowth (δ : ℝ) (i : Fin 3) : Function.HasTemperateGrowth (regularizedFrequencyCoord δ i)

Each rescaled frequency coordinate has temperate growth.

theorem CKN.regularizedPotentialEntry_hasTemperateGrowth (δ : ℝ) (i : Fin 3) : Function.HasTemperateGrowth (regularizedPotentialEntry δ i)

The regularized potential multiplier entry is of temperate growth, so it acts on tempered distributions.

theorem CKN.frequencyL2Coord_abs_le (ξ : Foundation.Parabolic.L2Vec3) (i : Fin 3) : |(frequencyL2Coord i) ξ| ≤ ‖ξ‖

A coordinate of a vector in the Euclidean L² product norm is bounded by the full vector norm.

theorem CKN.regularizedFrequencyCoord_eq_scaled (δ : ℝ) (i : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : regularizedFrequencyCoord δ i ξ = (frequencyL2Coord i) (δ⁻¹ • ξ)

The scaled coordinate is the corresponding coordinate of the scaled frequency vector.

theorem CKN.regularizedFrequencyCoord_mul_weight_abs_le_one (δ : ℝ) (ξ : Foundation.Parabolic.L2Vec3) (i : Fin 3) : |regularizedFrequencyCoord δ i ξ * regularizedFrequencyWeight δ ξ| ≤ 1

The first-order regularized symbol is bounded by the input frequency vector.

theorem CKN.regularizedFrequencyCoordProduct_mul_weight_abs_le_one (δ : ℝ) (ξ : Foundation.Parabolic.L2Vec3) (i j : Fin 3) : |regularizedFrequencyCoord δ i ξ * regularizedFrequencyCoord δ j ξ * regularizedFrequencyWeight δ ξ| ≤ 1

The second-order regularized scalar multipliers are bounded by one.

theorem CKN.regularizedPotentialEntry_norm_le (δ : ℝ) (hδ : 0 < δ) (ξ : Foundation.Parabolic.L2Vec3) (i : Fin 3) : ‖regularizedPotentialEntry δ i ξ‖ ≤ 1 / (2 * Real.pi * δ)

The regularized vector-potential multiplier is bounded for each fixed positive regularization length.

noncomputable def CKN.regularizedDerivativeEntry (δ : ℝ) (k j : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : ℂ

A first-derivative multiplier entry for the regularized vector potential.

Equations

• CKN.regularizedDerivativeEntry δ k j ξ = -↑(CKN.regularizedFrequencyCoord δ k ξ * CKN.regularizedFrequencyCoord δ j ξ * CKN.regularizedFrequencyWeight δ ξ)

theorem CKN.regularizedDerivativeEntry_hasTemperateGrowth (δ : ℝ) (k j : Fin 3) : Function.HasTemperateGrowth (regularizedDerivativeEntry δ k j)

The first-derivative multiplier is of temperate growth.

theorem CKN.regularizedDerivativeEntry_norm_le (δ : ℝ) (k j : Fin 3) (ξ : Foundation.Parabolic.L2Vec3) : ‖regularizedDerivativeEntry δ k j ξ‖ ≤ 1

The first-derivative multiplier entry is bounded by one.

theorem CKN.regularizedDerivativeEntry_eq_frequency_mul_potential (δ : ℝ) (hδ : 0 < δ) (ξ : Foundation.Parabolic.L2Vec3) (k j : Fin 3) : regularizedDerivativeEntry δ k j ξ = 2 * ↑Real.pi * Complex.I * ↑((frequencyL2Coord k) ξ) * regularizedPotentialEntry δ j ξ

Multiplying a potential symbol by the Fourier derivative symbol gives the bounded first-derivative entry.

theorem CKN.boundedComplexMultiplier_memLp (g : Foundation.Parabolic.L2Vec3 → ℂ) (hg : Function.HasTemperateGrowth g) {C : ℝ} (hbound : ∀ (ξ : Foundation.Parabolic.L2Vec3), ‖g ξ‖ ≤ C) : MeasureTheory.MemLp g ⊤ MeasureTheory.volume

A bounded temperate complex multiplier belongs to L∞.

noncomputable def CKN.fourierMultiplyScalarL2 (g : Foundation.Parabolic.L2Vec3 → ℂ) (hg : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Multiplication by a bounded Fourier symbol on scalar L².

Equations

• CKN.fourierMultiplyScalarL2 g hg f = MeasureTheory.MemLp.toLp g hg • f

theorem CKN.fourierMultiplyScalarL2_tendsto_zero_of_tendsto_ae {g : ℕ → Foundation.Parabolic.L2Vec3 → ℂ} (hg : ∀ (n : ℕ), MeasureTheory.MemLp (g n) ⊤ MeasureTheory.volume) (hbound : ∀ (n : ℕ) (ξ : Foundation.Parabolic.L2Vec3), ‖g n ξ‖ ≤ 1) (hpoint : ∀ᵐ (ξ : Foundation.Parabolic.L2Vec3), Filter.Tendsto (fun (n : ℕ) => g n ξ) Filter.atTop (nhds 0)) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (↑↑(fourierMultiplyScalarL2 (g n) ⋯ f)) 2 MeasureTheory.volume) Filter.atTop (nhds 0)

A uniformly bounded sequence of Fourier multipliers that converges almost everywhere to zero converges strongly to zero on each square-integrable input.

theorem CKN.fourierMultiplyScalarL2_toTemperedDistribution_of_memLp (g : Foundation.Parabolic.L2Vec3 → ℂ) (hg : Function.HasTemperateGrowth g) (hmem : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.Lp.toTemperedDistribution (fourierMultiplyScalarL2 g hmem f) = (TemperedDistribution.smulLeftCLM ℂ g) (MeasureTheory.Lp.toTemperedDistribution f)

The same multiplier identity when the L∞ membership is supplied directly.

theorem CKN.inverseFourier_fourierMultiplyScalarL2_eq_fourierMultiplierCLM (g : Foundation.Parabolic.L2Vec3 → ℂ) (hg : Function.HasTemperateGrowth g) (hmem : MeasureTheory.MemLp g ⊤ MeasureTheory.volume) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : MeasureTheory.Lp.toTemperedDistribution (FourierTransformInv.fourierInv (fourierMultiplyScalarL2 g hmem (FourierTransform.fourier f))) = (TemperedDistribution.fourierMultiplierCLM ℂ g) (MeasureTheory.Lp.toTemperedDistribution f)

The inverse Fourier transform of an L² multiplier is the corresponding tempered-distribution Fourier multiplier.

theorem CKN.regularizedPotentialEntry_memLp (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) : MeasureTheory.MemLp (regularizedPotentialEntry δ i) ⊤ MeasureTheory.volume

The regularized potential coefficient is an L∞ Fourier multiplier.

theorem CKN.regularizedDerivativeEntry_memLp (δ : ℝ) (k j : Fin 3) : MeasureTheory.MemLp (regularizedDerivativeEntry δ k j) ⊤ MeasureTheory.volume

Each first-derivative symbol entry is an L∞ Fourier multiplier.

noncomputable def CKN.regularizedDerivativeEntryApply (δ : ℝ) (k j : Fin 3) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Applying a bounded first-derivative symbol to a scalar frequency component.

Equations

• CKN.regularizedDerivativeEntryApply δ k j f = CKN.fourierMultiplyScalarL2 (CKN.regularizedDerivativeEntry δ k j) ⋯ f

noncomputable def CKN.regularizedPotentialEntryApply (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) (f : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

Applying a regularized potential coefficient to one scalar frequency component.

Equations

• CKN.regularizedPotentialEntryApply δ hδ i f = CKN.fourierMultiplyScalarL2 (CKN.regularizedPotentialEntry δ i) ⋯ f

noncomputable def CKN.regularizedPotentialFourierComponent (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) (f : Fin 3 → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The three component formulas for the regularized Fourier vector potential.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.regularizedPotentialL2Component (δ : ℝ) (hδ : 0 < δ) (i : Fin 3) (f : Fin 3 → ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℂ 2 MeasureTheory.volume)

The spatial L² regularized vector potential, obtained by inverse Fourier transformation of its three component multipliers.

Equations

• CKN.regularizedPotentialL2Component δ hδ i f = FourierTransformInv.fourierInv (CKN.regularizedPotentialFourierComponent δ hδ i f)