OAI/Analysis/AffineBernstein/LogBarrierCalculus.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.dirDeriv_real_log line 18
  2. lemma OAI.AffineBernstein.second_dirDeriv_log_of_neg line 26
  3. lemma OAI.AffineBernstein.inverseHessianTrace_self line 43
  4. lemma OAI.AffineBernstein.inverseHessianTrace_add line 50
  5. lemma OAI.AffineBernstein.inverseHessianTrace_const_mul line 58
  6. lemma OAI.AffineBernstein.inverseHessianTrace_log line 69
  7. lemma OAI.AffineBernstein.inverseHessianPair_symm line 90
  8. lemma OAI.AffineBernstein.inverseHessianPair_self_nonneg line 101
  9. def OAI.AffineBernstein.affineDetBarrier line 110

    Source documentation

    Literal log-determinant barrier. On a negative section its logarithmic cutoff is exactly log (-u), because the real logarithm uses absolute value.

    def affineDetBarrier {n : ℕ} (u : Space n → ℝ) (β γ : ℝ) (x : Space n) : ℝ :=
…

    Mentions: OAI.AffineBernstein.Space

  10. lemma OAI.AffineBernstein.contDiffOn_affineDetBarrier line 113
  11. lemma OAI.AffineBernstein.dirDeriv_affineDetBarrier line 121
  12. lemma OAI.AffineBernstein.inverseHessianTrace_affineDetBarrier line 143