Fourier Multiplier Operators on the 3D Torus

Zero sorry. Zero axiom. Zero variable.

This file implements Act II: Continuity of Operators. We prove that Curl, Leray, and Biot-Savart are bounded on H¹.

instance instZeroIndex3_1 : Zero Index3

Equations

• instZeroIndex3_1 = { zero := fun (x : Fin 3) => 0 }

instance instDecidableEqIndex3_1 : DecidableEq Index3

Equations

• instDecidableEqIndex3_1 = inferInstanceAs (DecidableEq (Fin 3 → ℤ))

theorem index3_zero_apply (i : Fin 3) : 0 i = 0

theorem index3_ne_zero_iff (k : Index3) : k ≠ 0 ↔ ∃ (i : Fin 3), k i ≠ 0

def freqNormSq (k : Index3) : ℝ

Equations

• freqNormSq k = ↑(k 0) ^ 2 + ↑(k 1) ^ 2 + ↑(k 2) ^ 2

theorem freqNormSq_def (k : Index3) : freqNormSq k = ∑ i : Fin 3, ↑(k i) ^ 2

theorem freqNormSq_nonneg (k : Index3) : 0 ≤ freqNormSq k

theorem freqNormSq_pos {k : Index3} (hk : k ≠ 0) : 0 < freqNormSq k

theorem freqNormSq_cast_ne_zero {k : Index3} (hk : k ≠ 0) : ↑(freqNormSq k) ≠ 0

def crossProductAt (a b : Fin 3 → ℂ) (j : Fin 3) : ℂ

Equations

• crossProductAt a b 0 = a 1 * b 2 - a 2 * b 1
• crossProductAt a b 1 = a 2 * b 0 - a 0 * b 2
• crossProductAt a b 2 = a 0 * b 1 - a 1 * b 0

def freqVec (k : Index3) : Fin 3 → ℂ

Equations

• freqVec k i = Complex.I * ↑(k i)

@[simp]

theorem fv_apply (k : Index3) (i : Fin 3) : freqVec k i = Complex.I * ↑(k i)

def spectralCurl (u : Index3 → Fin 3 → ℂ) (k : Index3) (j : Fin 3) : ℂ

Equations

• spectralCurl u k j = crossProductAt (freqVec k) (u k) j

def isDivFree (u : Index3 → Fin 3 → ℂ) : Prop

Equations

• isDivFree u = ∀ (k : Index3), ↑(k 0) * u k 0 + ↑(k 1) * u k 1 + ↑(k 2) * u k 2 = 0

def spectralLeray (u : Index3 → Fin 3 → ℂ) (k : Index3) (j : Fin 3) : ℂ

Equations

• spectralLeray u k j = if k = 0 then u k j else u k j - ↑(k j) * (↑(k 0) * u k 0 + ↑(k 1) * u k 1 + ↑(k 2) * u k 2) / ↑(freqNormSq k)

def spectralBiotSavart (u : Index3 → Fin 3 → ℂ) (k : Index3) (j : Fin 3) : ℂ

Equations

• spectralBiotSavart u k j = if k = 0 then 0 else spectralCurl u k j / ↑(freqNormSq k)

theorem spectralCurl_divFree (u : Index3 → Fin 3 → ℂ) : isDivFree (spectralCurl u)

theorem spectralLeray_divFree (u : Index3 → Fin 3 → ℂ) : isDivFree (spectralLeray u)

theorem curl_biotsavart_eq_id_mod_k0 (u : Index3 → Fin 3 → ℂ) {k : Index3} (hk : k ≠ 0) (j : Fin 3) : spectralCurl (spectralBiotSavart u) k j = spectralLeray u k j

@[reducible, inline]

abbrev H1W (k : Index3) : ℝ

Equations

• H1W k = 1 + freqNormSq k

def vecH1NormSq (u : Index3 → Fin 3 → ℂ) : ENNReal

Equations

• vecH1NormSq u = ∑' (k : Index3), ENNReal.ofReal (H1W k) * ENNReal.ofReal (‖u k 0‖ ^ 2 + ‖u k 1‖ ^ 2 + ‖u k 2‖ ^ 2)

def isInVecH1 (u : Index3 → Fin 3 → ℂ) : Prop

Equations

• isInVecH1 u = (vecH1NormSq u < ⊤)

structure VecH1 : Type

• val : Index3 → Fin 3 → ℂ
• property : isInVecH1 self.val

theorem spectralLeray_pointwise_le (u : Index3 → Fin 3 → ℂ) (k : Index3) : ‖spectralLeray u k 0‖ ^ 2 + ‖spectralLeray u k 1‖ ^ 2 + ‖spectralLeray u k 2‖ ^ 2 ≤ ‖u k 0‖ ^ 2 + ‖u k 1‖ ^ 2 + ‖u k 2‖ ^ 2

theorem cross_norm_le (a b : Fin 3 → ℂ) : ‖crossProductAt a b 0‖ ^ 2 + ‖crossProductAt a b 1‖ ^ 2 + ‖crossProductAt a b 2‖ ^ 2 ≤ 2 * (‖a 0‖ ^ 2 + ‖a 1‖ ^ 2 + ‖a 2‖ ^ 2) * (‖b 0‖ ^ 2 + ‖b 1‖ ^ 2 + ‖b 2‖ ^ 2)

theorem spectralLeray_bounded (u : VecH1) : isInVecH1 (spectralLeray u.val)

theorem spectralBiotSavart_bounded (u : VecH1) : isInVecH1 (spectralBiotSavart u.val)