Periodicity for functions on Euclidean space

This local predicate records invariance under the integer lattice. The ergodic lemmas use it for scalar functions on Vec d.

@[instance_reducible]

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

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

Equations

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

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

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

def AVenhance.Infra.Ergodic.IsZPeriodic {d : ℕ} {α : Type u_1} (f : Homogenization.Vec d → α) : Prop

A function on Vec d is ℤ^d-periodic when it is invariant under every integer lattice translation.

Equations

• AVenhance.Infra.Ergodic.IsZPeriodic f = ∀ (x : Homogenization.Vec d) (k : Fin d → ℤ), f (x + fun (i : Fin d) => ↑(k i)) = f x

def AVenhance.Infra.Ergodic.latticeVector {d : ℕ} (k : Fin d → ℤ) : Homogenization.Vec d

The Euclidean vector represented by an integer lattice vector.

Equations

• AVenhance.Infra.Ergodic.latticeVector k i = ↑(k i)

theorem AVenhance.Infra.Ergodic.isZPeriodic_iff_isZ2Periodic {α : Type u_1} (f : Homogenization.Vec 2 → α) : IsZPeriodic f ↔ IsZ2Periodic f

In dimension two, the local ergodic periodicity predicate agrees with the campaign carrier.

def AVenhance.Infra.Ergodic.IsFastPeriodic {d : ℕ} (N : ℕ) (f : Homogenization.Vec d → ℝ) : Prop

Invariance under translations in N⁻¹ℤ^d.

Equations

• AVenhance.Infra.Ergodic.IsFastPeriodic N f = ∀ (x : Homogenization.Vec d) (k : Fin d → ℤ), f (x + fun (i : Fin d) => ↑(k i) / ↑N) = f x

theorem AVenhance.Infra.Ergodic.IsFastPeriodic.isZPeriodic {d N : ℕ} {f : Homogenization.Vec d → ℝ} (hN : 0 < N) (hf : IsFastPeriodic N f) : IsZPeriodic f

@[reducible, inline]

abbrev AVenhance.Infra.Ergodic.UnitTorus (d : ℕ) : Type

The unit torus with coordinates indexed by Fin d.

Equations

• AVenhance.Infra.Ergodic.UnitTorus d = UnitAddTorus (Fin d)

def AVenhance.Infra.Ergodic.unitCellSet (d : ℕ) : Set (Homogenization.Vec d)

The half-open unit cell used to compute spatial averages.

Equations

• AVenhance.Infra.Ergodic.unitCellSet d = {x : Homogenization.Vec d | ∀ (i : Fin d), x i ∈ Set.Ioc 0 1}

noncomputable def AVenhance.Infra.Ergodic.unitCellRepresentative {d : ℕ} (x : UnitTorus d) : Homogenization.Vec d

The representative in (0,1]^d of a point on the unit torus.

Equations

• AVenhance.Infra.Ergodic.unitCellRepresentative x = ↑((UnitAddTorus.measurableEquivPiIoc fun (x : Fin d) => 0) x)

noncomputable def AVenhance.Infra.Ergodic.fastTorusShift {d : ℕ} (N : ℕ) (i : Fin d) : UnitTorus d

Translation by one fast period in coordinate i on the unit torus.

Equations

• AVenhance.Infra.Ergodic.fastTorusShift N i j = if j = i then ↑(1 / ↑N) else 0

noncomputable def AVenhance.Infra.Ergodic.Periodic.fastRealShift {d : ℕ} (N : ℕ) (i : Fin d) : Homogenization.Vec d

Translation by the reciprocal frequency in one coordinate direction.

Equations

• AVenhance.Infra.Ergodic.Periodic.fastRealShift N i j = if j = i then 1 / ↑N else 0

noncomputable def AVenhance.Infra.Ergodic.torusFunction {d : ℕ} {α : Type u_1} (f : Homogenization.Vec d → α) (x : UnitTorus d) : α

The function on the torus obtained by evaluating a Euclidean function at the canonical unit-cell representative. For a IsZPeriodic function this representative is immaterial up to the usual boundary identifications.

Equations

• AVenhance.Infra.Ergodic.torusFunction f x = f (AVenhance.Infra.Ergodic.unitCellRepresentative x)

theorem AVenhance.Infra.Ergodic.Periodic.unitCellRepresentative_add_fastTorusShift {d N : ℕ} (hN : 0 < N) (i : Fin d) (x : UnitTorus d) : ∃ (k : Fin d → ℤ), unitCellRepresentative (x + fastTorusShift N i) = unitCellRepresentative x + fun (j : Fin d) => ↑((if j = i then 1 else 0) + ↑N * k j) / ↑N

theorem AVenhance.Infra.Ergodic.torusFunction_add_fastTorusShift_eq {d N : ℕ} {f : Homogenization.Vec d → ℝ} (hN : 0 < N) (hf : IsFastPeriodic N f) (i : Fin d) (x : UnitTorus d) : torusFunction f (x + fastTorusShift N i) = torusFunction f x

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

The normalized average of a Euclidean function over the unit torus, computed using its canonical representative in (0,1]^d.

Equations

• AVenhance.Infra.Ergodic.cellAverage f = ∫ (x : AVenhance.Infra.Ergodic.UnitTorus d), AVenhance.Infra.Ergodic.torusFunction f x

@[simp]

theorem AVenhance.Infra.Ergodic.cellAverage_const {d : ℕ} (c : ℝ) : (cellAverage fun (x : Homogenization.Vec d) => c) = c

theorem AVenhance.Infra.Ergodic.cellAverage_eq_torus_integral {d : ℕ} (f : Homogenization.Vec d → ℝ) : cellAverage f = ∫ (x : UnitTorus d), torusFunction f x

theorem AVenhance.Infra.Ergodic.cellAverage_eq_unitCellIntegral {d : ℕ} {f : Homogenization.Vec d → ℝ} : cellAverage f = ∫ (x : Homogenization.Vec d) in unitCellSet d, f x