The §4 flow slices as periodic volume-preserving diffeomorphisms

The flow slice X_{m-1,l}(t,·) (Ingredients.xFlow) with inverse Ingredients.xFlowInv is packaged as an Infra.Ergodic.PeriodicVolumePreservingDiffeomorphism 2, the input of the App C ergodic lemmas.

theorem AVenhance.Infra.Section5.LeftToShow.FlowDiffeo.streamFlowSmooth {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : Flow.SmoothPeriodicField (streamVel (Φ (m - 1)))

theorem AVenhance.Infra.Section5.LeftToShow.FlowDiffeo.streamFlowIsFlow {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : IsFlow (streamVel (Φ (m - 1))) (flow (streamVel (Φ (m - 1))) ⋯ ⋯)

theorem AVenhance.Infra.Section5.LeftToShow.FlowDiffeo.streamFlowPeriodic {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (t : ℝ) : IsZ2Periodic (streamVel (Φ (m - 1)) t)

theorem AVenhance.Infra.Section5.LeftToShow.FlowDiffeo.streamFlow_slice_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (t s : ℝ) : ContDiff ℝ ↑⊤ fun (x : Homogenization.Vec 2) => flow (streamVel (Φ (m - 1))) ⋯ ⋯ t x s

Spatial slices x ↦ X t x s of the construction flow are C^∞.

noncomputable def AVenhance.Infra.Section5.LeftToShow.xFlowDiffeo {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : Ergodic.PeriodicVolumePreservingDiffeomorphism 2

X_{m-1,l}(t,·) (xFlow) packaged for the App C ergodic lemmas.

Equations

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

@[simp]

theorem AVenhance.Infra.Section5.LeftToShow.xFlowDiffeo_toFun {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (xFlowDiffeo I hΦ m l t).toFun = I.xFlow hΦ m l t

@[simp]

theorem AVenhance.Infra.Section5.LeftToShow.xFlowDiffeo_invFun {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) : (xFlowDiffeo I hΦ m l t).invFun = I.xFlowInv hΦ m l t

theorem AVenhance.Infra.Section5.LeftToShow.xFlowInv_lattice_equivariant {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) (t : ℝ) (x : Homogenization.Vec 2) (k : Fin 2 → ℤ) : I.xFlowInv hΦ m l t (x + Ergodic.latticeVector k) = I.xFlowInv hΦ m l t x + Ergodic.latticeVector k