Decay of all derivatives of a smooth periodic force with bounded time support

Each actual iterated derivative is continuous and spatially periodic, hence bounded on a compact time interval after reduction to a fundamental cube. Beyond the time support it is zero by locality of differentiation.

def NavierStokes.CompactForceDecay.unitCube : Set ProblemStatement.Space

The closed spatial unit cube, transported to the Euclidean space used by the PDE statement.

Equations

• NavierStokes.CompactForceDecay.unitCube = ⇑(WithLp.equiv 2 (Fin 3 → ℝ)).symm '' Set.univ.pi fun (x : Fin 3) => Set.Icc 0 1

theorem NavierStokes.CompactForceDecay.isCompact_unitCube : IsCompact unitCube

noncomputable def NavierStokes.CompactForceDecay.integerShift (n : Fin 3 → ℤ) : ProblemStatement.Space

Integer coordinate translation.

Equations

• NavierStokes.CompactForceDecay.integerShift n = ∑ i : Fin 3, n i • NavierStokes.ProblemStatement.coordinateVector i

@[simp]

theorem NavierStokes.CompactForceDecay.integerShift_apply (n : Fin 3 → ℤ) (j : Fin 3) : (integerShift n).ofLp j = ↑(n j)

noncomputable def NavierStokes.CompactForceDecay.fractionalPoint (x : ProblemStatement.Space) : ProblemStatement.Space

The coordinatewise fractional part of a spatial point.

Equations

• NavierStokes.CompactForceDecay.fractionalPoint x = (WithLp.equiv 2 (Fin 3 → ℝ)).symm fun (i : Fin 3) => Int.fract (x.ofLp i)

theorem NavierStokes.CompactForceDecay.fractionalPoint_mem_unitCube (x : ProblemStatement.Space) : fractionalPoint x ∈ unitCube

theorem NavierStokes.CompactForceDecay.fractionalPoint_eq_sub (x : ProblemStatement.Space) : fractionalPoint x = x - integerShift fun (i : Fin 3) => ⌊x.ofLp i⌋

theorem NavierStokes.CompactForceDecay.periodic_integerShift {V : Type u_1} {g : ProblemStatement.SpaceTime → V} (hg : ProblemStatement.UnitSpatialPeriodsOn Set.univ g) (t : ℝ) (n : Fin 3 → ℤ) : Function.Periodic (fun (x : ProblemStatement.Space) => g (t, x)) (integerShift n)

theorem NavierStokes.CompactForceDecay.periodic_fractionalPoint {V : Type u_1} {g : ProblemStatement.SpaceTime → V} (hg : ProblemStatement.UnitSpatialPeriodsOn Set.univ g) (t : ℝ) (x : ProblemStatement.Space) : g (t, fractionalPoint x) = g (t, x)

All points have the same field value as a point in the closed unit cube.

theorem NavierStokes.CompactForceDecay.periodic_bound_on_timeInterval {V : Type u_1} [NormedAddCommGroup V] {g : ProblemStatement.SpaceTime → V} (hg : Continuous g) (hper : ProblemStatement.UnitSpatialPeriodsOn Set.univ g) (a b : ℝ) : ∃ (C : ℝ), 0 < C ∧ ∀ t ∈ Set.Icc a b, ∀ (x : ProblemStatement.Space), ‖g (t, x)‖ ≤ C

A bound for a continuous periodic field on a compact interval follows from compactness of the interval times the actual fundamental cube.

theorem NavierStokes.CompactForceDecay.iteratedFDeriv_periods {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} (hf : ProblemStatement.UnitSpatialPeriodsOn Set.univ f) (m : ℕ) : ProblemStatement.UnitSpatialPeriodsOn Set.univ (iteratedFDeriv ℝ m f)

Unit spatial periods pass to the full derivative tensor, including all time and mixed derivatives. No derivative bound is assumed here.

theorem NavierStokes.CompactForceDecay.iteratedFDeriv_eq_zero_after {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] {f : ProblemStatement.SpaceTime → V} {T : ℝ} (hzero : ∀ (t : ℝ), T ≤ t → ∀ (x : ProblemStatement.Space), f (t, x) = 0) (m : ℕ) {t : ℝ} (ht : T < t) (x : ProblemStatement.Space) : iteratedFDeriv ℝ m f (t, x) = 0

Differentiation is local: every full derivative vanishes at times strictly after a uniform zero-tail threshold, including derivative order zero.

theorem NavierStokes.CompactForceDecay.iteratedFDeriv_decay (f : ProblemStatement.VelocityField) (hf : ContDiff ℝ (↑⊤) f) (hper : ProblemStatement.UnitSpatialPeriodsOn Set.univ f) (hsupport : ProblemStatement.CompactFutureTimeSupport f) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space), ‖iteratedFDeriv ℝ m f (t, x)‖ ≤ C * (1 + t) ^ (-K)

Every actual full derivative has arbitrary polynomial decay. The input smoothness and periods are global; compact future time support is the exact notion from the PDE specification.

noncomputable def NavierStokes.CompactForceDecay.spacetimeCoordinate : Fin 4 → ProblemStatement.SpaceTime

The four coordinate directions in the product spacetime norm.

Equations

• NavierStokes.CompactForceDecay.spacetimeCoordinate i = Fin.cases (1, 0) (fun (i : Fin 3) => (0, NavierStokes.ProblemStatement.coordinateVector i)) i

@[simp]

theorem NavierStokes.CompactForceDecay.norm_spacetimeCoordinate (i : Fin 4) : ‖spacetimeCoordinate i‖ = 1

theorem NavierStokes.CompactForceDecay.mixed_component_le_full (f : ProblemStatement.VelocityField) (m : ℕ) (z : ProblemStatement.SpaceTime) (directions : Fin m → Fin 4) (j : Fin 3) : |((iteratedFDeriv ℝ m f z) fun (i : Fin m) => spacetimeCoordinate (directions i)).ofLp j| ≤ ‖iteratedFDeriv ℝ m f z‖

Evaluating a full derivative on coordinate unit vectors, then taking one output component, is controlled by its full multilinear operator norm.

theorem NavierStokes.CompactForceDecay.mixed_coordinate_decay (f : ProblemStatement.VelocityField) (hf : ContDiff ℝ (↑⊤) f) (hper : ProblemStatement.UnitSpatialPeriodsOn Set.univ f) (hsupport : ProblemStatement.CompactFutureTimeSupport f) (m : ℕ) (K : ℝ) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ ∀ (t : ℝ), 0 ≤ t → ∀ (x : ProblemStatement.Space) (directions : Fin m → Fin 4) (j : Fin 3), |((iteratedFDeriv ℝ m f (t, x)) fun (i : Fin m) => spacetimeCoordinate (directions i)).ofLp j| ≤ C * (1 + t) ^ (-K)

Arbitrary polynomial decay for every coordinate mixed differential of every output component, with the same constant as the full derivative bound.