The heat approximant does not increase the H¹ seminorm

For g = realHeatApprox hf hs (real part of the heat Fourier series of the datum), the gradient energy is bounded by that of the datum: pointwise |∇ Re H| ≤ |∇ H|, Parseval for the smooth periodic H, the Fourier multiplier e^{-4π² s |k|²} ≤ 1, and Parseval for the datum's weak gradient.

@[instance_reducible]

noncomputable def heatGradMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem heatGradIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem heatGradProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.FullTheorem.Uniform.HeatGradient.heatMult_nonneg (s : ℝ) (k : Heat.Frequency) : 0 ≤ Heat.heatMultiplier s k

theorem AVenhance.Infra.FullTheorem.Uniform.HeatGradient.heatMult_le_one {s : ℝ} (hs : 0 ≤ s) (k : Heat.Frequency) : Heat.heatMultiplier s k ≤ 1

theorem AVenhance.Infra.FullTheorem.Uniform.fourierEnergy_heatTorusL2_le {s : ℝ} (hs : 0 ≤ s) (u : ↥(Torus.TorusL2 2)) (hu : Heat.HasFiniteFourierEnergy u) : Heat.HasFiniteFourierEnergy (Heat.heatTorusL2 s hs u) ∧ Heat.fourierEnergy (Heat.heatTorusL2 s hs u) ≤ Heat.fourierEnergy u

The heat flow does not increase the Fourier Dirichlet energy.

theorem AVenhance.Infra.FullTheorem.Uniform.HeatGradient.heatLift_periodicToTorusL2 {s : ℝ} (hs : 0 < s) (u : ↥(Torus.TorusL2 2)) (hc : Continuous (Heat.heatTorusSmoothLift hs u)) : Torus.periodicToTorusL2 (Heat.heatTorusSmoothLift hs u) hc = Heat.heatTorusL2 s ⋯ u

The classical complex heat series is the periodic lift of the continuous heat evolution.

theorem AVenhance.Infra.FullTheorem.Uniform.HeatGradient.heatLift_periodic {s : ℝ} (hs : 0 < s) (u : ↥(Torus.TorusL2 2)) : Torus.IsZdPeriodic (Heat.heatTorusSmoothLift hs u)

theorem AVenhance.Infra.FullTheorem.Uniform.HeatGradient.spaceGrad_re_apply {H : Homogenization.Vec 2 → ℂ} (hH : ContDiff ℝ 1 H) (i : Fin 2) (x : Homogenization.Vec 2) : spaceGrad (fun (y : Homogenization.Vec 2) => (H y).re) x i = (Torus.coordDeriv i H x).re

The real part of a C¹ function has coordinate derivatives bounded by the complex ones.

theorem AVenhance.Infra.FullTheorem.Uniform.realHeatApprox_gradNormSq_le {f : Homogenization.Vec 2 → ℝ} {Df : Homogenization.Vec 2 → Homogenization.Vec 2} (hf : IsPeriodicH1With f Df) {s : ℝ} (hs : 0 < s) : gradNormSq (spaceGrad (Section5.realHeatApprox hf hs)) ≤ gradNormSq Df

The heat approximant has gradient energy at most that of the datum.