Classical Derivative

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[instance_reducible]

noncomputable def avInfraHeatClassicalDerivativeMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraHeatClassicalDerivativeMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraHeatClassicalDerivativeIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Heat.degree_eq_zero_one (α : Fin 2 → ℕ) : multiIndexDegree α = α 0 + α 1

theorem AVenhance.Infra.Heat.heatDerivativeFourierCoeff_summable {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : Summable fun (k : Frequency) => ‖UnitAddTorus.mFourierCoeff (↑↑(heatDerivativeTorusL2 hs f α)) k‖

The Fourier coefficients of a heat-evolved multi-index derivative are absolutely summable. The Gaussian absorbs the polynomial frequency factor.

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

Continuous Fourier series representative of a classical heat derivative.

Equations

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

theorem AVenhance.Infra.Heat.heatDerivativeTorusContinuous_toLp {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : (ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (heatDerivativeTorusContinuous hs f α) = heatDerivativeTorusL2 hs f α

theorem AVenhance.Infra.Heat.heatDerivativeTorusContinuous_apply_toUnitTorus {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) (x : Homogenization.Vec 2) : (heatDerivativeTorusContinuous hs f α) (Torus.toUnitTorus 2 x) = ∑' (k : Frequency), UnitAddTorus.mFourierCoeff (↑↑f) k * heatDerivativeMultiplier s α k * Torus.torusCharacter (-k) x

theorem AVenhance.Infra.Heat.norm_heatTorusSmoothLift_multiIndexDerivative_le {s : ℝ} (hs : 0 < s) (f : ↥(Torus.TorusL2 2)) (α : Fin 2 → ℕ) : ‖(ContinuousMap.toLp 2 MeasureTheory.volume ℂ) (heatDerivativeTorusContinuous hs f α)‖ ≤ ↑(multiIndexDegree α).factorial * (1 / √s) ^ multiIndexDegree α * ‖f‖

The classical periodic derivative obeys the explicit analytic multiplier bound in torus L², with universal constant one.