Spectral energy identity and the quantitative heat-flow deficit estimate.

@[instance_reducible]

noncomputable def avInfraHeatEnergyMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraHeatEnergyMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraHeatEnergyIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Heat.norm_sq_eq_tsum_fourierCoeff (f : ↥(Torus.TorusL2 2)) : ‖f‖ ^ 2 = ∑' (k : Frequency), ‖UnitAddTorus.mFourierCoeff (↑↑f) k‖ ^ 2

The Fourier expression for the squared torus L² norm.

noncomputable def AVenhance.Infra.Heat.fourierEnergyTerm (f : ↥(Torus.TorusL2 2)) (k : Frequency) : ℝ

The spectral Dirichlet energy on the torus.

Equations

• AVenhance.Infra.Heat.fourierEnergyTerm f k = 4 * Real.pi ^ 2 * AVenhance.Infra.Heat.frequencySq k * ‖UnitAddTorus.mFourierCoeff (↑↑f) k‖ ^ 2

def AVenhance.Infra.Heat.HasFiniteFourierEnergy (f : ↥(Torus.TorusL2 2)) : Prop

Finite Fourier Dirichlet energy, stated as summability of its nonnegative terms.

Equations

• AVenhance.Infra.Heat.HasFiniteFourierEnergy f = Summable (AVenhance.Infra.Heat.fourierEnergyTerm f)

noncomputable def AVenhance.Infra.Heat.fourierEnergy (f : ↥(Torus.TorusL2 2)) : ℝ

The spectral Dirichlet energy associated with the Fourier coefficients.

Equations

• AVenhance.Infra.Heat.fourierEnergy f = ∑' (k : AVenhance.Infra.Heat.Frequency), AVenhance.Infra.Heat.fourierEnergyTerm f k

theorem AVenhance.Infra.Heat.Energy.fourierEnergyTerm_nonneg (f : ↥(Torus.TorusL2 2)) (k : Frequency) : 0 ≤ fourierEnergyTerm f k

theorem AVenhance.Infra.Heat.Energy.heatMultiplier_sq {s : ℝ} (k : Frequency) : heatMultiplier s k ^ 2 = Real.exp (-(8 * Real.pi ^ 2 * s * frequencySq k))

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

theorem AVenhance.Infra.Heat.normSq_sub_heatTorusL2_le {s : ℝ} (hs : 0 ≤ s) (f : ↥(Torus.TorusL2 2)) (hE : HasFiniteFourierEnergy f) : ‖f - heatTorusL2 s hs f‖ ^ 2 ≤ s * fourierEnergy f

The L² error between a function and its heat regularization is bounded by s times the spectral Dirichlet energy.

theorem AVenhance.Infra.Heat.Energy.frequencySq_ge_one_of_ne_zero (k : Frequency) (hk : k ≠ 0) : 1 ≤ frequencySq k

theorem AVenhance.Infra.Heat.meanZero_fourierPoincare {f : ↥(Torus.TorusL2 2)} (hmean : ∫ (x : UnitAddTorus (Fin 2)), ↑↑f x = 0) (hE : HasFiniteFourierEnergy f) : ‖f‖ ^ 2 ≤ (4 * Real.pi ^ 2)⁻¹ * fourierEnergy f

Mean-zero Poincaré inequality for arbitrary torus L² functions with finite spectral Dirichlet energy.

theorem AVenhance.Infra.Heat.Energy.normSq_fourierGradientMultiplier (m : ℤ) (z : ℂ) : ‖2 * ↑Real.pi * Complex.I * ↑m * z‖ ^ 2 = 4 * Real.pi ^ 2 * ↑m ^ 2 * ‖z‖ ^ 2

theorem AVenhance.Infra.Heat.Energy.smoothGradientFourierCoeff_eq_frequency {g : Homogenization.Vec 2 → ℂ} (hg : ContDiff ℝ 1 g) (hpg : Torus.IsZdPeriodic g) (k : Frequency) : ∑ i : Fin 2, ‖Torus.smoothFourierCoeff (Torus.coordDeriv i g) k‖ ^ 2 = 4 * Real.pi ^ 2 * frequencySq k * ‖Torus.smoothFourierCoeff g k‖ ^ 2

theorem AVenhance.Infra.Heat.Energy.periodicToTorusL2_fourierCoeff_eq_heat {g : Homogenization.Vec 2 → ℂ} (hg : Continuous g) (k : Frequency) : Torus.periodicL2FourierCoeff (Torus.periodicToTorusL2 g hg) k = Torus.smoothFourierCoeff g k

theorem AVenhance.Infra.Heat.hasFiniteFourierEnergy_periodicToTorusL2 {g : Homogenization.Vec 2 → ℂ} (hg : ContDiff ℝ 1 g) (hpg : Torus.IsZdPeriodic g) : HasFiniteFourierEnergy (Torus.periodicToTorusL2 g ⋯) ∧ fourierEnergy (Torus.periodicToTorusL2 g ⋯) = ∫ (x : Homogenization.Vec 2) in Torus.unitCell 2, ∑ i : Fin 2, ‖Torus.coordDeriv i g x‖ ^ 2

For a smooth periodic function, the spectral Dirichlet energy is exactly the cell integral of the squared gradient.

theorem AVenhance.Infra.Heat.hasFiniteFourierEnergy_realSmooth {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hpf : IsZ2Periodic f) : HasFiniteFourierEnergy (Torus.periodicToTorusL2 (Torus.realToComplex f) ⋯) ∧ fourierEnergy (Torus.periodicToTorusL2 (Torus.realToComplex f) ⋯) = gradNormSq (spaceGrad f)

Real smooth periodic functions enter the gradient-energy carrier.