Heat-flow energy estimates for the periodic weak H1 carriers.

@[instance_reducible]

noncomputable def frozenHeatMeasureSpaceUnitAddCircle : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem frozenHeatIsAddHaarUnitAddCircle : MeasureTheory.volume.IsAddHaarMeasure

theorem frozenHeatProbabilityUnitAddCircle : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Heat.FrozenEstimates.summable_sq_mFourierCoeff (f : ↥(Torus.TorusL2 2)) : Summable fun (k : Frequency) => ‖UnitAddTorus.mFourierCoeff (↑↑f) k‖ ^ 2

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

theorem AVenhance.Infra.Heat.FrozenEstimates.frozenH1_energyTerm_eq_gradientCoeffSum {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (k : Frequency) : fourierEnergyTerm (frozenPeriodicH1ValueL2 h) k = ∑ i : Fin 2, ‖UnitAddTorus.mFourierCoeff (↑↑(frozenPeriodicH1GradientL2 h i)) k‖ ^ 2

theorem AVenhance.Infra.Heat.FrozenEstimates.integrableOn_sq_of_memL2On {f : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) : MeasureTheory.IntegrableOn (fun (x : Homogenization.Vec 2) => f x ^ 2) unitCube MeasureTheory.volume

theorem AVenhance.Infra.Heat.FrozenEstimates.gradNormSq_eq_sum_componentL2 {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (hDu : Homogenization.GradMemL2On unitCube Du) : gradNormSq Du = ∑ i : Fin 2, l2NormSq fun (x : Homogenization.Vec 2) => Du x i

theorem AVenhance.Infra.Heat.hasFiniteFourierEnergy_frozenPeriodicH1 {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) : HasFiniteFourierEnergy (frozenPeriodicH1ValueL2 h)

The Fourier Dirichlet energy of any periodic weak H1 value is finite.

theorem AVenhance.Infra.Heat.fourierEnergy_frozenPeriodicH1_eq_gradNormSq {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) : fourierEnergy (frozenPeriodicH1ValueL2 h) = gradNormSq Du

Parseval identifies the spectral Dirichlet energy with the squared weak-gradient norm for arbitrary IsPeriodicH1With data.

theorem AVenhance.Infra.Heat.FrozenEstimates.frozenPeriodicH1Value_norm {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) : ‖frozenPeriodicH1ValueL2 h‖ = √(l2NormSq u)

theorem AVenhance.Infra.Heat.FrozenEstimates.frozenPeriodicH1Value_normSq {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) : ‖frozenPeriodicH1ValueL2 h‖ ^ 2 = l2NormSq u

theorem AVenhance.Infra.Heat.FrozenEstimates.l2NormSq_nonneg (u : Homogenization.Vec 2 → ℝ) : 0 ≤ l2NormSq u

theorem AVenhance.Infra.Heat.FrozenEstimates.heatGradNormSq_nonneg (Du : Homogenization.Vec 2 → Homogenization.Vec 2) : 0 ≤ gradNormSq Du

theorem AVenhance.Infra.Heat.normSq_sub_heatTorusL2_le_frozenPeriodicH1 {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) {s : ℝ} (hs : 0 ≤ s) : ‖frozenPeriodicH1ValueL2 h - heatTorusL2 s hs (frozenPeriodicH1ValueL2 h)‖ ^ 2 ≤ s * gradNormSq Du

The heat approximation error is at most s times the squared weak gradient norm for arbitrary periodic H1 data.

theorem AVenhance.Infra.Heat.FrozenEstimates.torusCharacter_zero (x : Homogenization.Vec 2) : Torus.torusCharacter 0 x = 1

theorem AVenhance.Infra.Heat.FrozenEstimates.frozenPeriodicH1_zeroCoeff {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (hmean : Homogenization.MeanZeroOn unitCube u) : UnitAddTorus.mFourierCoeff (↑↑(frozenPeriodicH1ValueL2 h)) 0 = 0

theorem AVenhance.Infra.Heat.FrozenEstimates.frozenPeriodicH1_torusMeanZero {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (hmean : Homogenization.MeanZeroOn unitCube u) : ∫ (x : UnitAddTorus (Fin 2)), ↑↑(frozenPeriodicH1ValueL2 h) x = 0

theorem AVenhance.Infra.Heat.meanZero_frozenPeriodicH1_fourierPoincare {u : Homogenization.Vec 2 → ℝ} {Du : Homogenization.Vec 2 → Homogenization.Vec 2} (h : IsPeriodicH1With u Du) (hmean : Homogenization.MeanZeroOn unitCube u) : l2NormSq u ≤ (4 * Real.pi ^ 2)⁻¹ * gradNormSq Du

Mean-zero periodic H1 data satisfy the mean-zero torus Poincare bound, written in the carriers.