OAI/Analysis/AffineBernstein/DetBarrierPhase.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.posSemidef_det_le_trace_pow line 16
2. def OAI.AffineBernstein.affineDetPhase line 30

   Source documentation

   Continuous phase whose logarithm is the maximum-principle barrier on a negative section; the phase vanishes, rather than diverging, on its boundary.

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

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.affineDetPhase_eq_exp line 33
4. lemma OAI.AffineBernstein.affineDetPhase_pos line 44
5. lemma OAI.AffineBernstein.continuousOn_affineDetPhase line 50
6. lemma OAI.AffineBernstein.affineDetPhase_peak_bound line 60