def SobolevSpace.multiIndexOrder (n : ℕ) (α : Fin n → ℕ) : ℕ

The order |α| = ∑ α i of a multi-index α : Fin n → ℕ.

noncomputable def SobolevSpace.iteratedPartialDerivDistrib (n : ℕ) (i : Fin n) (k : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

Iterated distributional partial derivative in the i-th coordinate, applied k times.

noncomputable def SobolevSpace.iteratedDistribDeriv (n : ℕ) (α : Fin n → ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ

The multi-index distributional derivative D^α u, applied coordinate by coordinate.

def SobolevSpace.AllDerivMemL2 (n m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : Prop

Characterization of H^m (for integer m ≥ 0): every multi-index derivative D^α u with |α| ≤ m lies in L².

theorem SobolevSpace.iteratedPartialDerivDistrib_eq {n : ℕ} (i : Fin n) (k : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : iteratedPartialDerivDistrib n i k u = FourierInversion.iterDistribDerivCoord i k u

The iterated coordinate distributional derivative agrees with FourierInversion.iterDistribDerivCoord.

theorem SobolevSpace.iteratedDistribDeriv_eq {n : ℕ} (α : Fin n → ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : iteratedDistribDeriv n α u = FourierInversion.iterDistribDeriv α u

The multi-index distributional derivative agrees with FourierInversion.iterDistribDeriv.

theorem SobolevSpace.abs_inner_single_le_japaneseBracket {n : ℕ} (j : Fin n) (ξ : EuclideanSpace ℝ (Fin n)) : |inner ℝ ξ (EuclideanSpace.single j 1)| ≤ TestFunctions.japaneseBracket n ξ

The absolute value of ⟨ξ, e_j⟩ is bounded by ⟨ξ⟩ = sqrt(1 + ‖ξ‖²).

theorem SobolevSpace.norm_two_pi_I : ‖2 * ↑Real.pi * Complex.I‖ = 2 * Real.pi

The complex norm of 2π i equals 2π.

theorem SobolevSpace.memHs_distribDeriv {n : ℕ} {s : ℝ} (j : Fin n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : MemHs n s u) : MemHs n (s - 1) ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u)

Differentiation lowers Sobolev regularity by one: if u ∈ H^s, then ∂_j u ∈ H^{s-1}.

theorem SobolevSpace.memHs_iteratedPartialDeriv {n : ℕ} {s : ℝ} (j : Fin n) (k : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : MemHs n s u) : MemHs n (s - ↑k) (iteratedPartialDerivDistrib n j k u)

Iterated coordinate differentiation lowers Sobolev regularity by k: H^s → H^{s-k} for ∂_j^k.

theorem SobolevSpace.memHs_foldr_iteratedPartialDeriv {n : ℕ} {s : ℝ} (l : List (Fin n)) (α : Fin n → ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : MemHs n s u) : MemHs n (s - ↑(List.map (fun (j : Fin n) => α j) l).sum) (List.foldr (fun (j : Fin n) (acc : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) => iteratedPartialDerivDistrib n j (α j) acc) u l)

Sobolev regularity loss for a fold over a list of coordinates: lowering by the sum of orders along the list.

theorem SobolevSpace.memHs_iteratedDistribDeriv {n : ℕ} {s : ℝ} (α : Fin n → ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : MemHs n s u) : MemHs n (s - ↑(multiIndexOrder n α)) (iteratedDistribDeriv n α u)

Melrose Proposition 10.2: D^α : H^s → H^{s - |α|}.

theorem SobolevSpace.iteratedDistribDeriv_zero {n : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : iteratedDistribDeriv n (fun (x : Fin n) => 0) u = u

The zero multi-index derivative D^0 is the identity.

theorem SobolevSpace.allDerivMemL2_of_succ {n m : ℕ} (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : AllDerivMemL2 n (m + 1) u) : AllDerivMemL2 n m u

Demotion: if all derivatives up to order m + 1 lie in L^2, then so do all derivatives up to order m.

theorem SobolevSpace.distribDeriv_comm {n : ℕ} (v w : EuclideanSpace ℝ (Fin n)) (T : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : (TemperedDistributions.distribDerivCLM v) ((TemperedDistributions.distribDerivCLM w) T) = (TemperedDistributions.distribDerivCLM w) ((TemperedDistributions.distribDerivCLM v) T)

Distributional partial derivatives in different directions commute.

theorem SobolevSpace.iteratedPartialDerivDistrib_distribDeriv_comm {n : ℕ} (i : Fin n) (k : ℕ) (j : Fin n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : iteratedPartialDerivDistrib n i k ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u) = (TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) (iteratedPartialDerivDistrib n i k u)

The iterated partial derivative in coordinate i commutes with ∂_j.

theorem SobolevSpace.foldr_iterPartialDeriv_distribDeriv_comm {n : ℕ} (l : List (Fin n)) (α : Fin n → ℕ) (j : Fin n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : List.foldr (fun (i : Fin n) (acc : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) => iteratedPartialDerivDistrib n i (α i) acc) ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u) l = (TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) (List.foldr (fun (i : Fin n) (acc : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) => iteratedPartialDerivDistrib n i (α i) acc) u l)

A foldr of iterated partial derivatives commutes with an additional ∂_j.

theorem SobolevSpace.foldr_update_eq {n : ℕ} (l : List (Fin n)) (α : Fin n → ℕ) (j : Fin n) (hj : j ∉ l) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : List.foldr (fun (k : Fin n) (acc : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) => iteratedPartialDerivDistrib n k (Function.update α j (α j + 1) k) acc) u l = List.foldr (fun (k : Fin n) (acc : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) => iteratedPartialDerivDistrib n k (α k) acc) u l

If j does not appear in l, updating α at j does not affect the fold over l.

theorem SobolevSpace.iteratedDistribDeriv_distribDeriv {n : ℕ} (α : Fin n → ℕ) (j : Fin n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : iteratedDistribDeriv n α ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u) = iteratedDistribDeriv n (Function.update α j (α j + 1)) u

Applying D^α after one further ∂_j equals applying D^{α with α_j ↦ α_j + 1}.

theorem SobolevSpace.multiIndexOrder_update {n : ℕ} (α : Fin n → ℕ) (j : Fin n) : multiIndexOrder n (Function.update α j (α j + 1)) = multiIndexOrder n α + 1

Incrementing α j increases the multi-index order by exactly one.

theorem SobolevSpace.allDerivMemL2_distribDeriv {n m : ℕ} (j : Fin n) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : AllDerivMemL2 n (m + 1) u) : AllDerivMemL2 n m ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u)

If all derivatives of order ≤ m + 1 of u lie in L², then ∂_j u has all derivatives of order ≤ m in L².

theorem sobolevWeight_mul_memLp {n : ℕ} (m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (g₀ : EuclideanSpace ℝ (Fin n) → ℂ) (hg₀_mem : MeasureTheory.MemLp g₀ 2 MeasureTheory.volume) (hg₀_eq : ∀ (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ), (FourierTransform.fourier u) φ = ∫ (ξ : EuclideanSpace ℝ (Fin n)), (↑(SobolevSpace.sobolevWeight n (↑m) ξ))⁻¹ * g₀ ξ * φ ξ) (hj : ∀ (j : Fin n), SobolevSpace.MemHs n (↑m) ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u)) : MeasureTheory.MemLp (fun (ξ : EuclideanSpace ℝ (Fin n)) => ↑(SobolevSpace.sobolevWeight n 1 ξ) * g₀ ξ) 2 MeasureTheory.volume

Multiplying the Fourier-side L² representative by the Sobolev weight ⟨·⟩ stays in L², given derivative regularity.

theorem SobolevSpace.memHs_succ_of_memHs_and_deriv {n : ℕ} (m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : MemHs n (↑m) u) (hj : ∀ (j : Fin n), MemHs n (↑m) ((TemperedDistributions.distribDerivCLM (EuclideanSpace.single j 1)) u)) : MemHs n (↑(m + 1)) u

Inductive step: if u ∈ H^m and every ∂_j u ∈ H^m, then u ∈ H^{m+1}.

theorem SobolevSpace.allDerivMemL2_imp_memHs {n : ℕ} (m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) (hu : AllDerivMemL2 n m u) : MemHs n (↑m) u

If all multi-index derivatives of u up to order m lie in L², then u ∈ H^m.

theorem SobolevSpace.sobolev_integer_iff_deriv_memL2 {n : ℕ} (m : ℕ) (u : TemperedDistribution (EuclideanSpace ℝ (Fin n)) ℂ) : MemHs n (↑m) u ↔ AllDerivMemL2 n m u

Melrose Lemma 9.4 (integer case): u ∈ H^m ↔ all D^α u with |α| ≤ m lie in L².