Coordinate Trace Contraction Identity

This auxiliary statement performs a finite trace contraction of coordinatewise integral identities.

Let d,n,m be natural numbers. On $E=\operatorname{EuclideanSpace}\,\mathbb R\,(\operatorname{Fin} d)$, let B be an n-by-n matrix; let H and E be matrix fields; let T and J be m-indexed matrix fields; let ρ and ψ be scalar fields; and let dψₐ be scalar coordinate derivatives. Assume the five families of coordinate expressions appearing in the theorem are integrable, including the pairings involving J, T, H, E, B, ρ, ψ, and dψ. Assume also that for every l,k,i,j,

Then the contracted flux identity holds:

This is a finite-sum and trace-algebra support lemma used by the public weak trace contraction theorem.

Formalization Note All integrals are with respect to the explicitly supplied measure μ; no analytic interpretation of the fields as Hessians or derivatives is assumed.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis. Shown in its original module context. Proof omitted.

private theorem integral_trace_contraction_of_coordinate_pairings {d n m : ℕ}
    (mu : Measure (EuclideanSpace ℝ (Fin d)))
    (B : Matrix (Fin n) (Fin n) ℝ)
    (H E : EuclideanSpace ℝ (Fin d) → Matrix (Fin n) (Fin n) ℝ)
    (T J : EuclideanSpace ℝ (Fin d) → Fin m → Matrix (Fin n) (Fin n) ℝ)
    (rho psi : EuclideanSpace ℝ (Fin d) → ℝ)
    (dpsi : Fin m → EuclideanSpace ℝ (Fin d) → ℝ)
    (hPair : ∀ l k i j : Fin n, Integrable (fun x => rho x *
      (∑ a : Fin m, J x a i j * (psi x * T x a l k + dpsi a x * H x l k))) mu)
    (hForce : ∀ l k i j : Fin n, Integrable
      (fun x => rho x * E x i j * (psi x * H x l k)) mu)
    (hTensor : ∀ a : Fin m, Integrable
      (fun x => rho x * psi x * (2 * (B * T x a * B * J x a).trace)) mu)
    (hFlux : ∀ a : Fin m, Integrable
      (fun x => rho x * dpsi a x * (2 * (B * H x * B * J x a).trace)) mu)
    (hTraceForce : Integrable
      (fun x => rho x * psi x * (2 * (B * H x * B * E x).trace)) mu)
    (hTest : ∀ l k i j : Fin n,
      (∫ x, rho x * (∑ a : Fin m, J x a i j *
        (psi x * T x a l k + dpsi a x * H x l k)) ∂mu) =
      -(∫ x, rho x * E x i j * (psi x * H x l k) ∂mu)) :
    (∫ x, rho x * (∑ a : Fin m, (2 * (B * H x * B * J x a).trace) * dpsi a x) ∂mu) =
      -(∫ x, rho x *
        (2 * (B * H x * B * E x).trace +
          ∑ a : Fin m, 2 * (B * T x a * B * J x a).trace) * psi x ∂mu)

Module navigation

Module: Analysis/Matrix/WeakTrace.

Supporting theorems: trace_mul_mul_mul_eq_sum.

Next: integral_trace_quadratic_flux_eq_neg_density.

Source excerpt, lines 48–72 · Frozen source 408915f.