Smooth jointly time-space periodic fields have globally bounded derivatives of each fixed order.

def AVenhance.Infra.Flow.jointLatticeShift (z : ℤ × (Fin 2 → ℤ)) : ℝ × Homogenization.Vec 2

A simultaneous integer shift in time and in the two spatial coordinates.

Equations

• AVenhance.Infra.Flow.jointLatticeShift z = (↑z.1, AVenhance.latticeShift z.2)

def AVenhance.Infra.Flow.IsJointPeriodicField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

Joint ℤ × ℤ² periodicity of a time-dependent vector field.

Equations

• AVenhance.Infra.Flow.IsJointPeriodicField b = ∀ (m : ℤ) (k : Fin 2 → ℤ) (t : ℝ) (x : Homogenization.Vec 2), b (t + ↑m) (x + AVenhance.latticeShift k) = b t x

structure AVenhance.Infra.Flow.SmoothPeriodicField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : Prop

A smooth jointly periodic field. In Mathlib's ContDiff order, ∞ is the coercion of (⊤ : ℕ∞), the C-infinity order used in the flow estimates.

• smooth : ContDiff ℝ (↑⊤) (Function.uncurry b)
• periodic : IsJointPeriodicField b

def AVenhance.Infra.Flow.PeriodicSmooth.jointUnitCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell used for smooth periodic field estimates.

Equations

• AVenhance.Infra.Flow.PeriodicSmooth.jointUnitCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Flow.PeriodicSmooth.isCompact_jointUnitCell : IsCompact jointUnitCell

theorem AVenhance.Infra.Flow.PeriodicSmooth.mem_jointUnitCell_normalize (p : ℝ × Homogenization.Vec 2) : p - jointLatticeShift (⌊p.1⌋, fun (i : Fin 2) => ⌊p.2 i⌋) ∈ jointUnitCell

theorem AVenhance.Infra.Flow.PeriodicSmooth.joint_normalize_add_shift (p : ℝ × Homogenization.Vec 2) : p - jointLatticeShift (⌊p.1⌋, fun (i : Fin 2) => ⌊p.2 i⌋) + jointLatticeShift (⌊p.1⌋, fun (i : Fin 2) => ⌊p.2 i⌋) = p

theorem AVenhance.Infra.Flow.iteratedFDeriv_jointPeriodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : IsJointPeriodicField b) (n : ℕ) (z : ℤ × (Fin 2 → ℤ)) (p : ℝ × Homogenization.Vec 2) : iteratedFDeriv ℝ n (Function.uncurry b) (p + jointLatticeShift z) = iteratedFDeriv ℝ n (Function.uncurry b) p

Iterated derivatives inherit the same lattice periodicity as the field.

theorem AVenhance.Infra.Flow.exists_global_iteratedFDeriv_bound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (n : ℕ) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (p : ℝ × Homogenization.Vec 2), ‖iteratedFDeriv ℝ n (Function.uncurry b) p‖ ≤ C

Every fixed-order mixed derivative of a smooth jointly periodic field is bounded on all of space-time. The bound may depend on the derivative order.