GlobalHessianBound.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.second_directional_eq_quadratic line 18
lemma OAI.AffineBernstein.second_directional_normalized line 24

theorem OAI.AffineBernstein.centered_balanced_global_directional_bound line 37

Source documentation

The pointwise normalized estimate transfers through actual section maps to a global upper bound for every directional second derivative.

theorem centered_balanced_global_directional_bound {n : ℕ} (hn : 1 ≤ n)
    {u : Space n → ℝ} (hu : ContDiff ℝ ∞ u) (hp : ∀ x, (hessian u x).PosDef)
    (hm : AffineMaximalOn univ u) (hzero : u 0=0) (hdzero : fderiv ℝ u 0=0)
    {ρ : ℝ} (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hbal : SectionBalance univ u ρ) :
    ∃ C : ℝ, 0 < C ∧ ∀ e x : Space n,
      dirDeriv e (dirDeriv e u) x ≤ C*dirDeriv e (dirDeriv e u) 0 := by
…

Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.SectionBalance, OAI.AffineBernstein.dirDeriv

theorem OAI.AffineBernstein.balanced_global_directional_bddAbove line 73