PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.IntegrationByParts

Imports

/-
Copyright (c) 2026 Juan Jose Fernandez Morales. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Juan Jose Fernandez Morales
-/
module

public import PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support

First variation integration by parts

i. Overview

This module contains the repeated integration-by-parts step needed for the local first-variation formula, together with the termwise and summed packaged versions used later in the Euler-Lagrange criterion.

ii. Key results

ClassicalFieldTheory.Local.integral_mul_iteratedDeriv_eq_sign

ClassicalFieldTheory.Local.hasTermwiseIntegratedByPartsFormula_of_regular

ClassicalFieldTheory.Local.hasIntegratedByPartsFormula_of_termwise

iii. Table of contents

A. Repeated integration by parts

B. Termwise formulas

iv. References

J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, Chapter 5, Theorem 5.2.

@[expose] public section

A. Repeated integration by parts

The integration-by-parts step sending the linearized density to the Euler-Lagrange pairing.

def HasIntegratedByPartsFormula (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop :=
  ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)),
    ∫ x, firstVariationDensity L f η x = firstVariationValue L f η

Termwise integration-by-parts data for the linearized first-variation density.

def HasTermwiseIntegratedByPartsFormula (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop :=
  ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)),
    ∀ I : DerivativeIndex d k, ∀ a : Fin m,
    Integrable (firstVariationDensityTerm L f η I a) ∧
    Integrable (fun x => eulerLagrangeTerm L I a f x * (η x) a) ∧
    (∫ x, firstVariationDensityTerm L f η I a x)
      = ∫ x, eulerLagrangeTerm L I a f x * (η x) a



private lemma integral_mul_space_deriv_eq_neg_deriv_mul (i : Fin d) {g h : Space d → ℝ}
    (hg : ContDiff ℝ ∞ g) (hh : IsTestFunction h) :
    ∫ x, g x * ∂[i] h x = ∫ x, (-∂[i] g x) * h x := byd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * Space.deriv i h x = ∫ (x : Space d), -Space.deriv i g x * h x
  rw [Space.deriv_eq_fderiv_fun,d:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fun x => (fderiv ℝ (fun x => h x) x) (Space.basis i)) x =
  ∫ (x : Space d), -Space.deriv i g x * h xd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fun x => (fderiv ℝ (fun x => h x) x) (Space.basis i)) x =
  ∫ (x : Space d), -(fun x => (fderiv ℝ (fun x => g x) x) (Space.basis i)) x * h x Space.deriv_eq_fderiv_fund:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fun x => (fderiv ℝ (fun x => h x) x) (Space.basis i)) x =
  ∫ (x : Space d), -(fun x => (fderiv ℝ (fun x => g x) x) (Space.basis i)) x * h xd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fun x => (fderiv ℝ (fun x => h x) x) (Space.basis i)) x =
  ∫ (x : Space d), -(fun x => (fderiv ℝ (fun x => g x) x) (Space.basis i)) x * h x]d:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fun x => (fderiv ℝ (fun x => h x) x) (Space.basis i)) x =
  ∫ (x : Space d), -(fun x => (fderiv ℝ (fun x => g x) x) (Space.basis i)) x * h x
  calc
    ∫ x, g x * fderiv ℝ h x (Space.basis i)
      = -∫ x, fderiv ℝ g x (Space.basis i) * h x := byd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * (fderiv ℝ h x) (Space.basis i) = -∫ (x : Space d), (fderiv ℝ g x) (Space.basis i) * h x
          rw [integral_mul_fderiv_eq_neg_fderiv_mul_of_integrabled:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ -∫ (x : Space d), (fderiv ℝ g x) (Space.basis i) * h x = -∫ (x : Space d), (fderiv ℝ g x) (Space.basis i) * h xhf'gd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => (fderiv ℝ g x) (Space.basis i) * h x) volumehfg'd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * (fderiv ℝ h x) (Space.basis i)) volumehfgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * h x) volumehfd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport h, DifferentiableAt ℝ g xhgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ h xhf'gd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => (fderiv ℝ g x) (Space.basis i) * h x) volumehfg'd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * (fderiv ℝ h x) (Space.basis i)) volumehfgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * h x) volumehfd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport h, DifferentiableAt ℝ g xhgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ h x]hf'gd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => (fderiv ℝ g x) (Space.basis i) * h x) volumehfg'd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * (fderiv ℝ h x) (Space.basis i)) volumehfgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * h x) volumehfd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport h, DifferentiableAt ℝ g xhgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ h x
          ·hf'gd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => (fderiv ℝ g x) (Space.basis i) * h x) volume simpa [Space.deriv_eq_fderiv_basis] using
              (IsTestFunction.integrable (μ := volume) <|
                IsTestFunction.mul_left (contDiff_space_deriv hg i) hh)All goals completed! 🐙
          ·hfg'd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * (fderiv ℝ h x) (Space.basis i)) volume simpa [Space.deriv_eq_fderiv_basis] using
              (IsTestFunction.integrable (μ := volume) <|
                IsTestFunction.mul_left hg (isTestFunction_space_deriv hh i))All goals completed! 🐙
          ·hfgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => g x * h x) volume exact IsTestFunction.integrable (μ := volume) <| IsTestFunction.mul_left hg hhAll goals completed! 🐙
          ·hfd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport h, DifferentiableAt ℝ g x intro x hxhfd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hx:Space dhx:x ∈ tsupport h⊢ DifferentiableAt ℝ g x
            exact Differentiable.differentiableAt (hg.differentiable (byd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hx:Space dhx:x ∈ tsupport h⊢ ∞ ≠ 0 simpAll goals completed! 🐙))
          ·hgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∀ x ∈ tsupport g, DifferentiableAt ℝ h x intro x hxhgd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hx:Space dhx:x ∈ tsupport g⊢ DifferentiableAt ℝ h x
            exact Differentiable.differentiableAt hh.differentiableAll goals completed! 🐙
    _ = ∫ x, (-fderiv ℝ g x (Space.basis i)) * h x := byd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ -∫ (x : Space d), (fderiv ℝ g x) (Space.basis i) * h x = ∫ (x : Space d), -(fderiv ℝ g x) (Space.basis i) * h x
          rw [← integral_negd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (a : Space d), -((fderiv ℝ g a) (Space.basis i) * h a) = ∫ (x : Space d), -(fderiv ℝ g x) (Space.basis i) * h xd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (a : Space d), -((fderiv ℝ g a) (Space.basis i) * h a) = ∫ (x : Space d), -(fderiv ℝ g x) (Space.basis i) * h x]d:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (a : Space d), -((fderiv ℝ g a) (Space.basis i) * h a) = ∫ (x : Space d), -(fderiv ℝ g x) (Space.basis i) * h x
          congr with xe_fd:ℕi:Fin dg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hx:Space d⊢ -((fderiv ℝ g x) (Space.basis i) * h x) = -(fderiv ℝ g x) (Space.basis i) * h x
          ringAll goals completed! 🐙



private lemma integral_mul_iteratedDerivList_eq_sign (L : List (Fin d)) {g h : Space d → ℝ}
    (hg : ContDiff ℝ ∞ g) (hh : IsTestFunction h) :
    ∫ x, g x * L.foldr (fun i f => ∂[i] f) h x =
      ∫ x, (((-1 : ℝ) ^ L.length) * L.foldr (fun i f => ∂[i] f) g x) * h x := byd:ℕL:List (Fin d)g:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
  ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h x
  induction L generalizing g h with
  | nil =>nild:ℕg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h [] x =
  ∫ (x : Space d), (-1) ^ [].length * List.foldr (fun i f => Space.deriv i f) g [] x * h x
      simpAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h x
      have hdg : ContDiff ℝ ∞ (∂[i] g) := byd:ℕL:List (Fin d)g:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
  ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h x
        exact contDiff_space_deriv hg iconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h xconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h x
      have hhL : IsTestFunction (L.foldr (fun j f => ∂[j] f) h) := byd:ℕL:List (Fin d)g:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
  ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h x
        exact iteratedDerivList_isTestFunction L hhconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h xconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h (i :: L) x =
  ∫ (x : Space d), (-1) ^ (i :: L).length * List.foldr (fun i f => Space.deriv i f) g (i :: L) x * h x
      calc
        ∫ x, g x * ∂[i] (L.foldr (fun j f => ∂[j] f) h) x
          = ∫ x, (-∂[i] g x) * L.foldr (fun j f => ∂[j] f) h x := byd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), g x * Space.deriv i (List.foldr (fun j f => Space.deriv j f) h L) x =
  ∫ (x : Space d), -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x
              exact integral_mul_space_deriv_eq_neg_deriv_mul i hg hhLAll goals completed! 🐙
        _ = -∫ x, ∂[i] g x * L.foldr (fun j f => ∂[j] f) h x := byd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  -∫ (x : Space d), Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x
              rw [← integral_negd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  ∫ (a : Space d), -(Space.deriv i g a * List.foldr (fun j f => Space.deriv j f) h L a)d:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  ∫ (a : Space d), -(Space.deriv i g a * List.foldr (fun j f => Space.deriv j f) h L a)]d:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (x : Space d), -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  ∫ (a : Space d), -(Space.deriv i g a * List.foldr (fun j f => Space.deriv j f) h L a)
              congr with xe_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  -(Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x)
              ringAll goals completed! 🐙
        _ = -∫ x, (((-1 : ℝ) ^ L.length) *
            L.foldr (fun j f => ∂[j] f) (∂[i] g) x) * h x := byd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ -∫ (x : Space d), Space.deriv i g x * List.foldr (fun j f => Space.deriv j f) h L x =
  -∫ (x : Space d), (-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L x * h x
              rw [ih hdg hhd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ -∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) (Space.deriv i g) L x * h x =
  -∫ (x : Space d), (-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L x * h xAll goals completed! 🐙]All goals completed! 🐙
        _ = ∫ x, (((-1 : ℝ) ^ (L.length + 1)) *
            ∂[i] (L.foldr (fun j f => ∂[j] f) g) x) * h x := byd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ -∫ (x : Space d), (-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L x * h x =
  ∫ (x : Space d), (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x
              rw [← integral_negd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (a : Space d), -((-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L a * h a) =
  ∫ (x : Space d), (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h xd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (a : Space d), -((-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L a * h a) =
  ∫ (x : Space d), (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x]d:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)⊢ ∫ (a : Space d), -((-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L a * h a) =
  ∫ (x : Space d), (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x
              congr with xe_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * List.foldr (fun j f => Space.deriv j f) (Space.deriv i g) L x * h x) =
  (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x
              rw [iteratedDerivList_commute_deriv L i hg,e_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x) =
  (-1) ^ (L.length + 1) * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h xe_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x)) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x pow_succ,e_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h xe_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x)) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x mul_assoce_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x)) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h xe_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x)) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x]e_fd:ℕi:Fin dL:List (Fin d)ih:∀ {g h : Space d → ℝ},
  ContDiff ℝ ∞ g →
    IsTestFunction h →
      ∫ (x : Space d), g x * List.foldr (fun i f => Space.deriv i f) h L x =
        ∫ (x : Space d), (-1) ^ L.length * List.foldr (fun i f => Space.deriv i f) g L x * h xg:Space d → ℝh:Space d → ℝhg:ContDiff ℝ ∞ ghh:IsTestFunction hhdg:ContDiff ℝ ∞ (Space.deriv i g)hhL:IsTestFunction (List.foldr (fun j f => Space.deriv j f) h L)x:Space d⊢ -((-1) ^ L.length * (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L) x * h x)) =
  (-1) ^ L.length * -1 * Space.deriv i (List.foldr (fun j f => Space.deriv j f) g L) x * h x
              ringAll goals completed! 🐙

Repeated integration by parts for iterated coordinate derivatives against a test function.

lemma integral_mul_iteratedDeriv_eq_sign {g h : Space d → ℝ} (I : MultiIndex d)
    (hg : ContDiff ℝ ∞ g) (hh : IsTestFunction h) :
    ∫ x, g x * ∂^[I] h x =
      ∫ x, (((-1 : ℝ) ^ I.order) * ∂^[I] g x) * h x := byd:ℕg:Space d → ℝh:Space d → ℝI:MultiIndex dhg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), g x * Space.iteratedDeriv I h x = ∫ (x : Space d), (-1) ^ I.order * Space.iteratedDeriv I g x * h x
  simpa [Space.iteratedDeriv, Physlib.MultiIndex.length_toList] using
    integral_mul_iteratedDerivList_eq_sign I.toList hg hhAll goals completed! 🐙

B. Termwise formulas

Concrete termwise integration by parts for the first-variation density, assuming the jet coordinate coefficient functions are smooth along the field.


lemma hasTermwiseIntegratedByPartsFormula_of_contDiff_coordDeriv
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (hcoeff : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      ContDiff ℝ ∞ (fun x => L.coordDeriv I a (jetAt k f x))) :
    HasTermwiseIntegratedByPartsFormula L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)⊢ HasTermwiseIntegratedByPartsFormula L f
  intro η I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin m⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  let g : Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  let h : Space d → ℝ := fun x => (η.toFun x) ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp a⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  have hg : ContDiff ℝ ∞ g := hcoeff I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ g⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  have hh : IsTestFunction h := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)⊢ HasTermwiseIntegratedByPartsFormula L fd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
    simpa [h] using η.coord_euclidean ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (firstVariationDensityTerm L f η I a) volume ∧
  Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
    ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
      ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  constructorleftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (firstVariationDensityTerm L f η I a) volumerightd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume ∧
  ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
    ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  ·leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (firstVariationDensityTerm L f η I a) volume simpa [g, h, firstVariationDensityTerm, Space.iteratedDeriv] using
      firstVariationDensityTerm_integrable_of_continuous_coordDeriv L f η I a hg.continuousAll goals completed! 🐙
  constructorright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volumeright.rightd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
  ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
  ·right.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume have htd : ContDiff ℝ ∞ (∂^[I.1] g) :=
      Space.iteratedDeriv_contDiff I.1 hgright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume
    have htdSign : ContDiff ℝ ∞
        (fun x => ((-1 : ℝ) ^ I.1.order) * ∂^[I.1] g x) := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)⊢ HasTermwiseIntegratedByPartsFormula L fright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume
      apply ContDiff.mulhfd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)⊢ ContDiff ℝ ∞ fun x => (-1) ^ (↑I).orderhgd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)⊢ ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)right.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume
      ·hfd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)⊢ ContDiff ℝ ∞ fun x => (-1) ^ (↑I).orderright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume fun_propAll goals completed! 🐙right.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume
      ·hgd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)⊢ ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)right.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume exact htdright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volumeright.leftd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction hhtd:ContDiff ℝ ∞ (Space.iteratedDeriv (↑I) g)htdSign:ContDiff ℝ ∞ fun x => (-1) ^ (↑I).order * Space.iteratedDeriv (↑I) g x⊢ Integrable (fun x => eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a) volume
    exact
      (IsTestFunction.integrable (μ := volume) <|
        IsTestFunction.mul_left htdSign hh)All goals completed! 🐙
  ·right.rightd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:∀ (I : DerivativeIndex d k) (a : Fin m), ContDiff ℝ ∞ fun x => L.coordDeriv I a (jetAt k f x)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mg:Space d → ℝ := fun x => L.coordDeriv I a (jetAt k f x)h:Space d → ℝ := fun x => (η.toFun x).ofLp ahg:ContDiff ℝ ∞ ghh:IsTestFunction h⊢ ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
  ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a exact
      integral_mul_iteratedDeriv_eq_sign I.1 hg hhAll goals completed! 🐙

              lemma hasTermwiseIntegratedByPartsFormula_of_regular
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (hcoeff : Lagrangian.ContDiffCoordDerivAlongField L f) :
    HasTermwiseIntegratedByPartsFormula L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hcoeff:L.ContDiffCoordDerivAlongField f⊢ HasTermwiseIntegratedByPartsFormula L f
  exact hasTermwiseIntegratedByPartsFormula_of_contDiff_coordDeriv L f hcoeffAll goals completed! 🐙

private lemma integral_firstVariationDensity_eq_termwise_sum
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (hterm : HasTermwiseIntegratedByPartsFormula L f) :
    ∫ x, firstVariationDensity L f η x =
      ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        ∫ x, firstVariationDensityTerm L f η I a x := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), firstVariationDensity L f η x = ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x
  calc
    ∫ x, firstVariationDensity L f η x
      = ∫ x, ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        firstVariationDensityTerm L f η I a x := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), firstVariationDensity L f η x = ∫ (x : Space d), ∑ I, ∑ a, firstVariationDensityTerm L f η I a x
          rflAll goals completed! 🐙
    _ = ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        ∫ x, firstVariationDensityTerm L f η I a x := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), ∑ I, ∑ a, firstVariationDensityTerm L f η I a x =
  ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x
          rw [MeasureTheory.integral_finsetSum Finset.univ
            (fun I _ => integrable_finsetSum Finset.univ (fun a _ => (hterm η I a).1))d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ i, ∫ (a : Space d), ∑ i_1, firstVariationDensityTerm L f η i i_1 a ∂volume =
  ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ i, ∫ (a : Space d), ∑ i_1, firstVariationDensityTerm L f η i i_1 a ∂volume =
  ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ i, ∫ (a : Space d), ∑ i_1, firstVariationDensityTerm L f η i i_1 a ∂volume =
  ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x
          apply Finset.sum_congr rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∀ x ∈ Finset.univ,
  ∫ (a : Space d), ∑ i, firstVariationDensityTerm L f η x i a ∂volume =
    ∑ a, ∫ (x_1 : Space d), firstVariationDensityTerm L f η x a x_1
          intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∫ (a : Space d), ∑ i, firstVariationDensityTerm L f η I i a ∂volume =
  ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x
          rw [MeasureTheory.integral_finsetSum Finset.univ (fun a _ => (hterm η I a).1)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∑ i, ∫ (a : Space d), firstVariationDensityTerm L f η I i a ∂volume =
  ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a xAll goals completed! 🐙]All goals completed! 🐙

private lemma integral_eulerLagrange_termwise_sum_eq_pairing
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (hterm : HasTermwiseIntegratedByPartsFormula L f) :
    ∑ I : DerivativeIndex d k, ∑ a : Fin m, ∫ x, eulerLagrangeTerm L I a f x * (η x) a
      = firstVariationValue L f η := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ I, ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = firstVariationValue L f η
  calc
    ∑ I : DerivativeIndex d k, ∑ a : Fin m, ∫ x, eulerLagrangeTerm L I a f x * (η x) a
      = ∫ x, ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        eulerLagrangeTerm L I a f x * (η x) a := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ I, ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∫ (x : Space d), ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
          calc
            ∑ I : DerivativeIndex d k, ∑ a : Fin m,
                ∫ x, eulerLagrangeTerm L I a f x * (η x) a
              =
                ∑ I : DerivativeIndex d k,
                  ∫ x, ∑ a : Fin m, eulerLagrangeTerm L I a f x * (η x) a := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ I, ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∑ I, ∫ (x : Space d), ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
                  apply Finset.sum_congr rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∀ x ∈ Finset.univ,
  ∑ a, ∫ (x_1 : Space d), eulerLagrangeTerm L x a f x_1 * (η.toFun x_1).ofLp a =
    ∫ (x_1 : Space d), ∑ a, eulerLagrangeTerm L x a f x_1 * (η.toFun x_1).ofLp a
                  intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∫ (x : Space d), ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
                  rw [← MeasureTheory.integral_finsetSum Finset.univ
                    (fun a _ => (hterm η I a).2.1)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∫ (a : Space d), ∑ i, eulerLagrangeTerm L I i f a * (η.toFun a).ofLp i ∂volume =
  ∫ (x : Space d), ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp aAll goals completed! 🐙]All goals completed! 🐙
            _ =
                ∫ x, ∑ I : DerivativeIndex d k,
                  ∑ a : Fin m, eulerLagrangeTerm L I a f x * (η x) a := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∑ I, ∫ (x : Space d), ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∫ (x : Space d), ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
                  rw [← MeasureTheory.integral_finsetSum Finset.univ
                    (fun I _ => integrable_finsetSum Finset.univ (fun a _ => (hterm η I a).2.1))d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (a : Space d), ∑ i, ∑ i_1, eulerLagrangeTerm L i i_1 f a * (η.toFun a).ofLp i_1 ∂volume =
  ∫ (x : Space d), ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp aAll goals completed! 🐙]All goals completed! 🐙
    _ = ∫ x, ⟪eulerLagrangeOp L f x, η x⟫_ℝ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∫ (x : Space d), ⟪eulerLagrangeOp L f x, η.toFun x⟫_ℝ
          apply integral_congr_aed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ (fun a => ∑ I, ∑ a_1, eulerLagrangeTerm L I a_1 f a * (η.toFun a).ofLp a_1) =ᵐ[volume] fun a =>
  ⟪eulerLagrangeOp L f a, η.toFun a⟫_ℝ
          filter_upwards with xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = ⟪eulerLagrangeOp L f x, η.toFun x⟫_ℝ
          rw [PiLp.inner_applyd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = ∑ i, ⟪(eulerLagrangeOp L f x).ofLp i, (η.toFun x).ofLp i⟫_ℝd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = ∑ i, ⟪(eulerLagrangeOp L f x).ofLp i, (η.toFun x).ofLp i⟫_ℝ]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = ∑ i, ⟪(eulerLagrangeOp L f x).ofLp i, (η.toFun x).ofLp i⟫_ℝ
          simp_rw [d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = ∑ i, ⟪(eulerLagrangeOp L f x).ofLp i, (η.toFun x).ofLp i⟫_ℝeulerLagrangeOp_apply,d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∑ x_1, ⟪eulerLagrangeComponent L x_1 f x, (η.toFun x).ofLp x_1⟫_ℝ eulerLagrangeComponent_applyd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∑ x_1, ⟪∑ I, eulerLagrangeTerm L I x_1 f x, (η.toFun x).ofLp x_1⟫_ℝ]
          rw [Finset.sum_commd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ y, ∑ x_1, eulerLagrangeTerm L x_1 y f x * (η.toFun x).ofLp y =
  ∑ x_1, ⟪∑ I, eulerLagrangeTerm L I x_1 f x, (η.toFun x).ofLp x_1⟫_ℝd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ y, ∑ x_1, eulerLagrangeTerm L x_1 y f x * (η.toFun x).ofLp y =
  ∑ x_1, ⟪∑ I, eulerLagrangeTerm L I x_1 f x, (η.toFun x).ofLp x_1⟫_ℝ]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∑ y, ∑ x_1, eulerLagrangeTerm L x_1 y f x * (η.toFun x).ofLp y =
  ∑ x_1, ⟪∑ I, eulerLagrangeTerm L I x_1 f x, (η.toFun x).ofLp x_1⟫_ℝ
          apply Finset.sum_congr rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space d⊢ ∀ x_1 ∈ Finset.univ,
  ∑ x_2, eulerLagrangeTerm L x_2 x_1 f x * (η.toFun x).ofLp x_1 =
    ⟪∑ I, eulerLagrangeTerm L I x_1 f x, (η.toFun x).ofLp x_1⟫_ℝ
          intro a _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ ∑ x_1, eulerLagrangeTerm L x_1 a f x * (η.toFun x).ofLp a = ⟪∑ I, eulerLagrangeTerm L I a f x, (η.toFun x).ofLp a⟫_ℝ
          rw [show ⟪∑ I : DerivativeIndex d k, eulerLagrangeTerm L I a f x,
              (η.toFun x).ofLp a⟫_ℝ =
              (∑ I : DerivativeIndex d k, eulerLagrangeTerm L I a f x) *
                (η.toFun x).ofLp a byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), ∑ I, ∑ a, eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a =
  ∫ (x : Space d), ⟪eulerLagrangeOp L f x, η.toFun x⟫_ℝd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ ∑ x_1, eulerLagrangeTerm L x_1 a f x * (η.toFun x).ofLp a = (∑ I, eulerLagrangeTerm L I a f x) * (η.toFun x).ofLp a
            norm_num [inner, Inner.inner]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ (η.toFun x).ofLp a *
    ∑ x_1, (-1) ^ (↑x_1).order * Space.iteratedDeriv (↑x_1) (fun x => L.coordDeriv x_1 a (jetAt k f x)) x =
  (∑ x_1, (-1) ^ (↑x_1).order * Space.iteratedDeriv (↑x_1) (fun x => L.coordDeriv x_1 a (jetAt k f x)) x) *
    (η.toFun x).ofLp ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ ∑ x_1, eulerLagrangeTerm L x_1 a f x * (η.toFun x).ofLp a = (∑ I, eulerLagrangeTerm L I a f x) * (η.toFun x).ofLp a
            ringAll goals completed! 🐙d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ ∑ x_1, eulerLagrangeTerm L x_1 a f x * (η.toFun x).ofLp a = (∑ I, eulerLagrangeTerm L I a f x) * (η.toFun x).ofLp a]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ ∑ x_1, eulerLagrangeTerm L x_1 a f x * (η.toFun x).ofLp a = (∑ I, eulerLagrangeTerm L I a f x) * (η.toFun x).ofLp a
          rw [← Finset.sum_muld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L fx:Space da:Fin ma✝:a ∈ Finset.univ⊢ (∑ i, eulerLagrangeTerm L i a f x) * (η.toFun x).ofLp a = (∑ I, eulerLagrangeTerm L I a f x) * (η.toFun x).ofLp aAll goals completed! 🐙]All goals completed! 🐙
    _ = firstVariationValue L f η := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hterm:HasTermwiseIntegratedByPartsFormula L f⊢ ∫ (x : Space d), ⟪eulerLagrangeOp L f x, η.toFun x⟫_ℝ = firstVariationValue L f η
          rflAll goals completed! 🐙lemma hasIntegratedByPartsFormula_of_termwise (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m))
    (hterm : HasTermwiseIntegratedByPartsFormula L f) :
    HasIntegratedByPartsFormula L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L f⊢ HasIntegratedByPartsFormula L f
  intro ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ ∫ (x : Space d), firstVariationDensity L f η x = firstVariationValue L f η
  calc
    ∫ x, firstVariationDensity L f η x
      = ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        ∫ x, firstVariationDensityTerm L f η I a x := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ ∫ (x : Space d), firstVariationDensity L f η x = ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x
          exact integral_firstVariationDensity_eq_termwise_sum L f η htermAll goals completed! 🐙
    _ = ∑ I : DerivativeIndex d k, ∑ a : Fin m,
        ∫ x, eulerLagrangeTerm L I a f x * (η x) a := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ ∑ I, ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
  ∑ I, ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
          apply Finset.sum_congr rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ ∀ x ∈ Finset.univ,
  ∑ a, ∫ (x_1 : Space d), firstVariationDensityTerm L f η x a x_1 =
    ∑ a, ∫ (x_1 : Space d), eulerLagrangeTerm L x a f x_1 * (η.toFun x_1).ofLp a
          intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∑ a, ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
  ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
          apply Finset.sum_congr rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∀ x ∈ Finset.univ,
  ∫ (x_1 : Space d), firstVariationDensityTerm L f η I x x_1 =
    ∫ (x_1 : Space d), eulerLagrangeTerm L I x f x_1 * (η.toFun x_1).ofLp x
          intro a _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka✝¹:I ∈ Finset.univa:Fin ma✝:a ∈ Finset.univ⊢ ∫ (x : Space d), firstVariationDensityTerm L f η I a x =
  ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a
          exact (hterm η I a).2.2All goals completed! 🐙
    _ = firstVariationValue L f η := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hterm:HasTermwiseIntegratedByPartsFormula L fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ ∑ I, ∑ a, ∫ (x : Space d), eulerLagrangeTerm L I a f x * (η.toFun x).ofLp a = firstVariationValue L f η
          exact integral_eulerLagrange_termwise_sum_eq_pairing L f η htermAll goals completed! 🐙