H² ⊂ L∞ on the 2-torus

For a smooth ℤ²-periodic function u : Vec 2 → ℝ we prove |u x| ≤ sobolevConst * (‖u‖₂ + ‖∂₀²u‖₂ + ‖∂₁²u‖₂), by expanding u in its (absolutely convergent) Fourier series and applying Cauchy–Schwarz against the weight sobolevWeight k = 1 + (2π)⁴(k₀⁴ + k₁⁴).

noncomputable def AVenhance.Infra.Section5.AnalyticBridge.sobolevWeight (k : Fin 2 → ℤ) : ℝ

The Fourier weight 1 + (2π)⁴ (k₀⁴ + k₁⁴) on ℤ².

Equations

• AVenhance.Infra.Section5.AnalyticBridge.sobolevWeight k = 1 + (2 * Real.pi) ^ 4 * (↑(k 0) ^ 4 + ↑(k 1) ^ 4)

theorem AVenhance.Infra.Section5.AnalyticBridge.sobolevWeight_pos (k : Fin 2 → ℤ) : 0 < sobolevWeight k

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.one_le_two_pi_pow_four : 1 ≤ (2 * Real.pi) ^ 4

1 ≤ (2π)⁴, in abstract-real form.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.prod_le_two_mul (a b : ℝ) : (1 + a ^ 2) * (1 + b ^ 2) ≤ 2 * (1 + (a ^ 4 + b ^ 4))

Product bound (1 + a²)(1 + b²) ≤ 2 (1 + a⁴ + b⁴).

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.prod_le_two_mul_sobolevWeight (k : Fin 2 → ℤ) : (1 + ↑(k 0) ^ 2) * (1 + ↑(k 1) ^ 2) ≤ 2 * sobolevWeight k

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.summable_one_div_one_add_sq : Summable fun (n : ℤ) => 1 / (1 + ↑n ^ 2)

One-dimensional summability of 1 / (1 + n²) over ℤ.

theorem AVenhance.Infra.Section5.AnalyticBridge.summable_inv_sobolevWeight : Summable fun (k : Fin 2 → ℤ) => (sobolevWeight k)⁻¹

The inverse Sobolev weight is summable over ℤ².

noncomputable def AVenhance.Infra.Section5.AnalyticBridge.sobolevConst : ℝ

The Sobolev constant (∑_{k ∈ ℤ²} (1 + (2π)⁴ (k₀⁴ + k₁⁴))⁻¹)^{1/2}.

Equations

• AVenhance.Infra.Section5.AnalyticBridge.sobolevConst = √(∑' (k : Fin 2 → ℤ), (AVenhance.Infra.Section5.AnalyticBridge.sobolevWeight k)⁻¹)

theorem AVenhance.Infra.Section5.AnalyticBridge.sobolevConst_pos : 0 < sobolevConst

Coordinate derivatives of smooth periodic real functions

noncomputable def AVenhance.Infra.Section5.AnalyticBridge.Sobolev.coordPartial (i : Fin 2) (u : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → ℝ

The real coordinate derivative ∂ᵢ u.

Equations

• AVenhance.Infra.Section5.AnalyticBridge.Sobolev.coordPartial i u y = (fderiv ℝ u y) (Homogenization.basisVec i)

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.contDiff_coordPartial {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin 2) : ContDiff ℝ (↑⊤) (coordPartial i u)

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.isZ2Periodic_coordPartial {u : Homogenization.Vec 2 → ℝ} (hp : IsZ2Periodic u) (i : Fin 2) : IsZ2Periodic (coordPartial i u)

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.coordPartial_coordPartial {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (i : Fin 2) (y : Homogenization.Vec 2) : coordPartial i (coordPartial i u) y = (iteratedFDeriv ℝ 2 u y) fun (x : Fin 2) => Homogenization.basisVec i

The second coordinate derivative as the iterated Fréchet derivative.

Parseval for u and its pure second derivatives

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.norm_sq_fourierMultiplier (m : ℤ) : ‖2 * ↑Real.pi * Complex.I * ↑m‖ ^ 2 = (2 * Real.pi) ^ 2 * ↑m ^ 2

The squared modulus of a Fourier multiplier 2πi m.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.norm_sq_multiplier_twice (m : ℤ) (z : ℂ) : ‖2 * ↑Real.pi * Complex.I * ↑m * (2 * ↑Real.pi * Complex.I * ↑m * z)‖ ^ 2 = (2 * Real.pi) ^ 4 * ↑m ^ 4 * ‖z‖ ^ 2

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.smoothFourierCoeff_second {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hp : IsZ2Periodic u) (i : Fin 2) (k : Fin 2 → ℤ) : Torus.smoothFourierCoeff (Torus.realToComplex (coordPartial i (coordPartial i u))) k = 2 * ↑Real.pi * Complex.I * ↑(k i) * (2 * ↑Real.pi * Complex.I * ↑(k i) * Torus.smoothFourierCoeff (Torus.realToComplex u) k)

Fourier coefficients of the second coordinate derivative.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.hasSum_sq_zeroth {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) : HasSum (fun (k : Fin 2 → ℤ) => ‖Torus.smoothFourierCoeff (Torus.realToComplex u) k‖ ^ 2) (l2NormSq u)

Parseval for u.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.hasSum_sq_second {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hp : IsZ2Periodic u) (i : Fin 2) : HasSum (fun (k : Fin 2 → ℤ) => (2 * Real.pi) ^ 4 * ↑(k i) ^ 4 * ‖Torus.smoothFourierCoeff (Torus.realToComplex u) k‖ ^ 2) (l2NormSq fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ 2 u y) fun (x : Fin 2) => Homogenization.basisVec i)

Parseval for the pure second derivative ∂ᵢ²u, weighted by (2π)⁴ kᵢ⁴.

Cauchy–Schwarz against the Sobolev weight

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.sum_norm_le_sobolevConst_mul {c : (Fin 2 → ℤ) → ℂ} {S : ℝ} (hsum : HasSum (fun (k : Fin 2 → ℤ) => sobolevWeight k * ‖c k‖ ^ 2) S) (s : Finset (Fin 2 → ℤ)) : ∑ k ∈ s, ‖c k‖ ≤ sobolevConst * √S

Finite Cauchy–Schwarz: weighted ℓ² control gives finite ℓ¹ control.

Pointwise Fourier expansion of a smooth periodic function

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.continuous_periodicToTorus {f : Homogenization.Vec 2 → ℂ} (hc : Continuous f) (hp : Torus.IsZdPeriodic f) : Continuous (Torus.periodicToTorus f)

A continuous periodic function descends to a continuous function on the torus.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.mFourierCoeff_periodicToTorus (f : Homogenization.Vec 2 → ℂ) (k : Fin 2 → ℤ) : UnitAddTorus.mFourierCoeff (Torus.periodicToTorus f) k = Torus.smoothFourierCoeff f k

The torus Fourier coefficient of the periodic transfer is smoothFourierCoeff.

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.norm_le_sobolevConst_mul_sqrt {f : Homogenization.Vec 2 → ℂ} (hc : Continuous f) (hp : Torus.IsZdPeriodic f) {S : ℝ} (hsum : HasSum (fun (k : Fin 2 → ℤ) => sobolevWeight k * ‖Torus.smoothFourierCoeff f k‖ ^ 2) S) (x : Homogenization.Vec 2) : ‖f x‖ ≤ sobolevConst * √S

Pointwise bound from weighted ℓ² control of the Fourier coefficients.

Main theorem

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.sqrt_add_add_le (A B C : ℝ) (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) : √(A + B + C) ≤ √A + √B + √C

theorem AVenhance.Infra.Section5.AnalyticBridge.Sobolev.l2NormSq_nonneg (f : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq f

theorem AVenhance.Infra.Section5.AnalyticBridge.abs_le_sobolevConst_mul {u : Homogenization.Vec 2 → ℝ} (hu : ContDiff ℝ (↑⊤) u) (hp : IsZ2Periodic u) (x : Homogenization.Vec 2) : |u x| ≤ sobolevConst * (√(l2NormSq u) + √(l2NormSq fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ 2 u y) fun (x : Fin 2) => Homogenization.basisVec 0) + √(l2NormSq fun (y : Homogenization.Vec 2) => (iteratedFDeriv ℝ 2 u y) fun (x : Fin 2) => Homogenization.basisVec 1))

H² ⊂ L∞ on 𝕋²: a smooth ℤ²-periodic function is bounded by its L² norm and the L² norms of its pure second derivatives.