OAI/Analysis/AffineBernstein/AffineParametricStationarity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.affineParametricVariationArea line 13

   Source comment

   The literal arbitrary affine image of a parametrized graph variation.

   def affineParametricVariationArea {n : ℕ} (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ))
       (v : Space n × ℝ) (u β : Space n → ℝ) (a : Fin n → Space n → ℝ)
       (x : Space n) (t : ℝ) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

2. lemma OAI.AffineBernstein.affineParametricVariationArea_eq line 21
3. theorem OAI.AffineBernstein.affineMaximal_affine_parametric_first_variation line 40

   Source comment

   Stationarity is genuinely preserved by every ambient affine transformation. The integrand is the derivative of the actual transformed parametric density. No equation for the affine image is assumed.

   theorem affineMaximal_affine_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)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ) :
       IntegrableOn (fun x => deriv (affineParametricVariationArea L v u β a x) 0) Ω ∧
         (∫ x in Ω, deriv (affineParametricVariationArea L v u β a x) 0) = 0 := by
   …

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