The frequency split in the homogeneous H⁻¹ ergodic estimate

@[instance_reducible]

noncomputable def AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneErgodicCoreMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

• AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneErgodicCoreMeasureSpace1 = { toMeasurableSpace := QuotientAddGroup.measurableSpace (AddSubgroup.zmultiples 1), volume := AddCircle.haarAddCircle }

theorem AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneErgodicCoreMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem AVenhance.Infra.Ergodic.avInfraErgodicHMinusOneErgodicCoreIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.mFourierCoeff_character {d : ℕ} (q k : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (⇑(UnitAddTorus.mFourier k)) q = if q = k then 1 else 0

theorem AVenhance.Infra.Ergodic.finite_frequencyBall {d : ℕ} (M : ℕ) : {k : Fin d → ℤ | ‖k‖ ≤ ↑M}.Finite

noncomputable def AVenhance.Infra.Ergodic.frequencyBall {d : ℕ} (M : ℕ) : Finset (Fin d → ℤ)

Finite set of integer frequencies within the specified frequency bound.

Equations

• AVenhance.Infra.Ergodic.frequencyBall M = ⋯.toFinset

theorem AVenhance.Infra.Ergodic.mem_frequencyBall {d M : ℕ} {k : Fin d → ℤ} : k ∈ frequencyBall M ↔ ‖k‖ ≤ ↑M

theorem AVenhance.Infra.Ergodic.frequencyBall_neg {d : ℕ} (M : ℕ) {k : Fin d → ℤ} (hk : k ∈ frequencyBall M) : -k ∈ frequencyBall M

noncomputable def AVenhance.Infra.Ergodic.fourierCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : C(UnitAddTorus (Fin d), ℂ)

Finite Fourier sum on the torus with the supplied coefficients.

Equations

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

theorem AVenhance.Infra.Ergodic.continuous_unitTorus_integrable {d : ℕ} {u : UnitAddTorus (Fin d) → ℂ} (hu : Continuous u) : MeasureTheory.Integrable u MeasureTheory.volume

def AVenhance.Infra.Ergodic.closedUnitCube {d : ℕ} : Set (Homogenization.Vec d)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Ergodic.closedUnitCube = Set.univ.pi fun (x : Fin d) => Set.Icc 0 1

theorem AVenhance.Infra.Ergodic.unitCell_subset_closedUnitCube {d : ℕ} : Torus.unitCell d ⊆ closedUnitCube

theorem AVenhance.Infra.Ergodic.continuous_complex_unitCell_integrable {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell d) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.mFourierCoeff_sum {d : ℕ} {ι : Type u_1} (S : Finset ι) (F : ι → UnitAddTorus (Fin d) → ℂ) (q : Fin d → ℤ) (hF : ∀ k ∈ S, MeasureTheory.Integrable (fun (x : UnitAddTorus (Fin d)) => (UnitAddTorus.mFourier (-q)) x * F k x) MeasureTheory.volume) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin d)) => ∑ k ∈ S, F k x) q = ∑ k ∈ S, UnitAddTorus.mFourierCoeff (F k) q

theorem AVenhance.Infra.Ergodic.mFourierCoeff_const_smul_character {d : ℕ} (c : ℂ) (q k : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (fun (x : UnitAddTorus (Fin d)) => c * (UnitAddTorus.mFourier k) x) q = if q = k then c else 0

theorem AVenhance.Infra.Ergodic.mFourierCoeff_fourierCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (q : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (⇑(fourierCutoff M a)) q = if q ∈ frequencyBall M then a q else 0

theorem AVenhance.Infra.Ergodic.fourierCutoff_star_eq {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (ha : ∀ (k : Fin d → ℤ), a (-k) = star (a k)) (x : UnitAddTorus (Fin d)) : star ((fourierCutoff M a) x) = (fourierCutoff M a) x

noncomputable def AVenhance.Infra.Ergodic.realFourierCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : C(UnitAddTorus (Fin d), ℝ)

Real part of the finite torus Fourier sum.

Equations

• AVenhance.Infra.Ergodic.realFourierCutoff M a = { toFun := fun (x : UnitAddTorus (Fin d)) => ((AVenhance.Infra.Ergodic.fourierCutoff M a) x).re, continuous_toFun := ⋯ }

theorem AVenhance.Infra.Ergodic.realFourierCutoff_complexification {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (ha : ∀ (k : Fin d → ℤ), a (-k) = star (a k)) : (fun (x : UnitAddTorus (Fin d)) => ↑((realFourierCutoff M a) x)) = ⇑(fourierCutoff M a)

theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_real_neg {d : ℕ} {f : Homogenization.Vec d → ℝ} (k : Fin d → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec d) => ↑(f x)) (-k) = star (Torus.smoothFourierCoeff (fun (x : Homogenization.Vec d) => ↑(f x)) k)

noncomputable def AVenhance.Infra.Ergodic.complexEuclideanCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (x : Homogenization.Vec d) : ℂ

Finite Fourier sum evaluated on Euclidean space using periodic characters.

Equations

• AVenhance.Infra.Ergodic.complexEuclideanCutoff M a x = ∑ k ∈ AVenhance.Infra.Ergodic.frequencyBall M, a k * AVenhance.Infra.Torus.torusCharacter (-k) x

noncomputable def AVenhance.Infra.Ergodic.euclideanFourierCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (x : Homogenization.Vec d) : ℝ

Real part of the Euclidean finite Fourier sum.

Equations

• AVenhance.Infra.Ergodic.euclideanFourierCutoff M a x = (AVenhance.Infra.Ergodic.complexEuclideanCutoff M a x).re

theorem AVenhance.Infra.Ergodic.complexEuclideanCutoff_smooth {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : ContDiff ℝ ⊤ (complexEuclideanCutoff M a)

theorem AVenhance.Infra.Ergodic.complexEuclideanCutoff_periodic {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : IsZPeriodic (complexEuclideanCutoff M a)

theorem AVenhance.Infra.Ergodic.euclideanFourierCutoff_contDiff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : ContDiff ℝ ⊤ (euclideanFourierCutoff M a)

theorem AVenhance.Infra.Ergodic.euclideanFourierCutoff_periodic {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) : IsZPeriodic (euclideanFourierCutoff M a)

theorem AVenhance.Infra.Ergodic.periodicToTorus_euclideanFourierCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (y : UnitAddTorus (Fin d)) : Torus.periodicToTorus (fun (x : Homogenization.Vec d) => ↑(euclideanFourierCutoff M a x)) y = ↑((realFourierCutoff M a) y)

theorem AVenhance.Infra.Ergodic.mFourierCoeff_periodicToTorus_eq_smooth {d : ℕ} {f : Homogenization.Vec d → ℂ} (hper : Torus.IsZdPeriodic f) (hf : Continuous f) (k : Fin d → ℤ) : UnitAddTorus.mFourierCoeff (⇑{ toFun := Torus.periodicToTorus f, continuous_toFun := ⋯ }) k = Torus.smoothFourierCoeff f k

theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_sub {d : ℕ} {f g : Homogenization.Vec d → ℂ} (hf : Continuous f) (hg : Continuous g) (k : Fin d → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec d) => f x - g x) k = Torus.smoothFourierCoeff f k - Torus.smoothFourierCoeff g k

theorem AVenhance.Infra.Ergodic.hasCoordinateAnalyticL2Bounds_of_fourierDomination {d : ℕ} {u v : Homogenization.Vec d → ℂ} (hu : ContDiff ℝ (↑⊤) u) (huper : Torus.IsZdPeriodic u) (hv : ContDiff ℝ (↑⊤) v) (hvper : Torus.IsZdPeriodic v) (Cf r : ℝ) (hdom : ∀ (i : Fin d) (n : ℕ) (k : Fin d → ℤ), ‖Torus.smoothFourierCoeff (coordDerivIter i n u) k‖ ≤ ‖Torus.smoothFourierCoeff (coordDerivIter i n v) k‖) (hderiv : HasCoordinateAnalyticL2Bounds v Cf r) : HasCoordinateAnalyticL2Bounds u Cf r

theorem AVenhance.Infra.Ergodic.exists_coordinate_ge_of_piNorm_gt {d : ℕ} (hd : 0 < d) {M : ℕ} {k : Fin d → ℤ} (hk : ↑M < ‖k‖) : ∃ (i : Fin d), ↑M + 1 ≤ ‖↑(k i)‖

theorem AVenhance.Infra.Ergodic.fourierTailL2_le_of_coordinateAnalyticL2Bounds {d : ℕ} (hd : 0 < d) {v : Homogenization.Vec d → ℂ} (hv : ContDiff ℝ (↑⊤) v) (hvper : Torus.IsZdPeriodic v) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderiv : HasCoordinateAnalyticL2Bounds v Cf r) (M : ℕ) (hscale : 1 ≤ r * (↑M + 1)) {q : Homogenization.Vec d → ℂ} (hqcont : ContDiff ℝ (↑⊤) q) (hqcoeff : ∀ (k : Fin d → ℤ), Torus.smoothFourierCoeff q k = if ‖k‖ ≤ ↑M then 0 else Torus.smoothFourierCoeff v k) : (∫ (x : Homogenization.Vec d) in Torus.unitCell d, ‖q x‖ ^ 2) ^ (1 / 2) ≤ 1024 * (↑d + 1) * Cf * Real.exp (-r * (↑M + 1) / 512)

Parseval turns the repeated derivative bounds into an exponential L² tail for the Fourier modes outside a finite cube.

theorem AVenhance.Infra.Ergodic.smoothFourierCoeff_euclideanCutoff {d : ℕ} (M : ℕ) (a : (Fin d → ℤ) → ℂ) (ha : ∀ (k : Fin d → ℤ), a (-k) = star (a k)) (q : Fin d → ℤ) : Torus.smoothFourierCoeff (fun (x : Homogenization.Vec d) => ↑(euclideanFourierCutoff M a x)) q = if q ∈ frequencyBall M then a q else 0

noncomputable def AVenhance.Infra.Ergodic.lowProjection {d : ℕ} (f : Homogenization.Vec d → ℝ) (M : ℕ) : Homogenization.Vec d → ℝ

Low-frequency projection using the smooth Fourier coefficients of a real function.

Equations

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

noncomputable def AVenhance.Infra.Ergodic.highRemainder {d : ℕ} (f : Homogenization.Vec d → ℝ) (M : ℕ) : Homogenization.Vec d → ℝ

Remainder after subtracting the low-frequency projection.

Equations

• AVenhance.Infra.Ergodic.highRemainder f M x = f x - AVenhance.Infra.Ergodic.lowProjection f M x

theorem AVenhance.Infra.Ergodic.lowProjection_contDiff {d : ℕ} {f : Homogenization.Vec d → ℝ} (M : ℕ) : ContDiff ℝ ⊤ (lowProjection f M)

theorem AVenhance.Infra.Ergodic.lowProjection_periodic {d : ℕ} {f : Homogenization.Vec d → ℝ} (M : ℕ) : IsZPeriodic (lowProjection f M)

theorem AVenhance.Infra.Ergodic.highRemainder_contDiff {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (M : ℕ) : ContDiff ℝ (↑⊤) (highRemainder f M)

theorem AVenhance.Infra.Ergodic.highRemainder_periodic {d : ℕ} {f : Homogenization.Vec d → ℝ} (hper : IsZPeriodic f) (M : ℕ) : IsZPeriodic (highRemainder f M)

theorem AVenhance.Infra.Ergodic.lowHighCoordinateAnalyticL2Bounds {d : ℕ} (hd : 0 < d) {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hper : IsZPeriodic f) (Cf r : ℝ) (hderiv : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(f x)) Cf r) (M : ℕ) : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(lowProjection f M x)) Cf r ∧ HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(highRemainder f M x)) Cf r

theorem AVenhance.Infra.Ergodic.lowProjectionL2_le {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (M : ℕ) : (∫ (x : Homogenization.Vec d) in Torus.unitCell d, lowProjection f M x ^ 2) ^ (1 / 2) ≤ (∫ (x : Homogenization.Vec d) in Torus.unitCell d, f x ^ 2) ^ (1 / 2)

theorem AVenhance.Infra.Ergodic.unitCellSet_eq_torusUnitCell (d : ℕ) : unitCellSet d = Torus.unitCell d

theorem AVenhance.Infra.Ergodic.coordDeriv_realCast_ergodic {d : ℕ} {f : Homogenization.Vec d → ℝ} (hf : ContDiff ℝ 1 f) (i : Fin d) (x : Homogenization.Vec d) : Torus.coordDeriv i (fun (y : Homogenization.Vec d) => ↑(f y)) x = ↑((fderiv ℝ f x) (Homogenization.basisVec i))

theorem AVenhance.Infra.Ergodic.cellMemLp_two_of_localSquare {d : ℕ} {h : Homogenization.Vec d → ℝ} (hhmeas : MeasureTheory.AEStronglyMeasurable h MeasureTheory.volume) (hhsq : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |h x| ^ 2) MeasureTheory.volume) : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict (Torus.unitCell d)) ∧ MeasureTheory.MemLp (fun (x : Homogenization.Vec d) => ↑(h x)) 2 (MeasureTheory.volume.restrict (Torus.unitCell d))

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_le_of_torusFourierGap {d : ℕ} (hd : 0 < d) {h : Homogenization.Vec d → ℝ} (hh : MeasureTheory.MemLp (fun (x : Homogenization.Vec d) => ↑(h x)) (ENNReal.ofReal 2) (MeasureTheory.volume.restrict (Torus.unitCell d))) (M : ℝ) (hM : 0 < M) (hgap : ∀ (k : Fin d → ℤ), ‖k‖ < M → UnitAddTorus.mFourierCoeff (torusFunction fun (x : Homogenization.Vec d) => ↑(h x)) k = 0) : homogeneousHMinusOneNorm h ≤ ENNReal.ofReal ((2 * Real.pi * M)⁻¹ * (∫ (x : Homogenization.Vec d) in Torus.unitCell d, h x ^ 2) ^ (1 / 2))

An L² function with a Fourier gap has the reciprocal-frequency homogeneous dual bound in the cell normalization of the H⁻¹ test space.

theorem AVenhance.Infra.Ergodic.cellAverage_eq_torusUnitCellIntegral {d : ℕ} {v : Homogenization.Vec d → ℝ} : cellAverage v = ∫ (x : Homogenization.Vec d) in Torus.unitCell d, v x

theorem AVenhance.Infra.Ergodic.cellAverage_add_of_locallyIntegrable {d : ℕ} {u v : Homogenization.Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hv : MeasureTheory.LocallyIntegrable v MeasureTheory.volume) : (cellAverage fun (x : Homogenization.Vec d) => u x + v x) = cellAverage u + cellAverage v

theorem AVenhance.Infra.Ergodic.homogeneousHMinusOneNorm_add_le_of_locallyIntegrable {d : ℕ} {u v : Homogenization.Vec d → ℝ} (hu : MeasureTheory.LocallyIntegrable u MeasureTheory.volume) (hv : MeasureTheory.LocallyIntegrable v MeasureTheory.volume) : (homogeneousHMinusOneNorm fun (x : Homogenization.Vec d) => u x + v x) ≤ homogeneousHMinusOneNorm u + homogeneousHMinusOneNorm v

theorem AVenhance.Infra.Ergodic.productL2_le_of_coordinateAnalyticL2Bounds {d : ℕ} (hd : 0 < d) {u g : Homogenization.Vec d → ℝ} (hu : ContDiff ℝ (↑⊤) u) (huper : IsZPeriodic u) (Cf r : ℝ) (hCf : 0 ≤ Cf) (hr : 0 < r) (hderiv : HasCoordinateAnalyticL2Bounds (fun (x : Homogenization.Vec d) => ↑(u x)) Cf r) (hg2 : MeasureTheory.LocallyIntegrable (fun (x : Homogenization.Vec d) => |g x| ^ 2) MeasureTheory.volume) {N : ℕ} (hN : 0 < N) (hfast : IsFastPeriodic N g) (hNr : 2 ≤ r * ↑N) : (∫ (x : Homogenization.Vec d) in Torus.unitCell d, (u x * g x) ^ 2) ^ (1 / 2) ≤ ((∫ (x : Homogenization.Vec d) in Torus.unitCell d, u x ^ 2) ^ (1 / 2) + 32 * (∑' (k : Fin d → ℤ), Real.exp (-(1 / 1024) * ‖k‖)) ^ (1 / 2) * Cf * Real.exp (-r * ↑N / 4096)) * (∫ (x : Homogenization.Vec d) in Torus.unitCell d, g x ^ 2) ^ (1 / 2)

The square covariance estimate gives an L² bound for a slow-fast product.