OAI/Analysis/Unitarizability/FiniteSigns.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Dixmier.FiniteSigns.sign line 17
2. def OAI.Dixmier.FiniteSigns.value line 19
3. theorem OAI.Dixmier.FiniteSigns.sign_mgf line 21
4. theorem OAI.Dixmier.FiniteSigns.sign_mgf_le line 33
5. theorem OAI.Dixmier.FiniteSigns.value_smul line 43
6. theorem OAI.Dixmier.FiniteSigns.upper_tail_mgf line 48

   Source documentation

   Finite Markov inequality for the equiprobable sign space.

   theorem upper_tail_mgf (a : J → ℝ) {t u : ℝ} (ht : 0 ≤ t) :
       (((univ.filter fun σ : J → Bool => u < value a σ).card : ℕ) : ℝ) * Real.exp (t*u) ≤
         (2 : ℝ) ^ Fintype.card J * Real.exp (t^2 * (∑ j, (a j)^2) / 2) := by
   …

   Mentions: OAI.Dixmier.FiniteSigns.value

7. theorem OAI.Dixmier.FiniteSigns.upper_tail line 65

   Source documentation

   One-sided sign tail for coefficients of total squared size 1/k.

   theorem upper_tail (a : J → ℝ) {k u : ℝ} (hk : 0 < k) (hu : 0 < u)
       (ha : ∑ j, (a j)^2 = 1/k) :
       (((univ.filter fun σ : J → Bool => u < value a σ).card : ℕ) : ℝ) ≤
         (2 : ℝ) ^ Fintype.card J * Real.exp (-k*u^2/2) := by
   …

   Mentions: OAI.Dixmier.FiniteSigns.value

8. theorem OAI.Dixmier.FiniteSigns.value_neg line 76
9. theorem OAI.Dixmier.FiniteSigns.two_sided_tail line 80

   Source documentation

   The two-sided sign-tail bound as a fraction of the finite equiprobable sign space.

   theorem two_sided_tail (a : J → ℝ) {k u : ℝ} (hk : 0 < k) (hu : 0 < u)
       (ha : ∑ j, (a j)^2 = 1/k) :
       (((univ.filter fun σ : J → Bool => u < |value a σ|).card : ℕ) : ℝ) /
         (2 : ℝ)^Fintype.card J ≤ 2 * Real.exp (-k*u^2/2) := by
   …

   Mentions: OAI.Dixmier.FiniteSigns.value