OAI/Analysis/AffineBernstein/FlatTubeEuler.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.flatBlockHessian_neg line 17
2. def OAI.AffineBernstein.flatBaseEulerWeight line 30
3. def OAI.AffineBernstein.flatAngularEulerWeight line 33
4. lemma OAI.AffineBernstein.contDiffAt_flatEulerWeights line 36
5. lemma OAI.AffineBernstein.tubeAreaFirstVariation_eq_flatContraction line 49
6. theorem OAI.AffineBernstein.flatTubeEuler_of_stationary line 80

   Source comment

   Two true integrations by parts and Piola cancellation convert flat tube stationarity to the pointwise Euler equation.

   theorem flatTubeEuler_of_stationary {W : Set E} (hW : IsOpen W)
       (φ : E → ℝ) (v : ι → E) (w : κ → E) (δ : ℝ)
       (hφ : ContDiffOn ℝ ∞ φ W)
       (hB : ∀ x ∈ W, (flatBlockHessian (fun y => -φ y) v x).PosDef)
       (hR : ∀ x ∈ W, (flatBlockHessian φ w x).PosDef)
       (hstat : ∀ η : E → ℝ, ContDiff ℝ ∞ η → HasCompactSupport η → tsupport η ⊆ W →
         (∫ x, tubeAreaFirstVariation (flatBlockHessian (fun y => -φ y) v x)
           (-flatBlockHessian η v x) (flatBlockHessian φ w x) (flatBlockHessian η w x) δ ∂μ) = 0)
       {x : E} (hx : x ∈ W) :
       let B := fun y => flatBlockHessian (fun z => -φ z) v y
   …

   Mentions: OAI.AffineBernstein.flatBlockHessian, OAI.AffineBernstein.tubeAreaFirstVariation