OAI/Analysis/AffineBernstein/DualDetPhase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.dualDetPhase line 18

   Source documentation

   The pullback of the dual determinant phase to primal coordinates.

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

   Mentions: OAI.AffineBernstein.Space

2. lemma OAI.AffineBernstein.dualDetPhase_eq_exp line 21
3. lemma OAI.AffineBernstein.dualDetPhase_pos line 32
4. lemma OAI.AffineBernstein.continuousOn_dualDetPhase line 38
5. lemma OAI.AffineBernstein.dualDetPhase_peak_bound line 50