Basic measurable and periodic infrastructure for the unit torus.

@[instance_reducible]

noncomputable def avInfraTorusBasicMeasureSpace1 : MeasureTheory.MeasureSpace UnitAddCircle

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

Equations

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

theorem avInfraTorusBasicMeasureIsAddHaarMeasure2 : MeasureTheory.volume.IsAddHaarMeasure

theorem avInfraTorusBasicIsProbabilityMeasure3 : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume

def AVenhance.Infra.Torus.unitCellAt (d : ℕ) (a : Fin d → ℝ) : Set (Homogenization.Vec d)

A translated half-open fundamental cell (aᵢ,aᵢ+1]^d.

Equations

• AVenhance.Infra.Torus.unitCellAt d a = {x : Homogenization.Vec d | ∀ (i : Fin d), x i ∈ Set.Ioc (a i) (a i + 1)}

def AVenhance.Infra.Torus.unitCell (d : ℕ) : Set (Homogenization.Vec d)

The half-open fundamental cell (0,1]^d. This convention matches UnitAddTorus.measurableEquivPiIoc and gives an exact fundamental domain.

Equations

• AVenhance.Infra.Torus.unitCell d = AVenhance.Infra.Torus.unitCellAt d fun (x : Fin d) => 0

theorem AVenhance.Infra.Torus.measurableSet_unitCellAt (d : ℕ) (a : Fin d → ℝ) : MeasurableSet (unitCellAt d a)

theorem AVenhance.Infra.Torus.measurableSet_unitCell (d : ℕ) : MeasurableSet (unitCell d)

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

The integer vector k, viewed as a real vector.

Equations

• AVenhance.Infra.Torus.intVector k i = ↑(k i)

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

A function is ℤ^d-periodic if integer translations leave it unchanged.

Equations

• AVenhance.Infra.Torus.IsZdPeriodic f = ∀ (k : Fin d → ℤ) (x : Homogenization.Vec d), f (x + AVenhance.Infra.Torus.intVector k) = f x

theorem AVenhance.Infra.Torus.isZdPeriodic_iff_frozen {α : Type u_1} (f : Homogenization.Vec 2 → α) : IsZdPeriodic f ↔ IsZ2Periodic f

In dimension two, the generic periodicity predicate agrees with the paper carrier.

theorem AVenhance.Infra.Torus.unitCell_ae_eq_unitCube : unitCell 2 =ᵐ[MeasureTheory.volume] unitCube

The open and half-open unit cells agree almost everywhere for Lebesgue measure.

theorem AVenhance.Infra.Torus.integral_unitCell_eq_unitCube {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Homogenization.Vec 2 → E) : ∫ (x : Homogenization.Vec 2) in unitCell 2, f x = ∫ (x : Homogenization.Vec 2) in unitCube, f x

Set integrals over the generic half-open cell and the open square agree.

def AVenhance.Infra.Torus.toUnitTorus (d : ℕ) (x : Homogenization.Vec d) : UnitAddTorus (Fin d)

The quotient map from Euclidean coordinates to the unit additive torus.

Equations

• AVenhance.Infra.Torus.toUnitTorus d x i = ↑(x i)

noncomputable def AVenhance.Infra.Torus.unitTorusRepresentative (d : ℕ) (x : UnitAddTorus (Fin d)) : Homogenization.Vec d

The representative of a torus point in the half-open cell (0,1]^d.

Equations

• AVenhance.Infra.Torus.unitTorusRepresentative d x i = ↑((AddCircle.equivIoc 1 0) (x i))

noncomputable def AVenhance.Infra.Torus.periodicToTorus {d : ℕ} {α : Type u_1} (f : Homogenization.Vec d → α) : UnitAddTorus (Fin d) → α

Transfer a Euclidean function to the torus by taking its canonical cell representative.

Equations

• AVenhance.Infra.Torus.periodicToTorus f x = f (AVenhance.Infra.Torus.unitTorusRepresentative d x)

def AVenhance.Infra.Torus.fromUnitTorus {d : ℕ} {α : Type u_1} (f : UnitAddTorus (Fin d) → α) : Homogenization.Vec d → α

Pull a torus function back to a function on Euclidean coordinates.

Equations

• AVenhance.Infra.Torus.fromUnitTorus f x = f (AVenhance.Infra.Torus.toUnitTorus d x)

@[simp]

theorem AVenhance.Infra.Torus.unitTorusRepresentative_toUnitTorus (d : ℕ) (x : Homogenization.Vec d) : unitTorusRepresentative d (toUnitTorus d x) = fun (i : Fin d) => ↑((AddCircle.equivIoc 1 0) ↑(x i))

theorem AVenhance.Infra.Torus.unitTorusRepresentative_eq_of_mem_unitCell {d : ℕ} {x : Homogenization.Vec d} (hx : x ∈ unitCell d) : unitTorusRepresentative d (toUnitTorus d x) = x

theorem AVenhance.Infra.Torus.Basic.representative_int_translate {d : ℕ} (x : Homogenization.Vec d) : ∃ (k : Fin d → ℤ), unitTorusRepresentative d (toUnitTorus d x) = x + intVector k

theorem AVenhance.Infra.Torus.fromUnitTorus_periodicToTorus {d : ℕ} {α : Type u_1} {f : Homogenization.Vec d → α} (hf : IsZdPeriodic f) : fromUnitTorus (periodicToTorus f) = f

Transferring a periodic function to the torus and pulling it back recovers it.

theorem AVenhance.Infra.Torus.isZdPeriodic_fromUnitTorus {d : ℕ} {α : Type u_1} (f : UnitAddTorus (Fin d) → α) : IsZdPeriodic (fromUnitTorus f)

Pulling back a torus function always gives a ℤ^d-periodic function.

@[simp]

theorem AVenhance.Infra.Torus.toUnitTorus_unitTorusRepresentative (d : ℕ) (x : UnitAddTorus (Fin d)) : toUnitTorus d (unitTorusRepresentative d x) = x

A torus point is recovered from the canonical representative of that point.

@[simp]

theorem AVenhance.Infra.Torus.periodicToTorus_fromUnitTorus {d : ℕ} {α : Type u_1} (f : UnitAddTorus (Fin d) → α) : periodicToTorus (fromUnitTorus f) = f

Pulling back the transfer of a torus function gives the original torus function.

theorem AVenhance.Infra.Torus.integral_fromUnitTorus_eq_unitCellAt {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : UnitAddTorus (Fin d) → E) (a : Fin d → ℝ) : ∫ (x : UnitAddTorus (Fin d)), f x = ∫ (x : Homogenization.Vec d) in unitCellAt d a, fromUnitTorus f x

Integration on the torus agrees with integration of the pullback over a translated unit cell. The cell is half-open, as in Mathlib's fundamental-domain measure equivalence.

theorem AVenhance.Infra.Torus.integral_periodicToTorus_eq_unitCell {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : Homogenization.Vec d → E) : ∫ (x : UnitAddTorus (Fin d)), periodicToTorus f x = ∫ (x : Homogenization.Vec d) in unitCell d, f x

Integration on the torus agrees with integration of the periodic transfer on the unit cell.

theorem AVenhance.Infra.Torus.integral_periodic_unitCellAt_eq {d : ℕ} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : Homogenization.Vec d → E} (hf : IsZdPeriodic f) (a : Fin d → ℝ) : ∫ (x : Homogenization.Vec d) in unitCellAt d a, f x = ∫ (x : Homogenization.Vec d) in unitCell d, f x

Integrals of a periodic function over any translated half-open unit cell agree.