Smooth

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Heat.summable_gauss_int {c : ℝ} (hc : 0 < c) : Summable fun (n : ℤ) => Real.exp (-c * ↑n ^ 2)

theorem AVenhance.Infra.Heat.summable_gauss_frequency {c : ℝ} (hc : 0 < c) : Summable fun (k : Frequency) => Real.exp (-c * frequencySq k)

theorem AVenhance.Infra.Heat.gaussianWeight_memLp (c : ℝ) (hc : 0 < c) : Memℓp (fun (k : Frequency) => ↑(Real.exp (-c * frequencySq k))) 2

@[instance_reducible]

noncomputable def avInfraHeatSmoothMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraHeatSmoothMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraHeatSmoothIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Heat.heatFourierCoeff_summable {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) : Summable fun (k : Frequency) => ‖UnitAddTorus.mFourierCoeff (↑↑(heatTorusL2 s ⋯ f)) k‖

noncomputable def AVenhance.Infra.Heat.heatTorusContinuous {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) : C(UnitAddTorus (Fin 2), ℂ)

Continuous torus representative of the positive-time heat evolution.

Equations

• AVenhance.Infra.Heat.heatTorusContinuous hs f = ∑' (k : AVenhance.Infra.Heat.Frequency), UnitAddTorus.mFourierCoeff (↑↑(AVenhance.Infra.Heat.heatTorusL2 s ⋯ f)) k • UnitAddTorus.mFourier k

theorem AVenhance.Infra.Heat.heatTorusContinuous_toLp {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) : (ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (heatTorusContinuous hs f) = heatTorusL2 s ⋯ f