α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
have h₁ := ceil_lt_add_one hx.le
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
have h₂ : 1 - x ≤ 2 - ⌈x⌉₊ := by
  rw [_root_.le_sub_iff_add_le]
  apply (add_le_add_left h₁.le _).trans_eq
  rw [← add_assoc, sub_add_cancel]
  linarith
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (2 - ↑⌈x⌉₊) / (x + 1)
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) < exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
refine' lt_of_le_of_lt _ (div_lt_div_of_lt_left (exp_pos _) (cast_pos.2 <| ceil_pos.2 hx) h₁)
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (1 - x) / (x + 1)
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (2 - ↑⌈x⌉₊) / (x + 1)
refine' le_trans _ (div_le_div_of_le_of_nonneg (exp_le_exp.2 h₂) <| add_nonneg hx.le zero_le_one)
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ exp (x + 1)
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ exp (-2 * x) ≤ exp (1 - x) / (x + 1)
rw [le_div_iff (add_pos hx zero_lt_one), ← le_div_iff' (exp_pos _), ← exp_sub, neg_mul,
  sub_neg_eq_add, two_mul, sub_add_add_cancel, add_comm _ x]
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ x + 1 + 1
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ exp (x + 1)
refine' le_trans _ (add_one_le_exp_of_nonneg <| add_nonneg hx.le zero_le_one)
no goals
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ x + 1 + 1
exact le_add_of_nonneg_right zero_le_one
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + ↑⌈x⌉₊ ≤ 2
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x ≤ 2 - ↑⌈x⌉₊
rw [_root_.le_sub_iff_add_le]
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + (x + 1) = 2
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + ↑⌈x⌉₊ ≤ 2
apply (add_le_add_left h₁.le _).trans_eq
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 + 1 = 2
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 - x + (x + 1) = 2
rw [← add_assoc, sub_add_cancel]
no goals
α : Type ?u.690738
β : Type ?u.690741
n d k N : ℕ
x✝ : Fin n → ℕ
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
⊢ 1 + 1 = 2
linarith