Fourier definition of the periodic heat semigroup on the two dimensional torus.

@[instance_reducible]

noncomputable def avInfraHeatSemigroupMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

Use normalized Haar measure on the unit circle for periodic integrals.

Equations

• avInfraHeatSemigroupMeasureSpace1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem avInfraHeatSemigroupMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraHeatSemigroupIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

@[reducible, inline]

abbrev AVenhance.Infra.Heat.Frequency : Type

Two-dimensional integer frequencies for the periodic heat equation.

Equations

• AVenhance.Infra.Heat.Frequency = (Fin 2 → ℤ)

def AVenhance.Infra.Heat.frequencySq (k : Frequency) : ℝ

The squared Euclidean length of an integer torus frequency.

Equations

• AVenhance.Infra.Heat.frequencySq k = ∑ i : Fin 2, ↑(k i) ^ 2

noncomputable def AVenhance.Infra.Heat.heatMultiplier (s : ℝ) (k : Frequency) : ℝ

The Fourier multiplier of the heat flow at time s.

Equations

• AVenhance.Infra.Heat.heatMultiplier s k = Real.exp (-(4 * Real.pi ^ 2 * s * AVenhance.Infra.Heat.frequencySq k))

theorem AVenhance.Infra.Heat.Semigroup.frequencySq_nonneg (k : Frequency) : 0 ≤ frequencySq k

theorem AVenhance.Infra.Heat.Semigroup.heatMultiplier_nonneg (s : ℝ) (k : Frequency) : 0 ≤ heatMultiplier s k

theorem AVenhance.Infra.Heat.Semigroup.heatMultiplier_le_one {s : ℝ} (hs : 0 ≤ s) (k : Frequency) : heatMultiplier s k ≤ 1

theorem AVenhance.Infra.Heat.Semigroup.heatMultiplier_add (s t : ℝ) (k : Frequency) : heatMultiplier (s + t) k = heatMultiplier s k * heatMultiplier t k

noncomputable def AVenhance.Infra.Heat.Semigroup.heatSequence (s : ℝ) (a : Frequency → ℂ) : Frequency → ℂ

Apply the heat multiplier to each Fourier coefficient.

Equations

• AVenhance.Infra.Heat.Semigroup.heatSequence s a k = ↑(AVenhance.Infra.Heat.heatMultiplier s k) * a k

theorem AVenhance.Infra.Heat.Semigroup.memℓp_heatSequence {s : ℝ} (hs : 0 ≤ s) (a : Frequency → ℂ) (ha : Memℓp a 2) : Memℓp (heatSequence s a) 2

noncomputable def AVenhance.Infra.Heat.heatFourierSequence (s : ℝ) (hs : 0 ≤ s) (f : ↥(Torus.TorusL2 2)) : ↥(lp (fun (x : Frequency) => ℂ) 2)

Fourier coefficients after heat evolution, regarded as an ℓ² sequence.

Equations

• AVenhance.Infra.Heat.heatFourierSequence s hs f = ⟨AVenhance.Infra.Heat.Semigroup.heatSequence s fun (k : AVenhance.Infra.Heat.Frequency) => ↑(UnitAddTorus.mFourierBasis.repr f) k, ⋯⟩

noncomputable def AVenhance.Infra.Heat.heatTorusL2 (s : ℝ) (hs : 0 ≤ s) (f : ↥(Torus.TorusL2 2)) : ↥(Torus.TorusL2 2)

The torus heat semigroup, defined by the multiplier exp(-4π²s|k|²).

Equations

• AVenhance.Infra.Heat.heatTorusL2 s hs f = UnitAddTorus.mFourierBasis.repr.symm (AVenhance.Infra.Heat.heatFourierSequence s hs f)

theorem AVenhance.Infra.Heat.mFourierCoeff_heatTorusL2 {s : ℝ} (hs : 0 ≤ s) (f : ↥(Torus.TorusL2 2)) (k : Frequency) : UnitAddTorus.mFourierCoeff (↑↑(heatTorusL2 s hs f)) k = ↑(heatMultiplier s k) * UnitAddTorus.mFourierCoeff (↑↑f) k

The multiplier formula for every Fourier coefficient of the heat flow.

theorem AVenhance.Infra.Heat.integral_heatTorusL2 {s : ℝ} (hs : 0 ≤ s) (f : ↥(Torus.TorusL2 2)) : ∫ (x : UnitAddTorus (Fin 2)), ↑↑(heatTorusL2 s hs f) x = ∫ (x : UnitAddTorus (Fin 2)), ↑↑f x

Heat flow preserves the integral, since its zero Fourier mode is unchanged.