PhyslibAlpha.ClassicalFieldTheory.Local.JetPoint

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 Physlib.SpaceAndTime.Space.Derivatives.DerivativeIndex
public import Physlib.SpaceAndTime.Space.Derivatives.Iterated

Coordinate-level jet points

i. Overview

This module introduces the coordinate-level point of the locally trivialized k-jet bundle for fields on Space d with values in EuclideanSpace ℝ (Fin m).

This module only formalizes the local coordinate model Jet^k(Ω, ℝ^m) ≃ Ω × V; it does not attempt to define global jet bundles.

At this core stage, a jet point is represented by:

its base point in Space d,

and its jet coordinates indexed by derivative indices of order at most k.

In particular, the zero-th order field value is not stored separately: it is the zero derivative coordinate.

ii. Key results

ClassicalFieldTheory.Local.JetCoordinates

ClassicalFieldTheory.Local.JetPoint

ClassicalFieldTheory.Local.jetCoordinatesAt

ClassicalFieldTheory.Local.jetAt

iii. Table of contents

A. Jet coordinates

B. Jet points

C. Jet points of fields

iv. References

J. Cortés and A. Haupt, Lecture Notes on Mathematical Methods of Classical Physics, arXiv:1612.03100v2, Chapter 5, Section 5.1.

@[expose] public section

A. Jet coordinates

Coordinate data u^a_I for k-th order jet points.

For each derivative index I, these are the scalar components of the corresponding EuclideanSpace ℝ (Fin m) fiber coordinate. We keep this componentwise form because the local Euler-Lagrange formulas are indexed by both I and a.

abbrev JetCoordinates (d m k : ℕ) := DerivativeIndex d k → Fin m → ℝ

B. Jet points

The coordinate-level points of the locally trivialized k-jet bundle for fields Space d → EuclideanSpace ℝ (Fin m).

The base point of the jet point.

The jet coordinates indexed by all derivative indices of order at most k.

              structure JetPoint (d m k : ℕ) where  base : Space d  fiber : JetCoordinates d m k

The coordinate u^a_I of a jet point.

def coord (J : JetPoint d m k) (I : DerivativeIndex d k) (a : Fin m) : ℝ := J.fiber I a

The zero-th order value encoded by a jet point.

def value (J : JetPoint d m k) : EuclideanSpace ℝ (Fin m) :=
  WithLp.toLp 2 fun a => J.coord 0 a

@[simp]
lemma value_apply (J : JetPoint d m k) (a : Fin m) :
    J.value a = J.coord 0 a := byd:ℕm:ℕk:ℕJ:JetPoint d m ka:Fin m⊢ J.value.ofLp a = J.coord 0 a
  simp [value]All goals completed! 🐙

@[ext]
lemma ext (J K : JetPoint d m k) (hbase : J.base = K.base)
    (hcoord : ∀ I a, J.coord I a = K.coord I a) :
    J = K := byd:ℕm:ℕk:ℕJ:JetPoint d m kK:JetPoint d m khbase:J.base = K.basehcoord:∀ (I : DerivativeIndex d k) (a : Fin m), J.coord I a = K.coord I a⊢ J = K
  cases J with
  | mk x u =>mkd:ℕm:ℕk:ℕK:JetPoint d m kx:Space du:JetCoordinates d m khbase:{ base := x, fiber := u }.base = K.basehcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { base := x, fiber := u }.coord I a = K.coord I a⊢ { base := x, fiber := u } = K
    cases K with
    | mk y v =>mk.mkd:ℕm:ℕk:ℕx:Space du:JetCoordinates d m ky:Space dv:JetCoordinates d m khbase:{ base := x, fiber := u }.base = { base := y, fiber := v }.basehcoord:∀ (I : DerivativeIndex d k) (a : Fin m), { base := x, fiber := u }.coord I a = { base := y, fiber := v }.coord I a⊢ { base := x, fiber := u } = { base := y, fiber := v }
      dsimp [coord] at hbase hcoordmk.mkd:ℕm:ℕk:ℕx:Space du:JetCoordinates d m ky:Space dv:JetCoordinates d m khbase:x = yhcoord:∀ (I : DerivativeIndex d k) (a : Fin m), u I a = v I a⊢ { base := x, fiber := u } = { base := y, fiber := v }
      subst ymk.mkd:ℕm:ℕk:ℕx:Space du:JetCoordinates d m kv:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), u I a = v I a⊢ { base := x, fiber := u } = { base := x, fiber := v }
      congrmk.mk.e_fiberd:ℕm:ℕk:ℕx:Space du:JetCoordinates d m kv:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), u I a = v I a⊢ u = v
      funext I amk.mk.e_fiberd:ℕm:ℕk:ℕx:Space du:JetCoordinates d m kv:JetCoordinates d m khcoord:∀ (I : DerivativeIndex d k) (a : Fin m), u I a = v I aI:DerivativeIndex d ka:Fin m⊢ u I a = v I a
      exact hcoord I aAll goals completed! 🐙

Build a jet point from a base point and its jet coordinates.

def ofBaseCoordinates (x : Space d) (u : JetCoordinates d m k) : JetPoint d m k where
  base := x
  fiber := u

The base point and jet coordinates of a jet point.

def toBaseCoordinates (J : JetPoint d m k) : Space d × JetCoordinates d m k := (J.base, J.fiber)

              @[simp]
lemma ofBaseCoordinates_base (x : Space d) (u : JetCoordinates d m k) :
    (ofBaseCoordinates x u).base = x := rfl@[simp]
lemma ofBaseCoordinates_fiber (x : Space d) (u : JetCoordinates d m k) :
    (ofBaseCoordinates x u).fiber = u := rfl@[simp]
lemma ofBaseCoordinates_coord (x : Space d) (u : JetCoordinates d m k)
    (I : DerivativeIndex d k) (a : Fin m) :
    (ofBaseCoordinates x u).coord I a = u I a := rfl@[simp]
lemma ofBaseCoordinates_base_fiber (J : JetPoint d m k) :
    ofBaseCoordinates J.base J.fiber = J := byd:ℕm:ℕk:ℕJ:JetPoint d m k⊢ ofBaseCoordinates J.base J.fiber = J
  apply JetPoint.exthbased:ℕm:ℕk:ℕJ:JetPoint d m k⊢ (ofBaseCoordinates J.base J.fiber).base = J.basehcoordd:ℕm:ℕk:ℕJ:JetPoint d m k⊢ ∀ (I : DerivativeIndex d k) (a : Fin m), (ofBaseCoordinates J.base J.fiber).coord I a = J.coord I a
  ·hbased:ℕm:ℕk:ℕJ:JetPoint d m k⊢ (ofBaseCoordinates J.base J.fiber).base = J.base rflAll goals completed! 🐙
  ·hcoordd:ℕm:ℕk:ℕJ:JetPoint d m k⊢ ∀ (I : DerivativeIndex d k) (a : Fin m), (ofBaseCoordinates J.base J.fiber).coord I a = J.coord I a intro I ahcoordd:ℕm:ℕk:ℕJ:JetPoint d m kI:DerivativeIndex d ka:Fin m⊢ (ofBaseCoordinates J.base J.fiber).coord I a = J.coord I a
    rflAll goals completed! 🐙@[simp]
lemma toBaseCoordinates_ofBaseCoordinates (x : Space d) (u : JetCoordinates d m k) :
    (ofBaseCoordinates x u).toBaseCoordinates = (x, u) := rfl

C. Jet points of fields

              @[simp]
lemma jetAt_base (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d) :
    (jetAt k f x).base = x := rfl@[simp]
lemma jetAt_value (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d) :
    (jetAt k f x).value = f x := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ (jetAt k f x).value = f x
  ext ad:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space da:Fin m⊢ (jetAt k f x).value.ofLp a = (f x).ofLp a
  simp [JetPoint.value, JetPoint.coord, jetAt, jetCoordinatesAt, Space.iteratedDeriv_zero]All goals completed! 🐙@[simp]
lemma jetAt_coord (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d)
    (I : DerivativeIndex d k) (a : Fin m) :
    (jetAt k f x).coord I a = ∂^[I.1] (fun y => (f y) a) x := rfllemma jetAt_coord_zero (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d)
    (a : Fin m) :
    (jetAt k f x).coord 0 a = (f x) a := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space da:Fin m⊢ (jetAt k f x).coord 0 a = (f x).ofLp a
  simp [jetAt_coord]All goals completed! 🐙@[simp]
lemma jetCoordinatesAt_eq (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m)) (x : Space d)
    (I : DerivativeIndex d k) (a : Fin m) :
    jetCoordinatesAt k g x I a = ∂^[I.1] (fun y => (g y) a) x := rfllemma jetCoordinatesAt_zero (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m))
    (x : Space d) (a : Fin m) :
    jetCoordinatesAt k g x 0 a = (g x) a := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space da:Fin m⊢ jetCoordinatesAt k g x 0 a = (g x).ofLp a
  simp [jetCoordinatesAt]All goals completed! 🐙lemma jetAt_eq_ofBaseCoordinates (k : ℕ) (f : Space d → EuclideanSpace ℝ (Fin m))
    (x : Space d) :
    jetAt k f x = JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x) := byd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ jetAt k f x = JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)
  apply JetPoint.exthbased:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ (jetAt k f x).base = (JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)).basehcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ ∀ (I : DerivativeIndex d k) (a : Fin m),
  (jetAt k f x).coord I a = (JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)).coord I a
  ·hbased:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ (jetAt k f x).base = (JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)).base rflAll goals completed! 🐙
  ·hcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space d⊢ ∀ (I : DerivativeIndex d k) (a : Fin m),
  (jetAt k f x).coord I a = (JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)).coord I a intro I ahcoordd:ℕm:ℕk:ℕf:Space d → EuclideanSpace ℝ (Fin m)x:Space dI:DerivativeIndex d ka:Fin m⊢ (jetAt k f x).coord I a = (JetPoint.ofBaseCoordinates x (jetCoordinatesAt k f x)).coord I a
    rflAll goals completed! 🐙