OAI/Analysis/AffineBernstein/PositiveMatrixTraceBound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.posSemidef_quadratic_le_trace_mul_sq line 18
2. def OAI.AffineBernstein.gradientSquared line 48
3. def OAI.AffineBernstein.gradientHessianSquare line 51
4. lemma OAI.AffineBernstein.gradientSquared_nonneg line 54
5. lemma OAI.AffineBernstein.inverseHessianPair_gradient_self line 57
6. lemma OAI.AffineBernstein.gradientHessianSquare_eq_dotProduct line 63
7. lemma OAI.AffineBernstein.gradientHessianSquare_nonneg line 74
8. lemma OAI.AffineBernstein.gradientHessianSquare_le_trace line 80
9. lemma OAI.AffineBernstein.inverseHessianPair_grad_linear line 86
10. lemma OAI.AffineBernstein.affineDetBarrier_critical_gradient line 106
11. lemma OAI.AffineBernstein.inverseHessianPair_logHessianDet_of_barrier_max line 117
12. lemma OAI.AffineBernstein.gradient_logHessianDet_of_barrier_max line 129
13. lemma OAI.AffineBernstein.affineDetBarrier_peak_identity line 142

    Source documentation

    The unabridged differential barrier identity at a local maximum. Its coefficient is the original affine maximal exponent.

    lemma affineDetBarrier_peak_identity {n : ℕ} {Ω : Set (Space n)} (hΩ : IsOpen Ω)
        {u : Space n → ℝ} (hu : ContDiffOn ℝ ∞ u Ω)
        (hp : ∀ x ∈ Ω, (hessian u x).PosDef) (hm : AffineMaximalOn Ω u)
        (hneg : ∀ x ∈ Ω, u x < 0) {x : Space n} (hx : x ∈ Ω) (γ : ℝ)
        (hmax : IsLocalMax (affineDetBarrier u ((n:ℝ)+2) γ) x) :
        inverseHessianTrace u (affineDetBarrier u ((n:ℝ)+2) γ) x =
          ((n:ℝ)*((n:ℝ)+2)/(u x)^2) * inverseHessianPair u u u x +
          γ * (hessian u x).trace - γ^2/((n:ℝ)+2) * gradientHessianSquare u x +
          ((n:ℝ)*((n:ℝ)+2) + γ*(n:ℝ)*gradientSquared u x) / u x := by
    …

    Mentions: OAI.AffineBernstein.Space, OAI.AffineBernstein.hessian, OAI.AffineBernstein.AffineMaximalOn, OAI.AffineBernstein.affineDetBarrier, OAI.AffineBernstein.inverseHessianTrace, OAI.AffineBernstein.inverseHessianPair, OAI.AffineBernstein.gradientHessianSquare, OAI.AffineBernstein.gradientSquared