RelativeError: Euclidean energy control for divergence-free flow derivatives

The carrier Vec 2 has the coordinate sup norm, whereas vecNormSq is the sum of coordinate squares. In dimension two, the trace-free condition lets the latter energy grow at rate at most twice the sup-operator bound.

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.row_abs_sum_le_of_opNorm {A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {B : ℝ} (hA : ‖A‖ ≤ B) (i : Fin 2) : |A (Homogenization.basisVec 0) i| + |A (Homogenization.basisVec 1) i| ≤ B

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.traceFree_quadratic_le {A : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} {B : ℝ} (hA : ‖A‖ ≤ B) (htr : A (Homogenization.basisVec 0) 0 + A (Homogenization.basisVec 1) 1 = 0) (z : Homogenization.Vec 2) : Homogenization.vecDot (A z) z ≤ B * Homogenization.vecNormSq z

theorem AVenhance.Infra.Section5.RelativeError.divergenceFree_spatialDerivative_quadratic_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {B : ℝ} (hDb : ∀ (t : ℝ) (x : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b t x‖ ≤ B) (t : ℝ) (x z : Homogenization.Vec 2) : Homogenization.vecDot ((Flow.jointSpatialFDeriv b t x) z) z ≤ B * Homogenization.vecNormSq z

The divergence-free differential of a two-dimensional vector field has Euclidean logarithmic norm bounded by its operator norm on Vec 2.

theorem AVenhance.Infra.Section5.RelativeError.forwardFlow_derivative_vecNormSq_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {B : ℝ} (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) {s t : ℝ} (hst : s ≤ t) (x v : Homogenization.Vec 2) : Homogenization.vecNormSq ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) v) ≤ Homogenization.vecNormSq v * Real.exp (2 * B * (t - s))

The Euclidean squared norm of a forward flow derivative grows at the same exponential rate as the divergence-free logarithmic norm.

def AVenhance.Infra.Section5.RelativeError.euclideanTransposeApply (L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (w : Homogenization.Vec 2) : Homogenization.Vec 2

The Euclidean transpose action, written in the coordinate basis of Vec 2. It is the action that appears on gradients after composing with a map.

Equations

• AVenhance.Infra.Section5.RelativeError.euclideanTransposeApply L w i = ∑ j : Fin 2, L (Homogenization.basisVec i) j * w j

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.vecDot_sq_le (x y : Homogenization.Vec 2) : Homogenization.vecDot x y ^ 2 ≤ Homogenization.vecNormSq x * Homogenization.vecNormSq y

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.vecDot_transposeApply_eq (L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (w z : Homogenization.Vec 2) : Homogenization.vecDot (euclideanTransposeApply L w) z = Homogenization.vecDot w (L z)

theorem AVenhance.Infra.Section5.RelativeError.euclideanTranspose_vecNormSq_le (L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) {C : ℝ} (hL : ∀ (z : Homogenization.Vec 2), Homogenization.vecNormSq (L z) ≤ C ^ 2 * Homogenization.vecNormSq z) (w : Homogenization.Vec 2) : Homogenization.vecNormSq (euclideanTransposeApply L w) ≤ C ^ 2 * Homogenization.vecNormSq w

If a linear map has Euclidean energy norm at most C, then so does its transpose. The proof uses the dual characterization of the Euclidean norm.

def AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeField (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2

Reverse-time vector field in the Euclidean trace flow bound.

Equations

• AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeField b t x = -b (-t) x

def AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeFlow (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2

Flow with both times reversed in the Euclidean trace flow bound.

Equations

• AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeFlow X t x s = X (-t) x (-s)

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeField_smoothPeriodic {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) : Flow.SmoothPeriodicField (reverseTimeField b)

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeFlow_isFlow {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) : IsFlow (reverseTimeField b) (reverseTimeFlow X)

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeField_div_free {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) (r : ℝ) (x : Homogenization.Vec 2) : vecDiv (reverseTimeField b r) x = 0

theorem AVenhance.Infra.Section5.RelativeError.TraceEuclideanFlowBound.reverseTimeField_derivBound {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {B : ℝ} (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) (r : ℝ) (y : Homogenization.Vec 2) : ‖Flow.jointSpatialFDeriv (reverseTimeField b) r y‖ ≤ B

theorem AVenhance.Infra.Section5.RelativeError.inverseFlow_derivative_vecNormSq_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Flow.SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (hdiv : ∀ (t : ℝ) (x : Homogenization.Vec 2), vecDiv (b t) x = 0) {B : ℝ} (hDb : ∀ (r : ℝ) (y : Homogenization.Vec 2), ‖Flow.jointSpatialFDeriv b r y‖ ≤ B) {s t : ℝ} (hst : t ≤ s) (x v : Homogenization.Vec 2) : Homogenization.vecNormSq ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) v) ≤ Homogenization.vecNormSq v * Real.exp (2 * B * (s - t))

The inverse-flow spatial derivative has the same Euclidean energy bound as the forward derivative.