PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Density

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
public import Mathlib.Analysis.Calculus.ParametricIntegral

First variation density formulas

i. Overview

This module contains the pointwise and integral first-variation formulas before integration by parts: differentiation of the varied action density, dominated differentiation under the integral, and the corresponding packaged hypotheses.

ii. Key results

ClassicalFieldTheory.Local.hasPointwiseLinearizedDensityFormula_of_contDiff

ClassicalFieldTheory.Local.hasActionVariationDerivativeUnderIntegral_of_contDiff_of_regular

iii. Table of contents

A. Differentiation under the integral sign

B. Pointwise linearization

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. Differentiation under the integral sign

Differentiation of the varied action under the integral sign, packaged as a hypothesis.

def HasActionVariationDerivativeUnderIntegral (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m)) :
    Prop :=
  ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), HasFiniteActionVariation L f η →
    HasDerivAt (actionVariation L f η)
      (∫ x, deriv (fun s : ℝ => actionDensity L (variedField f η s) x) 0) 0

Pointwise linearization of the action density before integration by parts.

def HasPointwiseLinearizedDensityFormula (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m)) : Prop :=
  ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), ∀ x : Space d,
    deriv (fun s : ℝ => actionDensity L (variedField f η s) x) 0 =
      firstVariationDensity L f η x

A direct bridge from Mathlib's dominated differentiation-under-the-integral theorem to the local action variation. This isolates the measure-theoretic input needed to prove HasActionVariationDerivativeUnderIntegral.

lemma actionVariation_hasDerivAt_of_dominated_loc_of_deriv_le
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    {F' : ℝ → Space d → ℝ} {bound : Space d → ℝ} {ε : ℝ} (hε : 0 < ε)
    (hmeas :
      ∀ᶠ s in nhds (0 : ℝ),
        AEStronglyMeasurable (actionDensity L (variedField f η s)) volume)
    (hfinite0 : Integrable (actionDensity L (variedField f η 0)))
    (hF'_meas : AEStronglyMeasurable (F' 0) volume)
    (hbound :
      ∀ᵐ x ∂volume, ∀ s ∈ Metric.ball (0 : ℝ) ε, ‖F' s x‖ ≤ bound x)
    (hbound_int : Integrable bound volume)
    (hderiv :
      ∀ᵐ x ∂volume, ∀ s ∈ Metric.ball (0 : ℝ) ε,
        HasDerivAt (fun r : ℝ => actionDensity L (variedField f η r) x) (F' s x) s) :
    HasDerivAt (actionVariation L f η) (∫ x, F' 0 x) 0 := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))F':ℝ → Space d → ℝbound:Space d → ℝε:ℝhε:0 < εhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF'_meas:AEStronglyMeasurable (F' 0) volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖F' s x‖ ≤ bound xhbound_int:Integrable bound volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0
  have hs : Metric.ball (0 : ℝ) ε ∈ nhds (0 : ℝ) := Metric.ball_mem_nhds _ hεd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))F':ℝ → Space d → ℝbound:Space d → ℝε:ℝhε:0 < εhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF'_meas:AEStronglyMeasurable (F' 0) volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖F' s x‖ ≤ bound xhbound_int:Integrable bound volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shs:Metric.ball 0 ε ∈ nhds 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0
  exact
    (hasDerivAt_integral_of_dominated_loc_of_deriv_le
      (μ := volume) (F := fun s x => actionDensity L (variedField f η s) x)
      (x₀ := (0 : ℝ)) (s := Metric.ball (0 : ℝ) ε) hs
      hmeas hfinite0 hF'_meas hbound hbound_int hderiv).2All goals completed! 🐙

A dominated bound for the pointwise first variation along the varied-field family near s = 0. This packages the analytic domination needed to differentiate the action under the integral sign.

def HasDominatedVariationDerivativeNear (L : Lagrangian d m k)
    (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) : Prop :=
  ∃ ε > 0, ∃ bound : Space d → ℝ,
    AEStronglyMeasurable (firstVariationDensity L f η) volume ∧
    Integrable bound volume ∧
    ∀ᵐ x ∂volume, ∀ s ∈ Metric.ball (0 : ℝ) ε,
      ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x

              

private lemma continuous_coordDeriv_at_zero
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (hcont : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      Continuous (fun p : ℝ × Space d =>
        L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)))
    (I : DerivativeIndex d k) (a : Fin m) :
    Continuous (fun x : Space d => L.coordDeriv I a (jetAt k f x)) := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)I:DerivativeIndex d ka:Fin m⊢ Continuous fun x => L.coordDeriv I a (jetAt k f x)
  have hpair : Continuous (fun x : Space d => ((0 : ℝ), x)) := by
    fun_propd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)I:DerivativeIndex d ka:Fin mhpair:Continuous fun x => (0, x)⊢ Continuous fun x => L.coordDeriv I a (jetAt k f x)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)I:DerivativeIndex d ka:Fin mhpair:Continuous fun x => (0, x)⊢ Continuous fun x => L.coordDeriv I a (jetAt k f x)
  have hcoeff0 :
      Continuous (fun x : Space d => L.coordDeriv I a (jetAt k (variedField f η 0) x)) := by
    exact (hcont I a).comp hpaird:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)I:DerivativeIndex d ka:Fin mhpair:Continuous fun x => (0, x)hcoeff0:Continuous fun x => L.coordDeriv I a (jetAt k (variedField f η 0) x)⊢ Continuous fun x => L.coordDeriv I a (jetAt k f x)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)I:DerivativeIndex d ka:Fin mhpair:Continuous fun x => (0, x)hcoeff0:Continuous fun x => L.coordDeriv I a (jetAt k (variedField f η 0) x)⊢ Continuous fun x => L.coordDeriv I a (jetAt k f x)
  simpa [variedField_zero] using hcoeff0All goals completed! 🐙

private lemma firstVariationDensityTerm_norm_le_of_coeff_bound
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (ψ : DerivativeIndex d k → Fin m → Space d → ℝ)
    (hψ : ∀ I : DerivativeIndex d k, ∀ a : Fin m, ∀ x : Space d,
      ψ I a x = ∂^[I.1] (fun y => (η y) a) x)
    (C : DerivativeIndex d k → Fin m → ℝ)
    (K : DerivativeIndex d k → Fin m → Set (Space d))
    (hKzero : ∀ I : DerivativeIndex d k, ∀ a : Fin m, ∀ x, x ∉ K I a → ψ I a x = 0)
    (hC : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      ∀ p ∈ Metric.closedBall (0 : ℝ) 1 ×ˢ K I a,
        ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a)
    {x : Space d} {s : ℝ} (hs : s ∈ Metric.ball (0 : ℝ) 1)
    (I : DerivativeIndex d k) (a : Fin m) :
    ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin m⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
  by_cases hx : x ∈ K I aposd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖negd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
  ·posd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖ have hs' : s ∈ Metric.closedBall (0 : ℝ) 1 := Metric.ball_subset_closedBall hsposd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
    have hcoeff := hC I a (s, x) ⟨hs', hx⟩posd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
    calc
      ‖firstVariationDensityTerm L (variedField f η s) η I a x‖
        = ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ = ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * ψ I a x‖
            rw [hψ I a xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ =
  ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ =
  ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ =
  ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖
            simp [firstVariationDensityTerm]All goals completed! 🐙
      _ = ‖L.coordDeriv I a (jetAt k (variedField f η s) x)‖ * ‖ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖L.coordDeriv I a (jetAt k (variedField f η s) x) * ψ I a x‖ =
  ‖L.coordDeriv I a (jetAt k (variedField f η s) x)‖ * ‖ψ I a x‖
            rw [norm_muld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖L.coordDeriv I a (jetAt k (variedField f η s) x)‖ * ‖ψ I a x‖ =
  ‖L.coordDeriv I a (jetAt k (variedField f η s) x)‖ * ‖ψ I a x‖All goals completed! 🐙]All goals completed! 🐙
      _ ≤ C I a * ‖ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∈ K I ahs':s ∈ Metric.closedBall 0 1hcoeff:‖L.coordDeriv I a (jetAt k (variedField f η (s, x).1) (s, x).2)‖ ≤ C I a⊢ ‖L.coordDeriv I a (jetAt k (variedField f η s) x)‖ * ‖ψ I a x‖ ≤ C I a * ‖ψ I a x‖
            exact mul_le_mul_of_nonneg_right hcoeff (norm_nonneg _)All goals completed! 🐙
  ·negd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I a⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖ have hψzero : ψ I a x = 0 := hKzero I a x hxnegd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:ψ I a x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
    rw [hψ I a xnegd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖negd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖] at hψzeronegd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
    rw [hψ I a xnegd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  C I a * ‖Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖negd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  C I a * ‖Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖]negd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1I:DerivativeIndex d ka:Fin mhx:x ∉ K I ahψzero:Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x = 0⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  C I a * ‖Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x‖
    simp [firstVariationDensityTerm, hψzero]All goals completed! 🐙

private lemma norm_firstVariationDensity_le_bound
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (ψ : DerivativeIndex d k → Fin m → Space d → ℝ)
    (hψ : ∀ I : DerivativeIndex d k, ∀ a : Fin m, ∀ x : Space d,
      ψ I a x = ∂^[I.1] (fun y => (η y) a) x)
    (C : DerivativeIndex d k → Fin m → ℝ)
    (K : DerivativeIndex d k → Fin m → Set (Space d))
    (hKzero : ∀ I : DerivativeIndex d k, ∀ a : Fin m, ∀ x, x ∉ K I a → ψ I a x = 0)
    (hC : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      ∀ p ∈ Metric.closedBall (0 : ℝ) 1 ×ˢ K I a,
        ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a)
    {x : Space d} {s : ℝ} (hs : s ∈ Metric.ball (0 : ℝ) 1) :
    ‖firstVariationDensity L (variedField f η s) η x‖
      ≤ ∑ I : DerivativeIndex d k, ∑ a : Fin m, C I a * ‖ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1⊢ ‖firstVariationDensity L (variedField f η s) η x‖ ≤ ∑ I, ∑ a, C I a * ‖ψ I a x‖
  have houter :
      ‖∑ I : DerivativeIndex d k, ∑ a : Fin m,
          firstVariationDensityTerm L (variedField f η s) η I a x‖
        ≤ ∑ I : DerivativeIndex d k, ‖∑ a : Fin m,
            firstVariationDensityTerm L (variedField f η s) η I a x‖ := by
    exact norm_sum_le _ _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ‖firstVariationDensity L (variedField f η s) η x‖ ≤ ∑ I, ∑ a, C I a * ‖ψ I a x‖d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ‖firstVariationDensity L (variedField f η s) η x‖ ≤ ∑ I, ∑ a, C I a * ‖ψ I a x‖
  calc
    ‖firstVariationDensity L (variedField f η s) η x‖
      = ‖∑ I : DerivativeIndex d k, ∑ a : Fin m,
          firstVariationDensityTerm L (variedField f η s) η I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ‖firstVariationDensity L (variedField f η s) η x‖ = ‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖
            simp [firstVariationDensity]All goals completed! 🐙
    _ ≤ ∑ I : DerivativeIndex d k, ‖∑ a : Fin m,
          firstVariationDensityTerm L (variedField f η s) η I a x‖ := houter
    _ ≤ ∑ I : DerivativeIndex d k, ∑ a : Fin m,
          ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η I a x‖
            refine Finset.sum_le_sum ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ∀ i ∈ Finset.univ,
  ‖∑ a, firstVariationDensityTerm L (variedField f η s) η i a x‖ ≤
    ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η i a x‖
            intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η I a x‖
            exact norm_sum_le _ _All goals completed! 🐙
    _ ≤ ∑ I : DerivativeIndex d k, ∑ a : Fin m, C I a * ‖ψ I a x‖ := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ∑ I, ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ ∑ I, ∑ a, C I a * ‖ψ I a x‖
            refine Finset.sum_le_sum ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖⊢ ∀ i ∈ Finset.univ, ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η i a x‖ ≤ ∑ a, C i a * ‖ψ i a x‖
            intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∑ a, ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ ∑ a, C I a * ‖ψ I a x‖
            refine Finset.sum_le_sum ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∀ i ∈ Finset.univ, ‖firstVariationDensityTerm L (variedField f η s) η I i x‖ ≤ C I i * ‖ψ I i x‖
            intro a _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))ψ:DerivativeIndex d k → Fin m → Space d → ℝhψ:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xC:DerivativeIndex d k → Fin m → ℝK:DerivativeIndex d k → Fin m → Set (Space d)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ax:Space ds:ℝhs:s ∈ Metric.ball 0 1houter:‖∑ I, ∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤
  ∑ I, ‖∑ a, firstVariationDensityTerm L (variedField f η s) η I a x‖I:DerivativeIndex d ka✝¹:I ∈ Finset.univa:Fin ma✝:a ∈ Finset.univ⊢ ‖firstVariationDensityTerm L (variedField f η s) η I a x‖ ≤ C I a * ‖ψ I a x‖
            exact firstVariationDensityTerm_norm_le_of_coeff_bound
              L f η ψ hψ C K hKzero hC hs I aAll goals completed! 🐙

A concrete dominated bound for the varied first-variation density, obtained from continuity of the jet-coordinate coefficient family in (s, x). The compact support of the iterated derivatives of the admissible variation supplies the integrable majorant.


lemma hasDominatedVariationDerivativeNear_of_continuous_coordDeriv
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (hcont : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      Continuous (fun p : ℝ × Space d =>
        L.coordDeriv I a (jetAt k (variedField f η p.1) p.2))) :
    HasDominatedVariationDerivativeNear L f η := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)⊢ HasDominatedVariationDerivativeNear L f η
  classical
  let ψ : DerivativeIndex d k → Fin m → Space d → ℝ :=
    fun I a x => ∂^[I.1] (fun y => (η y) a) xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x⊢ HasDominatedVariationDerivativeNear L f η
  have hψ : ∀ I : DerivativeIndex d k, ∀ a : Fin m, IsTestFunction (ψ I a) := by
    intro I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xI:DerivativeIndex d ka:Fin m⊢ IsTestFunction (ψ I a)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)⊢ HasDominatedVariationDerivativeNear L f η
    simpa [ψ] using iteratedDeriv_coord_isTestFunction η I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)⊢ HasDominatedVariationDerivativeNear L f η
  have hψ_eval : ∀ I : DerivativeIndex d k, ∀ a : Fin m, ∀ x : Space d,
      ψ I a x = ∂^[I.1] (fun y => (η y) a) x := by
    intro I a xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)I:DerivativeIndex d ka:Fin mx:Space d⊢ ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x⊢ HasDominatedVariationDerivativeNear L f η
    rfld:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x⊢ HasDominatedVariationDerivativeNear L f η
  choose K hKcompact hKzero using fun I : DerivativeIndex d k => fun a : Fin m =>
    exists_compact_iff_hasCompactSupport.mpr (hψ I a).suppd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0⊢ HasDominatedVariationDerivativeNear L f η
  let C : DerivativeIndex d k → Fin m → ℝ := fun I a =>
    Classical.choose <|
      ((isCompact_closedBall (0 : ℝ) 1).prod (hKcompact I a)).exists_bound_of_continuousOn
        ((hcont I a).continuousOn)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯⊢ HasDominatedVariationDerivativeNear L f η
  have hC : ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      ∀ p ∈ Metric.closedBall (0 : ℝ) 1 ×ˢ K I a,
        ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a := by
    intro I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯I:DerivativeIndex d ka:Fin m⊢ ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a⊢ HasDominatedVariationDerivativeNear L f η
    simpa [C] using Classical.choose_spec
      (((isCompact_closedBall (0 : ℝ) 1).prod (hKcompact I a)).exists_bound_of_continuousOn
        ((hcont I a).continuousOn))d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I a⊢ HasDominatedVariationDerivativeNear L f η
  let bound : Space d → ℝ :=
    fun x => ∑ I : DerivativeIndex d k, ∑ a : Fin m, C I a * ‖ψ I a x‖d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖⊢ HasDominatedVariationDerivativeNear L f η
  have hbound_int : Integrable bound volume := by
    refine integrable_finsetSum Finset.univ ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖⊢ ∀ i ∈ Finset.univ, Integrable (fun x => ∑ a, C i a * ‖ψ i a x‖) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f η
    intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ Integrable (fun x => ∑ a, C I a * ‖ψ I a x‖) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f η
    refine integrable_finsetSum Finset.univ ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖I:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∀ i ∈ Finset.univ, Integrable (fun x => C I i * ‖ψ I i x‖) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f η
    intro a _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖I:DerivativeIndex d ka✝¹:I ∈ Finset.univa:Fin ma✝:a ∈ Finset.univ⊢ Integrable (fun x => C I a * ‖ψ I a x‖) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f η
    exact ((hψ I a).integrable (μ := volume)).norm.const_mul (C I a)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ HasDominatedVariationDerivativeNear L f η
  have hfirst_int :
      Integrable (firstVariationDensity L f η) volume := by
    refine integrable_finsetSum Finset.univ ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volume⊢ ∀ i ∈ Finset.univ, Integrable (fun a => ∑ a_1, firstVariationDensityTerm L f η i a_1 a) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
    intro I _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumeI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ Integrable (fun a => ∑ a_1, firstVariationDensityTerm L f η I a_1 a) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
    refine integrable_finsetSum Finset.univ ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumeI:DerivativeIndex d ka✝:I ∈ Finset.univ⊢ ∀ i ∈ Finset.univ, Integrable (firstVariationDensityTerm L f η I i) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
    intro a _d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumeI:DerivativeIndex d ka✝¹:I ∈ Finset.univa:Fin ma✝:a ∈ Finset.univ⊢ Integrable (firstVariationDensityTerm L f η I a) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
    have hcoeff0 :
        Continuous (fun x : Space d => L.coordDeriv I a (jetAt k f x)) :=
      continuous_coordDeriv_at_zero L f η hcont I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumeI:DerivativeIndex d ka✝¹:I ∈ Finset.univa:Fin ma✝:a ∈ Finset.univhcoeff0:Continuous fun x => L.coordDeriv I a (jetAt k f x)⊢ Integrable (firstVariationDensityTerm L f η I a) volumed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
    exact firstVariationDensityTerm_integrable_of_continuous_coordDeriv L f η I a hcoeff0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volume⊢ HasDominatedVariationDerivativeNear L f η
  have hbound :
      ∀ x : Space d, ∀ s ∈ Metric.ball (0 : ℝ) 1,
        ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x := by
    intro x s hsd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volumex:Space ds:ℝhs:s ∈ Metric.ball 0 1⊢ ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volumehbound:∀ (x : Space d), ∀ s ∈ Metric.ball 0 1, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x⊢ HasDominatedVariationDerivativeNear L f η
    simpa [bound] using norm_firstVariationDensity_le_bound
      L f η ψ hψ_eval C K hKzero hC hsd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volumehbound:∀ (x : Space d), ∀ s ∈ Metric.ball 0 1, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x⊢ HasDominatedVariationDerivativeNear L f ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volumehbound:∀ (x : Space d), ∀ s ∈ Metric.ball 0 1, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x⊢ HasDominatedVariationDerivativeNear L f η
  refine ⟨1, zero_lt_one, bound, hfirst_int.aestronglyMeasurable, hbound_int, ?_⟩d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hcont:∀ (I : DerivativeIndex d k) (a : Fin m), Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)ψ:DerivativeIndex d k → Fin m → Space d → ℝ := fun I a x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:∀ (I : DerivativeIndex d k) (a : Fin m), IsTestFunction (ψ I a)hψ_eval:∀ (I : DerivativeIndex d k) (a : Fin m) (x : Space d),
  ψ I a x = Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xK:DerivativeIndex d k → Fin m → Set (Space d)hKcompact:∀ (I : DerivativeIndex d k) (a : Fin m), IsCompact (K I a)hKzero:∀ (I : DerivativeIndex d k) (a : Fin m), ∀ x ∉ K I a, ψ I a x = 0C:DerivativeIndex d k → Fin m → ℝ := fun I a => Classical.choose ⋯hC:∀ (I : DerivativeIndex d k) (a : Fin m),
  ∀ p ∈ Metric.closedBall 0 1 ×ˢ K I a, ‖L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)‖ ≤ C I abound:Space d → ℝ := fun x => ∑ I, ∑ a, C I a * ‖ψ I a x‖hbound_int:Integrable bound volumehfirst_int:Integrable (firstVariationDensity L f η) volumehbound:∀ (x : Space d), ∀ s ∈ Metric.ball 0 1, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x⊢ ∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 1, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x
  exact Filter.Eventually.of_forall hboundAll goals completed! 🐙

B. Pointwise linearization

              

lemma hasDerivAt_actionDensity_variedField_zero_of_contDiff
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) :
    ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)), ∀ x : Space d,
      HasDerivAt (fun s : ℝ => actionDensity L (variedField f η s) x)
        (firstVariationDensity L f η x) 0 := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ f⊢ ∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (x : Space d),
  HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
  intro η xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space d⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
  have hjet :
      ∀ s : ℝ, jetAt k (variedField f η s) x =
        (jetAt k f x).lineMap (jetDirectionAt k η x) s := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ f⊢ ∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (x : Space d),
  HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
    intro sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝ⊢ jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
    exact jetAt_add_smul k f η x s hf η.isTestFunction.contDiffd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
  have hfun :
      (fun s : ℝ => actionDensity L (variedField f η s) x) =
        fun s : ℝ => L ((jetAt k f x).lineMap (jetDirectionAt k η x) s) := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ f⊢ ∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (x : Space d),
  HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
    funext sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) ss:ℝ⊢ actionDensity L (variedField f η s) x = L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
    rw [actionDensity_applyd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) ss:ℝ⊢ L.toFun (jetAt k (variedField f η s) x) = L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) ss:ℝ⊢ L.toFun (jetAt k (variedField f η s) x) = L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) ss:ℝ⊢ L.toFun (jetAt k (variedField f η s) x) = L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
    simp [hjet s]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => actionDensity L (variedField f η s) x) (firstVariationDensity L f η x) 0
  rw [hfund:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)) (firstVariationDensity L f η x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)) (firstVariationDensity L f η x) 0]d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space dhjet:∀ (s : ℝ), jetAt k (variedField f η s) x = (jetAt k f x).lineMap (jetDirectionAt k η.toFun x) shfun:(fun s => actionDensity L (variedField f η s) x) = fun s =>
  L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)⊢ HasDerivAt (fun s => L.toFun ((jetAt k f x).lineMap (jetDirectionAt k η.toFun x) s)) (firstVariationDensity L f η x) 0
  simpa [Lagrangian.fiberDerivative, firstVariationDensity, firstVariationDensityTerm,
    jetDirectionAt_coord] using
    (L.hasDerivAt_lineMap (jetAt k f x) (jetDirectionAt k η x))All goals completed! 🐙

lemma hasDerivAt_actionDensity_variedField_of_contDiff
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f)
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (x : Space d) (s : ℝ) :
    HasDerivAt (fun r : ℝ => actionDensity L (variedField f η r) x)
      (firstVariationDensity L (variedField f η s) η x) s := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝ⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) s
  have hzero :
      HasDerivAt (fun t : ℝ => actionDensity L (variedField (variedField f η s) η t) x)
        (firstVariationDensity L (variedField f η s) η x) 0 := by
    exact hasDerivAt_actionDensity_variedField_zero_of_contDiff L (variedField f η s)
      (variedField_contDiff f η s hf) η xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) s
  have hshift :
      HasDerivAt (fun t : ℝ => actionDensity L (variedField f η (t + s)) x)
        (firstVariationDensity L (variedField f η s) η x) 0 := by
    simpa [variedField_variedField, add_comm] using hzerod:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0hshift:HasDerivAt (fun t => actionDensity L (variedField f η (t + s)) x) (firstVariationDensity L (variedField f η s) η x) 0⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0hshift:HasDerivAt (fun t => actionDensity L (variedField f η (t + s)) x) (firstVariationDensity L (variedField f η s) η x) 0⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) s
  let k : ℝ → ℝ := fun t => actionDensity L (variedField f η (t + s)) xd:ℕm:ℕk✝:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0hshift:HasDerivAt (fun t => actionDensity L (variedField f η (t + s)) x) (firstVariationDensity L (variedField f η s) η x) 0k:ℝ → ℝ := fun t => actionDensity L (variedField f η (t + s)) x⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) s
  have hk : HasDerivAt k (firstVariationDensity L (variedField f η s) η x) (s - s) := by
    simpa [k] using hshiftd:ℕm:ℕk✝:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0hshift:HasDerivAt (fun t => actionDensity L (variedField f η (t + s)) x) (firstVariationDensity L (variedField f η s) η x) 0k:ℝ → ℝ := fun t => actionDensity L (variedField f η (t + s)) xhk:HasDerivAt k (firstVariationDensity L (variedField f η s) η x) (s - s)⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) sd:ℕm:ℕk✝:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space ds:ℝhzero:HasDerivAt (fun t => actionDensity L (variedField (variedField f η s) η t) x)
  (firstVariationDensity L (variedField f η s) η x) 0hshift:HasDerivAt (fun t => actionDensity L (variedField f η (t + s)) x) (firstVariationDensity L (variedField f η s) η x) 0k:ℝ → ℝ := fun t => actionDensity L (variedField f η (t + s)) xhk:HasDerivAt k (firstVariationDensity L (variedField f η s) η x) (s - s)⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (firstVariationDensity L (variedField f η s) η x) s
  simpa [k, sub_eq_add_neg, add_assoc] using
    (HasDerivAt.comp_sub_const (f := k) (x := s) (a := s) hk)All goals completed! 🐙lemma hasPointwiseLinearizedDensityFormula_of_contDiff
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f) :
    HasPointwiseLinearizedDensityFormula L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ f⊢ HasPointwiseLinearizedDensityFormula L f
  intro η xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space d⊢ deriv (fun s => actionDensity L (variedField f η s) x) 0 = firstVariationDensity L f η x
  exact (hasDerivAt_actionDensity_variedField_zero_of_contDiff L f hf η x).derivAll goals completed! 🐙

lemma hasActionVariationDerivativeUnderIntegral_of_contDiff_of_dominatedVariation
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f)
    (hdom : ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)),
      HasFiniteActionVariation L f η →
      HasDominatedVariationDerivativeNear L f η) :
    HasActionVariationDerivativeUnderIntegral L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η⊢ HasActionVariationDerivativeUnderIntegral L f
  intro η hηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f η⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  rcases hdom η hη with ⟨ε, hε, bound, hF'_meas, hbound_int, hbound⟩d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound x⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  let F' : ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) η⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hmeas :
      ∀ᶠ s in nhds (0 : ℝ),
        AEStronglyMeasurable (actionDensity L (variedField f η s)) volume := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η⊢ HasActionVariationDerivativeUnderIntegral L fd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    exact Filter.Eventually.of_forall fun s => (hη s).aestronglyMeasurabled:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hderiv :
      ∀ᵐ x ∂volume, ∀ s ∈ Metric.ball (0 : ℝ) ε,
        HasDerivAt (fun r : ℝ => actionDensity L (variedField f η r) x) (F' s x) s := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η⊢ HasActionVariationDerivativeUnderIntegral L fd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    filter_upwards with xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumex:Space d⊢ ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    intro s hsd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumex:Space ds:ℝhs:s ∈ Metric.ball 0 ε⊢ HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    simpa [F'] using hasDerivAt_actionDensity_variedField_of_contDiff L f hf η x sd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) s⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hfinite0 : Integrable (actionDensity L (variedField f η 0)) := hη 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hF0_meas : AEStronglyMeasurable (F' 0) volume := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η⊢ HasActionVariationDerivativeUnderIntegral L fd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    simpa [F', firstVariationDensity, firstVariationDensityTerm, variedField] using hF'_measd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volume⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hresult :=
    actionVariation_hasDerivAt_of_dominated_loc_of_deriv_le L f η hε hmeas hfinite0
      hF0_meas hbound hbound_int hderivd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  have hvalue :
      (∫ x, F' 0 x)
        = ∫ x, deriv (fun s : ℝ => actionDensity L (variedField f η s) x) 0 := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η⊢ HasActionVariationDerivativeUnderIntegral L fd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    apply integral_congr_aed:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0⊢ F' 0 =ᵐ[volume] fun a => deriv (fun s => actionDensity L (variedField f η s) a) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    filter_upwards with xd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0x:Space d⊢ F' 0 x = deriv (fun s => actionDensity L (variedField f η s) x) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
    simpa [F', firstVariationDensity, firstVariationDensityTerm, variedField] using
      (hasPointwiseLinearizedDensityFormula_of_contDiff L f hf η x).symmd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), F' 0 x) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  rw [hvalued:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0] at hresultd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhdom:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f ηη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hη:HasFiniteActionVariation L f ηε:ℝhε:ε > 0bound:Space d → ℝhF'_meas:AEStronglyMeasurable (firstVariationDensity L f η) volumehbound_int:Integrable bound volumehbound:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, ‖firstVariationDensity L (variedField f η s) η x‖ ≤ bound xF':ℝ → Space d → ℝ := fun s => firstVariationDensity L (variedField f η s) ηhmeas:∀ᶠ (s : ℝ) in nhds 0, AEStronglyMeasurable (actionDensity L (variedField f η s)) volumehderiv:∀ᵐ (x : Space d), ∀ s ∈ Metric.ball 0 ε, HasDerivAt (fun r => actionDensity L (variedField f η r) x) (F' s x) shfinite0:Integrable (actionDensity L (variedField f η 0)) volumehF0_meas:AEStronglyMeasurable (F' 0) volumehresult:HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0hvalue:∫ (x : Space d), F' 0 x = ∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0⊢ HasDerivAt (actionVariation L f η) (∫ (x : Space d), deriv (fun s => actionDensity L (variedField f η s) x) 0) 0
  exact hresultAll goals completed! 🐙lemma hasActionVariationDerivativeUnderIntegral_of_contDiff_of_continuous_coordDeriv
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f)
    (hcontVar : ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)),
      ∀ I : DerivativeIndex d k, ∀ a : Fin m,
      Continuous (fun p : ℝ × Space d =>
        L.coordDeriv I a (jetAt k (variedField f η p.1) p.2))) :
    HasActionVariationDerivativeUnderIntegral L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (I : DerivativeIndex d k) (a : Fin m),
  Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)⊢ HasActionVariationDerivativeUnderIntegral L f
  refine hasActionVariationDerivativeUnderIntegral_of_contDiff_of_dominatedVariation L f hf ?_d:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (I : DerivativeIndex d k) (a : Fin m),
  Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)⊢ ∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))),
  HasFiniteActionVariation L f η → HasDominatedVariationDerivativeNear L f η
  intro η _hηd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (I : DerivativeIndex d k) (a : Fin m),
  Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))_hη:HasFiniteActionVariation L f η⊢ HasDominatedVariationDerivativeNear L f η
  exact hasDominatedVariationDerivativeNear_of_continuous_coordDeriv L f η (hcontVar η)All goals completed! 🐙lemma hasActionVariationDerivativeUnderIntegral_of_contDiff_of_regular
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m)) (hf : ContDiff ℝ ∞ f)
    (hcontVar : ∀ η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)),
      Lagrangian.ContinuousCoordDerivAlongFamily L (fun s : ℝ => variedField f η s)) :
    HasActionVariationDerivativeUnderIntegral L f := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η s⊢ HasActionVariationDerivativeUnderIntegral L f
  apply hasActionVariationDerivativeUnderIntegral_of_contDiff_of_continuous_coordDeriv L f hfd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η s⊢ ∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) (I : DerivativeIndex d k) (a : Fin m),
  Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)
  intro η I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)hf:ContDiff ℝ ∞ fhcontVar:∀ (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))), L.ContinuousCoordDerivAlongFamily fun s => variedField f η sη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin m⊢ Continuous fun p => L.coordDeriv I a (jetAt k (variedField f η p.1) p.2)
  exact hcontVar η I aAll goals completed! 🐙