PhyslibAlpha.ClassicalFieldTheory.Local.JetPointRegularity

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

Regularity and support for jet-coordinate maps

i. Overview

This module collects the analytic facts about coordinate-level jet maps that are needed later in the local variational argument.

At this stage, it provides:

smoothness of jet-coordinate maps of smooth fields,

smoothness of the base-plus-coordinate jet map,

and vanishing of jet coordinates outside topological support.

ii. Key results

ClassicalFieldTheory.Local.jetCoordinatesAt_contDiff

ClassicalFieldTheory.Local.jetBaseCoordinates_contDiff

ClassicalFieldTheory.Local.jetCoordinatesAt_eq_zero_of_notMem_tsupport

ClassicalFieldTheory.Local.jetDirectionAt_eq_zero_of_notMem_tsupport

iii. Table of contents

A. Smoothness of jet-coordinate maps

B. Support and vanishing lemmas

iv. References

@[expose] public section

A. Smoothness of jet-coordinate maps

Smoothness of the jet-coordinate map of a smooth field.


lemma jetCoordinatesAt_contDiff (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m))
    (hg : ContDiff ℝ ∞ g) :
    ContDiff ℝ ∞ (jetCoordinatesAt k g) := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ (jetCoordinatesAt k g)
  refine contDiff_pi.2 ?_d:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ g⊢ ∀ (i : DerivativeIndex d k), ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x i
  intro Id:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d k⊢ ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I
  refine contDiff_pi.2 ?_d:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d k⊢ ∀ (i : Fin m), ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I i
  intro ad:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin m⊢ ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I a
  have hga : ContDiff ℝ ∞ (fun y => (g y) a) := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ (jetCoordinatesAt k g)d:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I a
    exact (contDiff_piLp_apply (𝕜 := ℝ) (n := ∞) (p := 2)
      (E := fun _ : Fin m => ℝ) (i := a)).comp hgd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I ad:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ gI:DerivativeIndex d ka:Fin mhga:ContDiff ℝ ∞ fun y => (g y).ofLp a⊢ ContDiff ℝ ∞ fun x => jetCoordinatesAt k g x I a
  simpa [jetCoordinatesAt] using Space.iteratedDeriv_contDiff I.1 hgaAll goals completed! 🐙

Smoothness of the base-plus-coordinate jet map of a smooth field.

lemma jetBaseCoordinates_contDiff (k : ℕ) (g : Space d → EuclideanSpace ℝ (Fin m))
    (hg : ContDiff ℝ ∞ g) :
    ContDiff ℝ ∞ (fun x : Space d => (x, jetCoordinatesAt k g x)) := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)hg:ContDiff ℝ ∞ g⊢ ContDiff ℝ ∞ fun x => (x, jetCoordinatesAt k g x)
  exact contDiff_id.prodMk (jetCoordinatesAt_contDiff k g hg)All goals completed! 🐙

B. Support and vanishing lemmas



private lemma notMem_tsupport_coord {g : Space d → EuclideanSpace ℝ (Fin m)} {x : Space d}
    (hx : x ∉ tsupport g) (a : Fin m) :
    x ∉ tsupport (fun y => (g y) a) := byd:ℕm:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport ga:Fin m⊢ x ∉ tsupport fun y => (g y).ofLp a
  rw [notMem_tsupport_iff_eventuallyEqd:ℕm:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:g =ᶠ[𝓝 x] 0a:Fin m⊢ (fun y => (g y).ofLp a) =ᶠ[𝓝 x] 0d:ℕm:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:g =ᶠ[𝓝 x] 0a:Fin m⊢ (fun y => (g y).ofLp a) =ᶠ[𝓝 x] 0] at hx ⊢d:ℕm:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:g =ᶠ[𝓝 x] 0a:Fin m⊢ (fun y => (g y).ofLp a) =ᶠ[𝓝 x] 0
  filter_upwards [hx] with y hyd:ℕm:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:g =ᶠ[𝓝 x] 0a:Fin my:Space dhy:g y = 0 y⊢ (g y).ofLp a = 0 y
  simp [hy]All goals completed! 🐙

Outside the topological support of a field, all of its jet coordinates vanish.

lemma jetCoordinatesAt_eq_zero_of_notMem_tsupport (k : ℕ)
    (g : Space d → EuclideanSpace ℝ (Fin m)) {x : Space d}
    (hx : x ∉ tsupport g) :
    jetCoordinatesAt k g x = 0 := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport g⊢ jetCoordinatesAt k g x = 0
  funext Id:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport gI:DerivativeIndex d k⊢ jetCoordinatesAt k g x I = 0 I
  funext ad:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport gI:DerivativeIndex d ka:Fin m⊢ jetCoordinatesAt k g x I a = 0 I a
  exact Space.iteratedDeriv_eq_zero_of_notMem_tsupport I.1 (notMem_tsupport_coord hx a)All goals completed! 🐙

Outside the topological support of a field, the corresponding jet-fiber direction vanishes.

lemma jetDirectionAt_eq_zero_of_notMem_tsupport (k : ℕ)
    (g : Space d → EuclideanSpace ℝ (Fin m)) {x : Space d}
    (hx : x ∉ tsupport g) :
    jetDirectionAt k g x = 0 := byd:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport g⊢ jetDirectionAt k g x = 0
  ext I ad:ℕm:ℕk:ℕg:Space d → EuclideanSpace ℝ (Fin m)x:Space dhx:x ∉ tsupport gI:DerivativeIndex d ka:Fin m⊢ (jetDirectionAt k g x).coord I a = JetFiberData.coord 0 I a
  exact Space.iteratedDeriv_eq_zero_of_notMem_tsupport I.1 (notMem_tsupport_coord hx a)All goals completed! 🐙