Two-Slot Mixed Delta Collapse

This auxiliary lemma evaluates the mixed two-slot term arising from two matrix factors.

For a coordinate tensor $T$ and a real matrix $M$, the sum with two distinct slots and delta constraints equals

More explicitly, the left side is the finite sum over $J,K$ and $s,u$ whose factors are $T_JT_K$, the product of deltas outside $s$ and $u$, and $(-M_{J_uK_u})(-M_{J_sK_s})$. This is an internal identity used in the second derivative of the energy form.

Original Lean declaration header

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

private lemma two_slot_sum (T : (Fin r → Fin n) → ℝ) (M : Matrix (Fin n) (Fin n) ℝ) :
    (∑ J : Fin r → Fin n, ∑ K : Fin r → Fin n, T J * T K *
      (∑ s : Fin r, (∑ u ∈ Finset.univ.erase s,
        (∏ v ∈ (Finset.univ.erase s).erase u, if J v = K v then (1 : ℝ) else 0) *
          (-M (J u) (K u))) * (-M (J s) (K s)))) =
      ∑ s : Fin r, ∑ u ∈ Finset.univ.erase s, inner T (actOn M s (actOn M u T))

Module navigation

Module: Analysis/Tensor/EnergyForm.

Definition modules: Analysis/Tensor/SlotAction.

Supporting theorems: sum_mul_prod_delta_erase_erase.

Previous: slot_sum_two · Next: deriv_deriv_energyForm_line.

Source excerpt, lines 759–764 · Frozen source 408915f.