OAI/Analysis/BernoulliCone/MinimizerOuterVariation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Bernoulli.outerVariation_of_comparison line 14

   Source documentation

   Multiplicative variations preserve the positivity set exactly.

   lemma outerVariation_of_comparison [IsFiniteMeasure (volume.restrict D)]
       {u : Space d → ℝ} {G : Space d → Space d}
       (hD : IsOpen D) (hu : H1 D u G)
       (hn : ∀ᵐ x ∂volume.restrict D, 0 ≤ u x)
       (hmin : ∀ (v : Space d → ℝ) (V : Space d → Space d),
         H1 D v V → (∀ᵐ x ∂volume.restrict D, 0 ≤ v x) →
         H10 D (fun x => v x-u x) (fun x => V x-G x) →
         energy D u G ≤ energy D v V)
       {φ : Space d → ℝ} (hφ : Test D φ) :
       (∫ x in D, inner ℝ (G x) (φ x • G x+u x • gradient φ x)) = 0 := by
   …

   Mentions: OAI.Bernoulli.Space, OAI.Bernoulli.H1, OAI.Bernoulli.H10, OAI.Bernoulli.energy, OAI.Bernoulli.Test

2. lemma OAI.Bernoulli.GlobalMinimizer.outerVariation line 54