Finite Integral Balance for Paired Arrays

This is a finite-sum bookkeeping lemma for integrable scalar arrays.

Let $n\in\mathbb N$, let $A,B,C,D:(\operatorname{Fin} n)^2\times\mathbb R^n\to\mathbb R$, and let $F:\mathbb R^n\to\mathbb R$. Assume that every component of $A,B,C,D$ and $F$ is integrable with respect to Lebesgue measure on EuclideanSpace ℝ (Fin n). Assume also:

1. For every $a,b\in\operatorname{Fin} n$, the integrals of $A_{ab}+B_{ab}$ and $C_{ab}+D_{ab}$ agree.
2. The integral of the finite sum of the $D_{ab}$ equals minus the integral of $F$.

Then the integral of the finite sum of the $B_{ab}$ equals the negative of the integral of $F-\sum_{a,b}C_{ab}+\sum_{a,b}A_{ab}$:

This lemma packages finite summation and linearity of the integral for one subsequent flux identity.

Original Lean declaration header

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

private theorem integral_array_pair_balance {n : ℕ}
    (A B C D : Fin n → Fin n → EuclideanSpace ℝ (Fin n) → ℝ)
    (F : EuclideanSpace ℝ (Fin n) → ℝ)
    (hA : ∀ a b, Integrable (A a b) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hB : ∀ a b, Integrable (B a b) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hC : ∀ a b, Integrable (C a b) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hD : ∀ a b, Integrable (D a b) (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hF : Integrable F (volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hPair : ∀ a b,
      (∫ x, A a b x + B a b x ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
        ∫ x, C a b x + D a b x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))
    (hTrace : (∫ x, ∑ a : Fin n, ∑ b : Fin n, D a b x
        ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
      -(∫ x, F x ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))) :
    (∫ x, ∑ a : Fin n, ∑ b : Fin n, B a b x
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n)))) =
    -(∫ x, F x - (∑ a : Fin n, ∑ b : Fin n, C a b x) +
      ∑ a : Fin n, ∑ b : Fin n, A a b x
      ∂(volume : Measure (EuclideanSpace ℝ (Fin n))))

Module navigation

Module: Analysis/BakryEmery/IntegrationByParts/WeakHessianEvolution.

Previous: localLp_hessian_flux_trace_forcing · Next: integral_weak_hessian_flux_eq_trace_derivative.

Source excerpt, lines 563–581 · Frozen source 408915f.