Joint space-time bounds for ordered spatial derivatives of smooth periodic data.

@[reducible, inline]

abbrev AVenhance.Infra.Classical.ClassicalDerivativeWordIndex (s : ℕ) : Type

Finite indices for all ordered coordinate-derivative words of length at most s.

Equations

• AVenhance.Infra.Classical.ClassicalDerivativeWordIndex s = ((n : Fin (s + 1)) × (Fin ↑n → Fin 2))

def AVenhance.Infra.Classical.classicalDerivativeWordOfIndex {s : ℕ} (a : ClassicalDerivativeWordIndex s) : List (Fin 2)

Convert a finite derivative index to its ordered coordinate word.

Equations

• AVenhance.Infra.Classical.classicalDerivativeWordOfIndex a = List.ofFn a.snd

theorem AVenhance.Infra.Classical.classicalDerivativeWordOfIndex_length_le {s : ℕ} (a : ClassicalDerivativeWordIndex s) : (classicalDerivativeWordOfIndex a).length ≤ s

def AVenhance.Infra.Classical.classicalDerivativeWordIndexOfList {s : ℕ} (w : List (Fin 2)) (hw : w.length ≤ s) : ClassicalDerivativeWordIndex s

Every ordered coordinate word of length at most s has a finite derivative index.

Equations

• AVenhance.Infra.Classical.classicalDerivativeWordIndexOfList w hw = ⟨⟨w.length, ⋯⟩, w.get⟩

theorem AVenhance.Infra.Classical.classicalDerivativeWordOfIndexOfList {s : ℕ} (w : List (Fin 2)) (hw : w.length ≤ s) : classicalDerivativeWordOfIndex (classicalDerivativeWordIndexOfList w hw) = w

def AVenhance.Infra.Classical.classicalHalfSpace : Set (ℝ × Homogenization.Vec 2)

Joint time-space domain with nonnegative time, including the initial trace.

Equations

• AVenhance.Infra.Classical.classicalHalfSpace = Set.Ici 0 ×ˢ Set.univ

theorem AVenhance.Infra.Classical.GalerkinBounds.classicalHalfSpace_uniqueDiff : UniqueDiffOn ℝ classicalHalfSpace

theorem AVenhance.Infra.Classical.GalerkinBounds.classicalWordDerivative_periodic_aux (w : List (Fin 2)) (f : Homogenization.Vec 2 → ℝ) (hper : IsZ2Periodic f) : IsZ2Periodic (classicalWordDerivative w f)

def AVenhance.Infra.Classical.classicalJointWordDerivative (w : List (Fin 2)) (f : ℝ × Homogenization.Vec 2 → ℝ) : ℝ × Homogenization.Vec 2 → ℝ

Repeated spatial directional derivatives of a joint space-time scalar, taken using the within-derivative on the nonnegative-time domain.

Equations

• One or more equations did not get rendered due to their size.
• AVenhance.Infra.Classical.classicalJointWordDerivative [] f = f

theorem AVenhance.Infra.Classical.classicalJointWordDerivative_contDiffOn (w : List (Fin 2)) (f : ℝ × Homogenization.Vec 2 → ℝ) (hf : ContDiffOn ℝ (↑⊤) f classicalHalfSpace) : ContDiffOn ℝ (↑⊤) (classicalJointWordDerivative w f) classicalHalfSpace

theorem AVenhance.Infra.Classical.GalerkinBounds.classicalJointSection_directional_derivative (f : ℝ × Homogenization.Vec 2 → ℝ) (hf : ContDiffOn ℝ (↑⊤) f classicalHalfSpace) {t : ℝ} (ht : 0 ≤ t) (x : Homogenization.Vec 2) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => f (t, y)) x i = (fderivWithin ℝ f classicalHalfSpace (t, x)) (0, Homogenization.basisVec i)

theorem AVenhance.Infra.Classical.classicalJointWordDerivative_eq_slice (w : List (Fin 2)) (f : ℝ × Homogenization.Vec 2 → ℝ) (hf : ContDiffOn ℝ (↑⊤) f classicalHalfSpace) {t : ℝ} (ht : 0 ≤ t) (x : Homogenization.Vec 2) : classicalJointWordDerivative w f (t, x) = classicalWordDerivative w (fun (y : Homogenization.Vec 2) => f (t, y)) x

On every nonnegative-time slice, the joint within-derivative agrees with the ordinary ordered spatial derivative used by the Galerkin commutator calculus.

theorem AVenhance.Infra.Classical.exists_uniform_bound_of_continuous_spatiallyPeriodic (f : ℝ × Homogenization.Vec 2 → ℝ) (hf : ContinuousOn f (Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1)) (hper : ∀ (t : ℝ), 0 ≤ t → ∀ (k : Fin 2 → ℤ) (x : Homogenization.Vec 2), f (t, x + latticeShift k) = f (t, x)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖f (t, x)‖ ≤ C

A continuous function periodic in its spatial argument is uniformly bounded on a unit time interval times all of space.

theorem AVenhance.Infra.Classical.classicalWordDerivative_uniform_bound (w : List (Fin 2)) (f : ℝ × Homogenization.Vec 2 → ℝ) (hf : ContDiffOn ℝ (↑⊤) f classicalHalfSpace) (hper : ∀ (t : ℝ), 0 ≤ t → ∀ (k : Fin 2 → ℤ) (x : Homogenization.Vec 2), f (t, x + latticeShift k) = f (t, x)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (fun (y : Homogenization.Vec 2) => f (t, y)) x‖ ≤ C

Smooth joint half-space data and spatial periodicity give uniform bounds for every ordered spatial derivative on [0,1] × Vec 2.

theorem AVenhance.Infra.Classical.streamVel_wordDerivative_uniform_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (w : List (Fin 2)) (j : Fin 2) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (fun (y : Homogenization.Vec 2) => streamVel φ t y j) x‖ ≤ C

Uniform derivative bounds for an admissible drift component.

theorem AVenhance.Infra.Classical.classicalForcingWord_uniform_bound (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) classicalHalfSpace) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (w : List (Fin 2)) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (F t) x‖ ≤ C

Uniform derivative bounds for the smooth periodic forcing.

theorem AVenhance.Infra.Classical.exists_streamVel_allWordDerivative_uniform_bound (φ : ℝ → Homogenization.Vec 2 → ℝ) (hφ : IsAdmissibleStream φ) (s : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (w : List (Fin 2)), w.length ≤ s → ∀ (j : Fin 2), ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (fun (y : Homogenization.Vec 2) => streamVel φ t y j) x‖ ≤ B

A single constant bounds every spatial derivative of the drift through order s, uniformly in the component, time, and space variables.

theorem AVenhance.Infra.Classical.exists_classicalForcing_allWordDerivative_uniform_bound (F : ℝ → Homogenization.Vec 2 → ℝ) (hF : ContDiffOn ℝ (↑⊤) (Function.uncurry F) classicalHalfSpace) (hFper : ∀ (t : ℝ), 0 ≤ t → IsZ2Periodic (F t)) (s : ℕ) : ∃ (B : ℝ), 0 ≤ B ∧ ∀ (w : List (Fin 2)), w.length ≤ s → ∀ t ∈ Set.Icc 0 1, ∀ (x : Homogenization.Vec 2), ‖classicalWordDerivative w (F t) x‖ ≤ B

A single constant bounds every spatial derivative of the forcing through order s, uniformly on the physical time interval and on all of space.