ParametricStationarity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.normalVariation_compact line 13

Source comment

Every compact smooth parametric velocity has a genuinely smooth compact normal graph component, without extending the original graph smoothly.

lemma normalVariation_compact {n : ℕ} {Ω K : Set (Space n)} (hΩ : IsOpen Ω)
    (hK : IsCompact K) (hKΩ : K ⊆ Ω) {u β : Space n → ℝ}
    (hu : ContDiffOn ℝ ∞ u Ω) (hβ : ContDiff ℝ ∞ β) (hβK : tsupport β ⊆ K)
    {a : Fin n → Space n → ℝ} (ha : ∀ k, ContDiff ℝ ∞ (a k))
    (haK : ∀ k, tsupport (a k) ⊆ K) :
    ContDiff ℝ ∞ (normalVariation u β a) ∧
      HasCompactSupport (normalVariation u β a) ∧ tsupport (normalVariation u β a) ⊆ K := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.normalVariation

theorem OAI.AffineBernstein.affineMaximal_parametric_first_variation line 37

Source comment

The exact pointwise first variation under every compact smooth parametric velocity is integrable and has zero integral. The density uses the actual varying conormal and horizontal Jacobian.

theorem affineMaximal_parametric_first_variation {n : ℕ} {Ω K : Set (Space n)}
    (hΩ : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω)
    {u β : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
    (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
    (hβ : ContDiff ℝ ∞ β) (hβK : tsupport β ⊆ K)
    {a : Fin n → Space n → ℝ} (ha : ∀ k, ContDiff ℝ ∞ (a k))
    (haK : ∀ k, tsupport (a k) ⊆ K) :
    IntegrableOn (fun x => deriv (graphVariationArea u β a x) 0) Ω ∧
      (∫ x in Ω, deriv (graphVariationArea u β a x) 0) = 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.graphVariationArea