NormalizedHessianUpper.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.inverseNthRoot_sublevel_second line 18
lemma OAI.AffineBernstein.hessian_diagonal_le_trace line 28
theorem OAI.AffineBernstein.normalized_hessian_diagonal_upper line 36
Source documentation
A genuine normalized Hessian upper bound made from the original equation: the inverse-root Jacobi supersolution, ABP critical density, and the shifted gradient area formula. No interior regularity theorem is postulated.
```
theorem normalized_hessian_diagonal_upper {n : ℕ} (hn : 1 ≤ n) {ρ R : ℝ}
    (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hR : 1 ≤ R) :
    ∃ C : ℝ, 0 < C ∧ ∀ v : Space n → ℝ, BalancedNormalized ρ R v →
      ∀ a ∈ Metric.ball (0:Space n) (1/64:ℝ), ∀ i : Fin n, hessian v a i i ≤ C := by
…
```
Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.BalancedNormalized, OAI.AffineBernstein.hessian
theorem OAI.AffineBernstein.normalized_hessian_trace_upper line 95