Explicit Gaussian bounds for the Fourier heat multiplier.

def AVenhance.Infra.Heat.multiIndexDegree (α : Fin 2 → ℕ) : ℕ

Total order of a coordinate multi-index in two dimensions.

Equations

• AVenhance.Infra.Heat.multiIndexDegree α = ∑ i : Fin 2, α i

noncomputable def AVenhance.Infra.Heat.multiIndexFourierFactor (α : Fin 2 → ℕ) (k : Frequency) : ℂ

The Fourier multiplier for the coordinate derivative with multi-index α.

Equations

• AVenhance.Infra.Heat.multiIndexFourierFactor α k = ∏ i : Fin 2, (2 * ↑Real.pi * Complex.I * ↑(k i)) ^ α i

noncomputable def AVenhance.Infra.Heat.heatDerivativeMultiplier (s : ℝ) (α : Fin 2 → ℕ) (k : Frequency) : ℂ

Fourier multiplier of the corresponding derivative after heat evolution.

Equations

• AVenhance.Infra.Heat.heatDerivativeMultiplier s α k = ↑(AVenhance.Infra.Heat.heatMultiplier s k) * AVenhance.Infra.Heat.multiIndexFourierFactor α k

theorem AVenhance.Infra.Heat.Analytic.abs_frequencyCoord_le_sqrt (k : Frequency) (i : Fin 2) : |↑(k i)| ≤ √(frequencySq k)

The coordinate frequencies are controlled by the Euclidean frequency length.

theorem AVenhance.Infra.Heat.Analytic.multiIndexFourierFactor_norm_le (α : Fin 2 → ℕ) (k : Frequency) : ‖multiIndexFourierFactor α k‖ ≤ (2 * Real.pi * √(frequencySq k)) ^ multiIndexDegree α

The multi-index Fourier factor is bounded by the radial frequency power.

theorem AVenhance.Infra.Heat.radialHeatMultiplier_bound {s : ℝ} (hs : 0 < s) (n : ℕ) (k : Frequency) : (2 * Real.pi * √(frequencySq k)) ^ n * heatMultiplier s k ≤ ↑n.factorial * (1 / √s) ^ n

The Gaussian multiplier absorbs a radial frequency power with factorial loss one. This gives the universal analyticity constant C = 1.

theorem AVenhance.Infra.Heat.heatDerivativeMultiplier_norm_le {s : ℝ} (hs : 0 < s) (α : Fin 2 → ℕ) (k : Frequency) : ‖heatDerivativeMultiplier s α k‖ ≤ ↑(multiIndexDegree α).factorial * (1 / √s) ^ multiIndexDegree α

For every coordinate multi-index, the heat multiplier and derivative factor obey the factorial analyticity bound with explicit universal constant 1.

noncomputable def AVenhance.Infra.Heat.heatDerivativeSequence {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : ↥(lp (fun (x : Frequency) => ℂ) 2)

Fourier sequence of the order-α spectral derivative of the heat flow.

Equations

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

noncomputable def AVenhance.Infra.Heat.heatDerivativeTorusL2 {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : ↥(Torus.TorusL2 2)

The L² spectral derivative of heat flow, defined by the coordinate Fourier multiplier.

Equations

• AVenhance.Infra.Heat.heatDerivativeTorusL2 hs f α = UnitAddTorus.mFourierBasis.repr.symm (AVenhance.Infra.Heat.heatDerivativeSequence hs f α)

theorem AVenhance.Infra.Heat.mFourierCoeff_heatDerivativeTorusL2 {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) (k : Frequency) : UnitAddTorus.mFourierCoeff (↑↑(heatDerivativeTorusL2 hs f α)) k = heatDerivativeMultiplier s α k * UnitAddTorus.mFourierCoeff (↑↑f) k

Fourier coefficients of the spectral derivative are the expected multi-index multiplier.

theorem AVenhance.Infra.Heat.norm_heatDerivativeTorusL2_le {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : ‖heatDerivativeTorusL2 hs f α‖ ≤ ↑(multiIndexDegree α).factorial * (1 / √s) ^ multiIndexDegree α * ‖f‖

The L² norm of every spectral derivative obeys the factorial analyticity estimate with explicit constant C = 1.