PhyslibAlpha.ClassicalFieldTheory.Local.FirstVariation.Support

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.Basic

First variation support lemmas

i. Overview

This module collects the reusable support lemmas used by the analytic part of the local first-variation proof: basic identities for varied fields, iterated derivative regularity for test functions, and continuity of the varied local-jet coordinate map.

ii. Key results

ClassicalFieldTheory.Local.variedField_zero

ClassicalFieldTheory.Local.variedField_variedField

iii. Table of contents

A. Varied fields

B. Iterated derivative support lemmas

C. Varied local-jet coordinates

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. Varied fields

@[simp]
lemma variedField_zero (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m))) :
    variedField f η 0 = f := byd:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))⊢ variedField f η 0 = f
  funext xd:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))x:Space d⊢ variedField f η 0 x = f x
  simp [variedField]All goals completed! 🐙

@[simp]
lemma variedField_variedField (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (s t : ℝ) :
    variedField (variedField f η s) η t = variedField f η (s + t) := byd:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝt:ℝ⊢ variedField (variedField f η s) η t = variedField f η (s + t)
  funext xd:ℕm:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))s:ℝt:ℝx:Space d⊢ variedField (variedField f η s) η t x = variedField f η (s + t) x
  simp [variedField, add_assoc, add_smul]All goals completed! 🐙

B. Iterated derivative support lemmas

              

lemma contDiff_space_deriv {g : Space d → ℝ} (hg : ContDiff ℝ ∞ g)
    (i : Fin d) : ContDiff ℝ ∞ (∂[i] g) := byd:ℕg:Space d → ℝhg:ContDiff ℝ ∞ gi:Fin d⊢ ContDiff ℝ ∞ (Space.deriv i g)
  have hfamily : ContDiff ℝ ∞ (fun x : Space d => fun j : Fin d => ∂[j] g x) := by
    simpa using (Space.deriv_contDiff (n := ∞) hg)d:ℕg:Space d → ℝhg:ContDiff ℝ ∞ gi:Fin dhfamily:ContDiff ℝ ∞ fun x j => Space.deriv j g x⊢ ContDiff ℝ ∞ (Space.deriv i g)d:ℕg:Space d → ℝhg:ContDiff ℝ ∞ gi:Fin dhfamily:ContDiff ℝ ∞ fun x j => Space.deriv j g x⊢ ContDiff ℝ ∞ (Space.deriv i g)
  exact (contDiff_apply ℝ ℝ i).comp hfamilyAll goals completed! 🐙lemma isTestFunction_space_deriv {g : Space d → ℝ} (hg : IsTestFunction g) (i : Fin d) :
    IsTestFunction (∂[i] g) := byd:ℕg:Space d → ℝhg:IsTestFunction gi:Fin d⊢ IsTestFunction (Space.deriv i g)
  simpa [Space.deriv_eq_fderiv_fun] using IsTestFunction.fderiv_apply hg (Space.basis i)All goals completed! 🐙lemma iteratedDerivList_contDiff (L : List (Fin d)) {g : Space d → ℝ}
    (hg : ContDiff ℝ ∞ g) :
    ContDiff ℝ ∞ (L.foldr (fun i h => ∂[i] h) g) := byd:ℕL:List (Fin d)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g L)
  induction L generalizing g with
  | nil =>nild:ℕg:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g [])
      simpa using hgAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ}, ContDiff ℝ ∞ g → ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g (i :: L))
      have htail : ContDiff ℝ ∞ (L.foldr (fun j h => ∂[j] h) g) := ih hgconsd:ℕi:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ}, ContDiff ℝ ∞ g → ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ ghtail:ContDiff ℝ ∞ (List.foldr (fun j h => Space.deriv j h) g L)⊢ ContDiff ℝ ∞ (List.foldr (fun i h => Space.deriv i h) g (i :: L))
      exact contDiff_space_deriv htail iAll goals completed! 🐙lemma iteratedDerivList_isTestFunction (L : List (Fin d)) {g : Space d → ℝ}
    (hg : IsTestFunction g) :
    IsTestFunction (L.foldr (fun i h => ∂[i] h) g) := byd:ℕL:List (Fin d)g:Space d → ℝhg:IsTestFunction g⊢ IsTestFunction (List.foldr (fun i h => Space.deriv i h) g L)
  induction L generalizing g with
  | nil =>nild:ℕg:Space d → ℝhg:IsTestFunction g⊢ IsTestFunction (List.foldr (fun i h => Space.deriv i h) g [])
      simpa using hgAll goals completed! 🐙
  | cons i L ih =>consd:ℕi:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ}, IsTestFunction g → IsTestFunction (List.foldr (fun i h => Space.deriv i h) g L)g:Space d → ℝhg:IsTestFunction g⊢ IsTestFunction (List.foldr (fun i h => Space.deriv i h) g (i :: L))
      simp only [List.foldr]consd:ℕi:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ}, IsTestFunction g → IsTestFunction (List.foldr (fun i h => Space.deriv i h) g L)g:Space d → ℝhg:IsTestFunction g⊢ IsTestFunction (Space.deriv i (List.foldr (fun i h => Space.deriv i h) g L))
      exact isTestFunction_space_deriv (ih hg) iAll goals completed! 🐙

lemma iteratedDerivList_commute_deriv (L : List (Fin d)) (i : Fin d)
    {g : Space d → ℝ} (hg : ContDiff ℝ ∞ g) :
    L.foldr (fun j h => ∂[j] h) (∂[i] g) = ∂[i] (L.foldr (fun j h => ∂[j] h) g) := byd:ℕL:List (Fin d)i:Fin dg:Space d → ℝhg:ContDiff ℝ ∞ g⊢ List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
  Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)
  induction L generalizing g with
  | nil =>nild:ℕi:Fin dg:Space d → ℝhg:ContDiff ℝ ∞ g⊢ List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) [] =
  Space.deriv i (List.foldr (fun j h => Space.deriv j h) g [])
      rflAll goals completed! 🐙
  | cons j L ih =>consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) (j :: L) =
  Space.deriv i (List.foldr (fun j h => Space.deriv j h) g (j :: L))
      simp only [List.foldr]consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ Space.deriv j (List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L) =
  Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L))
      rw [ih hgconsd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ Space.deriv j (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)) =
  Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L))consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ Space.deriv j (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)) =
  Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L))]consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ Space.deriv j (Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)) =
  Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L))
      rw [Space.deriv_commute (u := j) (v := i)consd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L)) =
  Space.deriv i (Space.deriv j (List.foldr (fun j h => Space.deriv j h) g L))cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)]cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)
      have h2 : ContDiff ℝ (2 : ℕ∞) (L.foldr (fun j h => ∂[j] h) g) := byd:ℕL:List (Fin d)i:Fin dg:Space d → ℝhg:ContDiff ℝ ∞ g⊢ List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
  Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ gh2:ContDiff ℝ (↑2) (List.foldr (fun j h => Space.deriv j h) g L)⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)
        exact (iteratedDerivList_contDiff L hg).of_le (byd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ g⊢ ↑2 ≤ ∞cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ gh2:ContDiff ℝ (↑2) (List.foldr (fun j h => Space.deriv j h) g L)⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)
          exact WithTop.coe_le_coe.mpr le_topAll goals completed! 🐙cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ gh2:ContDiff ℝ (↑2) (List.foldr (fun j h => Space.deriv j h) g L)⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L))cons.hfd:ℕi:Fin dj:Fin dL:List (Fin d)ih:∀ {g : Space d → ℝ},
  ContDiff ℝ ∞ g →
    List.foldr (fun j h => Space.deriv j h) (Space.deriv i g) L =
      Space.deriv i (List.foldr (fun j h => Space.deriv j h) g L)g:Space d → ℝhg:ContDiff ℝ ∞ gh2:ContDiff ℝ (↑2) (List.foldr (fun j h => Space.deriv j h) g L)⊢ ContDiff ℝ 2 (List.foldr (fun j h => Space.deriv j h) g L)
      exact h2All goals completed! 🐙lemma iteratedDeriv_coord_isTestFunction (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (I : DerivativeIndex d k) (a : Fin m) :
    IsTestFunction (fun x => ∂^[I.1] (fun y => (η y) a) x) := byd:ℕm:ℕk:ℕη:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin m⊢ IsTestFunction fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x
  simpa [Space.iteratedDeriv, Space.coord] using
    iteratedDerivList_isTestFunction I.1.toList (η.coord_euclidean a)All goals completed! 🐙lemma firstVariationDensityTerm_integrable_of_continuous_coordDeriv
    (L : Lagrangian d m k) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (I : DerivativeIndex d k) (a : Fin m)
    (hcont : Continuous (fun x : Space d =>
      L.coordDeriv I a (jetAt k f x))) :
    Integrable (firstVariationDensityTerm L f η I a) := byd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  let ψ : Space d → ℝ := fun 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))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)ψ:Space d → ℝ := fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) x⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  have hψ : IsTestFunction ψ := iteratedDeriv_coord_isTestFunction η I ad:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)ψ:Space d → ℝ := fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:IsTestFunction ψ⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  have hψcont : Continuous ψ := hψ.contDiff.continuousd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)ψ:Space d → ℝ := fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:IsTestFunction ψhψcont:Continuous ψ⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  have htermCont : Continuous (fun x => L.coordDeriv I a (jetAt k f x) * ψ x) :=
    hcont.mul hψcontd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)ψ:Space d → ℝ := fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:IsTestFunction ψhψcont:Continuous ψhtermCont:Continuous fun x => L.coordDeriv I a (jetAt k f x) * ψ x⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  have hsupp : HasCompactSupport (fun x => L.coordDeriv I a (jetAt k f x) * ψ x) :=
    HasCompactSupport.mul_left hψ.suppd:ℕm:ℕk:ℕL:Lagrangian d m kf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))I:DerivativeIndex d ka:Fin mhcont:Continuous fun x => L.coordDeriv I a (jetAt k f x)ψ:Space d → ℝ := fun x => Space.iteratedDeriv (↑I) (fun y => (η.toFun y).ofLp a) xhψ:IsTestFunction ψhψcont:Continuous ψhtermCont:Continuous fun x => L.coordDeriv I a (jetAt k f x) * ψ xhsupp:HasCompactSupport fun x => L.coordDeriv I a (jetAt k f x) * ψ x⊢ Integrable (firstVariationDensityTerm L f η I a) volume
  exact
    htermCont.integrable_of_hasCompactSupport hsuppAll goals completed! 🐙

C. Varied local-jet coordinates



lemma continuous_jetBaseCoordinates_variedField
    (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m))
    (η : AdmissibleVariation d (EuclideanSpace ℝ (Fin m)))
    (hf : ContDiff ℝ ∞ f) :
    Continuous
      (fun p : ℝ × Space d => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ f⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  have hfjet : Continuous (jetCoordinatesAt k f) :=
    (jetCoordinatesAt_contDiff k f hf).continuousd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  have hηjet : Continuous (jetCoordinatesAt k η) :=
    (jetCoordinatesAt_contDiff k η η.isTestFunction.contDiff).continuousd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  have hcoord :
      Continuous
        (fun p : ℝ × Space d =>
          jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η p.2) := by
    exact (hfjet.comp continuous_snd).add (continuous_fst.smul (hηjet.comp continuous_snd))d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  have hpair :
      Continuous
        (fun p : ℝ × Space d =>
          (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η p.2)) := by
    exact Continuous.prodMk continuous_snd hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  have heq :
      (fun p : ℝ × Space d => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) =
      (fun p : ℝ × Space d =>
        (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η p.2)) := by
    funext pd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)p:ℝ × Space d⊢ (p.2, jetCoordinatesAt k (variedField f η p.1) p.2) =
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
    congr 1e_sndd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)p:ℝ × Space d⊢ jetCoordinatesAt k (variedField f η p.1) p.2 = jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
    exact
      (jetCoordinatesAt_add_smul k f η p.2 p.1 hf η.isTestFunction.contDiff)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)
  rw [heqd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)]d:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)η:AdmissibleVariation d (EuclideanSpace ℝ (Fin m))hf:ContDiff ℝ ∞ fhfjet:Continuous (jetCoordinatesAt k f)hηjet:Continuous (jetCoordinatesAt k η.toFun)hcoord:Continuous fun p => jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2hpair:Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)heq:(fun p => (p.2, jetCoordinatesAt k (variedField f η p.1) p.2)) = fun p =>
  (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)⊢ Continuous fun p => (p.2, jetCoordinatesAt k f p.2 + p.1 • jetCoordinatesAt k η.toFun p.2)
  exact hpairAll goals completed! 🐙