OAI/Analysis/AffineBernstein/FlatEulerCore.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.flatTestContraction line 18
2. def OAI.AffineBernstein.flatDoubleDivergence line 21
3. lemma OAI.AffineBernstein.integrable_flatTestContraction line 24
4. lemma OAI.AffineBernstein.contDiffAt_flatDoubleDivergence line 41
5. lemma OAI.AffineBernstein.integrable_flatDoubleDivergence_mul line 50
6. lemma OAI.AffineBernstein.flatTestContraction_eq_zero_of_notMem_tsupport line 61
7. theorem OAI.AffineBernstein.flatDoubleDivergence_eq_zero_of_stationary line 78

   Source comment

   The fundamental variational lemma applied to two independent flat Hessian blocks. No pointwise PDE is an assumption.

   theorem flatDoubleDivergence_eq_zero_of_stationary {W : Set E} (hW : IsOpen W)
       (A : ι → ι → E → ℝ) (B : κ → κ → E → ℝ) (e : ι → E) (f : κ → E)
       (ha : ∀ i j x, x ∈ W → ContDiffAt ℝ ∞ (A i j) x)
       (hb : ∀ i j x, x ∈ W → ContDiffAt ℝ ∞ (B i j) x)
       (hstat : ∀ η : E → ℝ, ContDiff ℝ ∞ η → HasCompactSupport η → tsupport η ⊆ W →
         (∫ x, flatTestContraction A e η x + flatTestContraction B f η x ∂μ) = 0)
       {x : E} (hx : x ∈ W) :
       flatDoubleDivergence A e x + flatDoubleDivergence B f x = 0 := by
   …

   Mentions: OAI.AffineBernstein.flatTestContraction, OAI.AffineBernstein.flatDoubleDivergence