Documentation

Marginis.KjosHanssen2010

Permutations of the integers induce only the trivial automorphism of the Turing degrees #

by Kjos-Hanssen, Bjørn

https://arxiv.org/pdf/1408.2850.pdf

source
theorem page5_display3_equals2 (b : ℝ) :
2 ^ (b + 1) * 4 ^ (b - 1) = 2 ^ (3 * b - 1)

https://arxiv.org/pdf/1408.2850.pdf Page 5 3rd displayed equation Second "equals" sign

source
theorem page7_display4_lt2 (b : ℝ) (c : ℝ) (h : b < c) :
2 ^ (-b) + 2 ^ (-c) < 2 ^ (-(b - 1))

https://arxiv.org/pdf/1408.2850.pdf Page 7 4th displayed equation Second "<" sign

source
theorem bound_of_nonneg (p : ℝ) :
0 ≤ 4 * p * (p - 1) + 1
source
theorem numerator_bound (p : ℝ) :
4 * (p * (1 - p)) ≤ 1
source
theorem le_div {a : ℝ} {b : ℝ} {c : ℝ} (ha : 0 < a) (g : a * b ≤ c) :
b ≤ c / a
source
theorem the_bound (p : ℝ) :
p * (1 - p) ≤ 1 / 4
source
theorem mul_self_bound {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
p * p ≤ 1
source
theorem sq_bound {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
p ^ 2 ≤ 1
source
theorem cube_bound {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
p ^ 3 ≤ 1
source
theorem cube_bound' {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
(1 - p) ^ 3 ≤ 1
source
theorem paper_bound {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
(1 - p) ^ 3 + p ^ 3 ≤ 2
source
theorem paper_bound' {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
p * (1 - p) * ((1 - p) ^ 3 + p ^ 3) ≤ 1 / 2
source
theorem paper_bound'' {p : ℝ} (h0 : 0 ≤ p) (h1 : p ≤ 1) :
(1 - p) ^ 4 * p + p ^ 4 * (1 - p) ≤ 1 / 2

Page 8 5th displayed equation Inequality

source
theorem choose_two (n : ℕ) :
2 * n.choose 2 = n * (n - 1)
source
theorem page7_bottom (n : ℕ) :
n.choose 2 * Nat.choose 4 2 = 3 * n * (n - 1)
source
noncomputable def one_on (P : Prop) :
ℕ
Equations
Instances For
    source
    noncomputable def oneOn (S : Set ℕ) (x : ℕ) :
    ℕ
    Equations
    Instances For
      source
      noncomputable def oneOn' {X : Type u_1} (S : Set X) (x : X) :
      ℕ
      Equations
      • oneOn' S x = S.indicator (fun (x : X) => 1) x
      Instances For
        source
        theorem one_one_inequality_indicator (x : ℕ) (a : ℕ) :
        a * (Set.Ici a).indicator (fun (x : ℕ) => 1) x ≤ x
        source
        theorem one_on_inequality (x : ℕ) (a : ℕ) :
        a * one_on (a ≤ x) ≤ x
        source
        theorem real_one_on_inequality (x : ℝ) (a : ℝ) (g : 0 ≤ x) :
        a * ↑(one_on (a ≤ x)) ≤ x
        source
        theorem real_one_on_inequality' (x : ℝ) (a : ℝ) (g : 0 ≤ x) :
        (Set.Ici a).indicator (fun (x : ℝ) => a) x ≤ x