Gradient Matrix

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.FaaDiBruno.spatialGradientMatrix (f : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : Fin 2 → Fin 2 → ℝ

The matrix of first spatial partial derivatives, with output component as the first index and differentiation direction as the second.

Equations

• AVenhance.FaaDiBruno.spatialGradientMatrix f x i j = (fderiv ℝ f x) (AVenhance.FaaDiBruno.coordinateVector 2 j) i

noncomputable def AVenhance.FaaDiBruno.gradientMatrixOfCLM : (VecOne 2 →L[ℝ] Homogenization.Vec 2) →L[ℝ] Fin 2 → Fin 2 → ℝ

Evaluating a linear map on the two coordinate vectors and then taking its two output coordinates is a norm-nonincreasing map into the entrywise matrix norm.

Equations

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

theorem AVenhance.FaaDiBruno.gradientMatrixOfCLM_norm_le (A : VecOne 2 →L[ℝ] Homogenization.Vec 2) : ‖gradientMatrixOfCLM A‖ ≤ ‖A‖

theorem AVenhance.FaaDiBruno.gradientMatrixOfCLM_opNorm_le : ‖gradientMatrixOfCLM‖ ≤ 1

theorem AVenhance.FaaDiBruno.lift_spatialGradientMatrix_eq (f : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ 1 f) (z : VecOne 2) : liftVecOne (spatialGradientMatrix f) z = gradientMatrixOfCLM (fderiv ℝ (liftVecOne f) z)

Lifting the paper gradient matrix to the ℓ¹ coordinate realization agrees with evaluating the derivative of the lifted vector field on coordinate vectors.

theorem AVenhance.FaaDiBruno.spatialGradientMatrix_derivativeSup_le (f : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : derivativeSup n (spatialGradientMatrix f) ≤ derivativeSup (n + 1) f

The order-n derivative seminorm of the gradient matrix is bounded by the order-n+1 derivative seminorm of the underlying vector field.

theorem AVenhance.FaaDiBruno.GradientMatrix.one_add_nat_mul_le_pow {a : ℝ} (ha : 0 ≤ a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n

theorem AVenhance.FaaDiBruno.spatialGradientMatrix_snorm_le_of_nextOrder (f : Homogenization.Vec 2 → Homogenization.Vec 2) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) {C_f C_g R τ : ℝ} (hCf : 0 < C_f) (hCg : 0 ≤ C_g) (hR : 0 < R) (hτ : 0 ≤ τ) (hT : τ ≤ 1 / (8 * C_f * R)) (hnext : snorm f (n + 1) (R * (1 + 8 * τ * C_f * R)) ≤ ENNReal.ofReal (16 * C_g * τ)) : snorm (spatialGradientMatrix f) n (R * (1 + 8 * τ * C_f * R) ^ 2) ≤ ENNReal.ofReal (8 * C_g / C_f)

The all-order gradient seminorm estimate (10670), reduced to the corresponding order-n+1 transport estimate. This theorem is in the consumed equal-radius, dimension-two form.

theorem AVenhance.FaaDiBruno.GradientMatrix.derivativeSup_zero_eq_eLpNormEssSup {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) : derivativeSup 0 f = MeasureTheory.eLpNormEssSup f (vecVolume d)

theorem AVenhance.FaaDiBruno.GradientMatrix.snorm_zero_eq_derivativeSup {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Homogenization.Vec d → F) (R : ℝ) : snorm f 0 R = derivativeSup 0 f