Smooth Classical

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.Infra.Heat.frequencyPhaseCLM (k : Frequency) : Homogenization.Vec 2 →L[ℝ] ℝ

The real linear phase associated with an integer frequency.

Equations

• AVenhance.Infra.Heat.frequencyPhaseCLM k = ∑ i : Fin 2, ↑(k i) • ContinuousLinearMap.proj i

@[simp]

theorem AVenhance.Infra.Heat.frequencyPhaseCLM_apply (k : Frequency) (x : Homogenization.Vec 2) : (frequencyPhaseCLM k) x = ∑ i : Fin 2, ↑(k i) * x i

theorem AVenhance.Infra.Heat.SmoothClassical.norm_proj_le_one (i : Fin 2) : ‖ContinuousLinearMap.proj i‖ ≤ 1

theorem AVenhance.Infra.Heat.norm_frequencyPhaseCLM_le (k : Frequency) : ‖frequencyPhaseCLM k‖ ≤ ∑ i : Fin 2, |↑(k i)|

theorem AVenhance.Infra.Heat.SmoothClassical.torusCharacter_neg_frequencyPhase (k : Frequency) : Torus.torusCharacter (-k) = fun (x : Homogenization.Vec 2) => ↑(Real.fourierChar ((frequencyPhaseCLM k) x))

theorem AVenhance.Infra.Heat.SmoothClassical.iteratedDeriv_fourierChar (n : ℕ) : (iteratedDeriv n fun (x : ℝ) => ↑(Real.fourierChar x)) = fun (x : ℝ) => (2 * ↑Real.pi * Complex.I) ^ n * ↑(Real.fourierChar x)

theorem AVenhance.Infra.Heat.SmoothClassical.norm_iteratedFDeriv_fourierChar (n : ℕ) (x : ℝ) : ‖iteratedFDeriv ℝ n (fun (x : ℝ) => ↑(Real.fourierChar x)) x‖ ≤ (2 * Real.pi) ^ n

theorem AVenhance.Infra.Heat.SmoothClassical.contDiff_fourierChar : ContDiff ℝ ⊤ fun (x : ℝ) => ↑(Real.fourierChar x)

theorem AVenhance.Infra.Heat.norm_iteratedFDeriv_torusCharacter_le (k : Frequency) (n : ℕ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (Torus.torusCharacter (-k)) x‖ ≤ (2 * Real.pi) ^ n * (∑ i : Fin 2, |↑(k i)|) ^ n

Uniform Fréchet derivative bound for a torus character in terms of its frequency.

theorem AVenhance.Infra.Heat.iteratedFDeriv_torusCharacter_apply (k : Frequency) (n : ℕ) (x : Homogenization.Vec 2) (v : Fin n → Homogenization.Vec 2) : (iteratedFDeriv ℝ n (Torus.torusCharacter (-k)) x) v = (2 * ↑Real.pi * Complex.I) ^ n * Torus.torusCharacter (-k) x * ↑(∏ j : Fin n, (frequencyPhaseCLM k) (v j))

Exact all-orders derivative multiplier for one torus character, evaluated on arbitrary directions.

theorem AVenhance.Infra.Heat.SmoothClassical.frequencyL1_le (k : Frequency) : ∑ i : Fin 2, |↑(k i)| ≤ 2 * √(frequencySq k)

theorem AVenhance.Infra.Heat.SmoothClassical.character_derivative_radial_bound (k : Frequency) (n : ℕ) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (Torus.torusCharacter (-k)) x‖ ≤ 2 ^ n * (2 * Real.pi * √(frequencySq k)) ^ n

noncomputable def AVenhance.Infra.Heat.SmoothClassical.heatSeriesMode {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (k : Frequency) : Homogenization.Vec 2 → ℂ

One Fourier mode of the positive-time heat evolution, lifted to Euclidean space.

Equations

• AVenhance.Infra.Heat.SmoothClassical.heatSeriesMode hs f k x = UnitAddTorus.mFourierCoeff (↑↑(AVenhance.Infra.Heat.heatTorusL2 s ⋯ f)) k * AVenhance.Infra.Torus.torusCharacter (-k) x

theorem AVenhance.Infra.Heat.SmoothClassical.heatSeriesMode_contDiff {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (k : Frequency) : ContDiff ℝ ⊤ (heatSeriesMode hs f k)

theorem AVenhance.Infra.Heat.SmoothClassical.heatSeriesMode_iteratedFDeriv_bound {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (n : ℕ) (k : Frequency) (x : Homogenization.Vec 2) : ‖iteratedFDeriv ℝ n (heatSeriesMode hs f k) x‖ ≤ 2 ^ n * ↑n.factorial * (1 / √(s / 2)) ^ n * (‖↑(UnitAddTorus.mFourierBasis.repr f) k‖ * Real.exp (-(2 * Real.pi ^ 2 * s) * frequencySq k))

theorem AVenhance.Infra.Heat.heatSeriesMode_iteratedFDeriv_apply {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (n : ℕ) (k : Frequency) (x : Homogenization.Vec 2) (v : Fin n → Homogenization.Vec 2) : (iteratedFDeriv ℝ n (SmoothClassical.heatSeriesMode hs f k) x) v = UnitAddTorus.mFourierCoeff (↑↑(heatTorusL2 s ⋯ f)) k * (2 * ↑Real.pi * Complex.I) ^ n * Torus.torusCharacter (-k) x * ↑(∏ j : Fin n, (frequencyPhaseCLM k) (v j))

Exact all-orders Fourier multiplier for one mode of the classical heat series.

noncomputable def AVenhance.Infra.Heat.heatTorusSmoothLift {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) : Homogenization.Vec 2 → ℂ

The classical Euclidean Fourier series representative of the heat evolution.

Equations

• AVenhance.Infra.Heat.heatTorusSmoothLift hs f x = ∑' (k : AVenhance.Infra.Heat.Frequency), AVenhance.Infra.Heat.SmoothClassical.heatSeriesMode hs f k x

theorem AVenhance.Infra.Heat.heatTorusSmoothLift_contDiff {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) : ContDiff ℝ (↑⊤) (heatTorusSmoothLift hs f)

theorem AVenhance.Infra.Heat.heatTorusSmoothLift_eq_heatTorusContinuous {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (x : Homogenization.Vec 2) : heatTorusSmoothLift hs f x = (heatTorusContinuous hs f) (Torus.toUnitTorus 2 x)

theorem AVenhance.Infra.Heat.heatTorusSmoothLift_iteratedFDeriv_apply {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (n : ℕ) (x : Homogenization.Vec 2) (v : Fin n → Homogenization.Vec 2) : (iteratedFDeriv ℝ n (heatTorusSmoothLift hs f) x) v = ∑' (k : Frequency), UnitAddTorus.mFourierCoeff (↑↑(heatTorusL2 s ⋯ f)) k * (2 * ↑Real.pi * Complex.I) ^ n * Torus.torusCharacter (-k) x * ↑(∏ j : Fin n, (frequencyPhaseCLM k) (v j))

The classical n-th Fréchet derivative is obtained by differentiating the heat Fourier series term by term. Its multiplier on a direction tuple is the product of the corresponding linear frequency phases.