Periodic volume-preserving diffeomorphisms

structure AVenhance.Infra.Ergodic.PeriodicVolumePreservingDiffeomorphism (d : ℕ) : Type

A smooth diffeomorphism of Vec d whose lift commutes with integer lattice translations and which preserves Lebesgue measure.

• toFun : Homogenization.Vec d → Homogenization.Vec d

  Forward Euclidean diffeomorphism preserving the periodic lattice and volume.

• invFun : Homogenization.Vec d → Homogenization.Vec d

  Inverse of the periodic volume-preserving diffeomorphism.

• contDiff_toFun : ContDiff ℝ (↑⊤) self.toFun
• contDiff_invFun : ContDiff ℝ (↑⊤) self.invFun
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• lattice_equivariant (x : Homogenization.Vec d) (k : Fin d → ℤ) : self.toFun (x + latticeVector k) = self.toFun x + latticeVector k
• measurePreserving : MeasureTheory.MeasurePreserving self.toFun MeasureTheory.volume MeasureTheory.volume

@[instance_reducible]

instance AVenhance.Infra.Ergodic.instCoeFunPeriodicVolumePreservingDiffeomorphismForallVec {d : ℕ} : CoeFun (PeriodicVolumePreservingDiffeomorphism d) fun (x : PeriodicVolumePreservingDiffeomorphism d) => Homogenization.Vec d → Homogenization.Vec d

Equations

• AVenhance.Infra.Ergodic.instCoeFunPeriodicVolumePreservingDiffeomorphismForallVec = { coe := AVenhance.Infra.Ergodic.PeriodicVolumePreservingDiffeomorphism.toFun }

noncomputable def AVenhance.Infra.Ergodic.Flow.negativeCoordinateBasis (d : ℕ) : Module.Basis (Fin d) ℝ (Homogenization.Vec d)

Negative coordinate basis used to represent the periodic lattice.

Equations

• AVenhance.Infra.Ergodic.Flow.negativeCoordinateBasis d = (Pi.basisFun ℝ (Fin d)).map (LinearEquiv.neg ℝ)

theorem AVenhance.Infra.Ergodic.Flow.negativeCoordinateBasis_repr {d : ℕ} (x : Homogenization.Vec d) (i : Fin d) : ((negativeCoordinateBasis d).repr x) i = -x i

def AVenhance.Infra.Ergodic.Flow.flowLattice (d : ℕ) : AddSubgroup (Homogenization.Vec d)

Integer lattice spanned by the negative coordinate basis.

Equations

• AVenhance.Infra.Ergodic.Flow.flowLattice d = (Submodule.span ℤ (Set.range ⇑(AVenhance.Infra.Ergodic.Flow.negativeCoordinateBasis d))).toAddSubgroup

def AVenhance.Infra.Ergodic.Flow.flowLatticeOne (d : ℕ) : ↥(flowLattice d)

The all-ones vector as an element of the flow lattice.

Equations

• AVenhance.Infra.Ergodic.Flow.flowLatticeOne d = ⟨fun (x : Fin d) => 1, ⋯⟩

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

Translated fundamental domain that agrees with the unit cell.

Equations

• AVenhance.Infra.Ergodic.Flow.flowFundamentalCell d = AVenhance.Infra.Ergodic.Flow.flowLatticeOne d +ᵥ ZSpan.fundamentalDomain (AVenhance.Infra.Ergodic.Flow.negativeCoordinateBasis d)

theorem AVenhance.Infra.Ergodic.Flow.unitCellSet_eq_flowFundamentalCell {d : ℕ} : unitCellSet d = flowFundamentalCell d

theorem AVenhance.Infra.Ergodic.Flow.flowFundamentalCell_isAddFundamentalDomain (d : ℕ) : MeasureTheory.IsAddFundamentalDomain (↥(flowLattice d)) (flowFundamentalCell d) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.Flow.flowLattice_mem_latticeVector {d : ℕ} (g : ↥(flowLattice d)) : ∃ (k : Fin d → ℤ), ↑g = latticeVector k

noncomputable def AVenhance.Infra.Ergodic.Flow.flowLatticeCoordinates {d : ℕ} (g : ↥(flowLattice d)) : Fin d → ℤ

Integer coordinates of a vector in the flow lattice.

Equations

• AVenhance.Infra.Ergodic.Flow.flowLatticeCoordinates g i = Classical.choose ⋯

theorem AVenhance.Infra.Ergodic.Flow.flowLatticeCoordinates_spec {d : ℕ} (g : ↥(flowLattice d)) (i : Fin d) : ↑(flowLatticeCoordinates g i) = ((negativeCoordinateBasis d).repr ↑g) i

theorem AVenhance.Infra.Ergodic.Flow.flowLattice_countable (d : ℕ) : Countable ↥(flowLattice d)

noncomputable def AVenhance.Infra.Ergodic.Flow.flowMeasurableEquiv {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) : Homogenization.Vec d ≃ᵐ Homogenization.Vec d

Measurable equivalence induced by a periodic volume-preserving diffeomorphism.

Equations

• AVenhance.Infra.Ergodic.Flow.flowMeasurableEquiv X = { toFun := X.toFun, invFun := X.invFun, left_inv := ⋯, right_inv := ⋯, measurable_toFun := ⋯, measurable_invFun := ⋯ }

theorem AVenhance.Infra.Ergodic.Flow.flowLattice_translation_invariant {d : ℕ} {α : Type u_1} {f : Homogenization.Vec d → α} (hf : IsZPeriodic f) (g : ↥(flowLattice d)) (x : Homogenization.Vec d) : f (g +ᵥ x) = f x

theorem AVenhance.Infra.Ergodic.Flow.flowEquiv_semiconj {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) (g : ↥(flowLattice d)) (x : Homogenization.Vec d) : X.toFun (g +ᵥ x) = g +ᵥ X.toFun x

theorem AVenhance.Infra.Ergodic.Flow.flow_imageFundamentalCell_isAddFundamentalDomain {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) : MeasureTheory.IsAddFundamentalDomain (↥(flowLattice d)) (X.toFun '' flowFundamentalCell d) MeasureTheory.volume

theorem AVenhance.Infra.Ergodic.cellAverage_comp_flow_eq {d : ℕ} (f : Homogenization.Vec d → ℝ) (hf : IsZPeriodic f) (X : PeriodicVolumePreservingDiffeomorphism d) : (cellAverage fun (x : Homogenization.Vec d) => f (X.toFun x)) = cellAverage f

A periodic cell average is invariant under a smooth, measure-preserving lattice-equivariant diffeomorphism.

theorem AVenhance.Infra.Ergodic.PeriodicVolumePreservingDiffeomorphism.inv_lattice_equivariant {d : ℕ} (X : PeriodicVolumePreservingDiffeomorphism d) (x : Homogenization.Vec d) (k : Fin d → ℤ) : X.invFun (x + latticeVector k) = X.invFun x + latticeVector k

The inverse lift of an equivariant diffeomorphism is equivariant too.

theorem AVenhance.Infra.Ergodic.cellAverage_mul_comp_inv_eq {d : ℕ} {f g : Homogenization.Vec d → ℝ} (hf : IsZPeriodic f) (hg : IsZPeriodic g) (X : PeriodicVolumePreservingDiffeomorphism d) : (cellAverage fun (x : Homogenization.Vec d) => f x * g (X.invFun x)) = cellAverage fun (x : Homogenization.Vec d) => f (X.toFun x) * g x

Change of variables by a periodic measure-preserving diffeomorphism moves the inverse composition from the oscillatory factor onto the smooth factor.

theorem AVenhance.Infra.Ergodic.IsZPeriodic.comp_invFlow {d : ℕ} {α : Type u_1} {f : Homogenization.Vec d → α} (hf : IsZPeriodic f) (X : PeriodicVolumePreservingDiffeomorphism d) : IsZPeriodic fun (x : Homogenization.Vec d) => f (X.invFun x)

Composing a lattice-periodic function with the inverse flow map preserves its periodicity.