OAI/Analysis/AffineBernstein/IntegratedParametricStationarity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.graphVariationArea_eq_of_notMem line 13
2. lemma OAI.AffineBernstein.fderiv_param_eq_deriv line 37
3. theorem OAI.AffineBernstein.affineMaximal_parametric_area_stationary line 48

   Source comment

   Actual differentiation of the compact affine-area functional, not just an integrated pointwise derivative.

   theorem affineMaximal_parametric_area_stationary {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) :
       HasDerivAt (fun t : ℝ => ∫ x in K, graphVariationArea u β a x t) 0 0 := by
   …

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

4. theorem OAI.AffineBernstein.affineMaximal_affine_parametric_area_stationary line 85

   Source comment

   The compact affine-area functional of every arbitrary affine image is stationary. All derivatives and integrals are the literal geometric density.

   theorem affineMaximal_affine_parametric_area_stationary {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 × ℝ) :
       HasDerivAt (fun t : ℝ => ∫ x in K, affineParametricVariationArea L v u β a x t) 0 0 := by
   …

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