awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
⊢ 0 < deriv (qaryEntropy q) p
have this : LE.le (α := ℝ) 2 (↑q : ℝ)
Tactic: have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ 0 < deriv (qaryEntropy q) p
have zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
Tactic: have zero_le_qinv : 0 < (q : ℝ)⁻¹ := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ 0 < 1 - p
have simp : p < 1
Tactic: simp only [sub_pos]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ p < 1
have p_lt_1_minus_qinv : p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
Tactic: have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
p_lt_1_minus_qinv : p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ p < 1
have linarith : 1 ≤ p →
  HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ +
        (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
      (1 - p) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
⊢ 0 < deriv (qaryEntropy q) p
have this₁ : 0 < 1 - p
Tactic: have : 0 < 1 - p := by
      simp only [sub_pos]
      have p_lt_1_minus_qinv : p < 1 - (q : ℝ)⁻¹ := by
        simp_all only [inv_pos, interior_Icc, mem_Ioo, one_div]
      linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)))
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
⊢ 0 < deriv (qaryEntropy q) p
have hp₁ : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
Tactic: simp only [one_div, interior_Icc, mem_Ioo] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ p ≠ 0
have linarith : p = 0 → 0 - p + (p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ 0 < deriv (qaryEntropy q) p
have rw : 0 < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
Tactic: rw [deriv_qaryEntropy (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
rw : 0 < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
⊢ 0 < deriv (qaryEntropy q) p
have rw₁ : p ≠ 1
Tactic: rw [deriv_qaryEntropy (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ 0 < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p
have simp : log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p)
Tactic: simp only [sub_pos, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≠ 0
have linarith : HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0 →
  HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹) + (0 - p) +
        (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
      (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ 1 - p ≠ 0
have linarith : 1 - p = 0 →
  HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ +
        (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
      (1 - p - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p)
have rw : log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
Tactic: rw [← log_mul (by linarith) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
have x : Membership.mem (γ := Set ℝ) (Ioi 0) (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
Tactic: apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
x : Membership.mem (γ := Set ℝ) (Ioi 0) (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
⊢ log p < log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p))
have a : p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
Tactic: apply Real.strictMonoOn_log (mem_Ioi.mpr hp.1)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ 0 < HSub.hSub (α := ℝ) (↑q : ℝ) 1
have linarith : HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≤ 0 →
  HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 0 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹) + (0 - p) +
        (1 * p - (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹)) +
      (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
⊢ p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
have qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
Tactic: have qpos : 0 < (q : ℝ) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1
have h : HSub.hSub (α := ℝ) (↑q : ℝ) 1 = (↑q : ℝ) * HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
Tactic: convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
have this₁ : (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1
Tactic: have : q * p < q - 1 := by
          convert! mul_lt_mul_of_pos_left hp.2 qpos using 1
          simp only [mul_sub, mul_one, isUnit_iff_ne_zero, ne_eq, ne_of_gt qpos, not_false_eq_true,
            IsUnit.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p2 : ℝ
hp2 : p2 ∈ Icc 0 (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ))
p1le2 : p1 < p2
p : ℝ
this_1 : LE.le (α := ℝ) 2 (↑q : ℝ)
zero_le_qinv : LT.lt (α := ℝ) 0 (↑q : ℝ)⁻¹
this_2 : 0 < 1 - p
hp : 0 < p ∧ p < HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
this : (↑q : ℝ) * p < HSub.hSub (α := ℝ) (↑q : ℝ) 1
⊢ p < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
have linarith : HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) ≤ p →
  (↑q : ℝ) * p - HSub.hSub (α := ℝ) (↑q : ℝ) 1 + (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) - p) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
⊢ qaryEntropy q p2 < qaryEntropy q p1
have apply : ContinuousOn (qaryEntropy q) (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
Tactic: apply strictAntiOn_of_deriv_neg (convex_Icc (1 - 1 / (q : ℝ)) 1) _ _ hp1 hp2 p1le2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
apply : ContinuousOn (qaryEntropy q) (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
⊢ qaryEntropy q p2 < qaryEntropy q p1
have apply₁ : ∀ x ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1), deriv (qaryEntropy q) x < 0
Tactic: apply strictAntiOn_of_deriv_neg (convex_Icc (1 - 1 / (q : ℝ)) 1) _ _ hp1 hp2 p1le2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
⊢ deriv (qaryEntropy q) p < 0
have this : LE.le (α := ℝ) 2 (↑q : ℝ)
Tactic: have : 2 ≤ (q : ℝ) := Nat.ofNat_le_cast.mpr qLe2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ LT.lt (α := ℝ) 1 (↑q : ℝ)
have linarith : LE.le (α := ℝ) (↑q : ℝ) 1 → -1 + HSub.hSub (α := ℝ) 2 (↑q : ℝ) + HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
⊢ deriv (qaryEntropy q) p < 0
have qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
Tactic: have qinv_lt_1 : (q : ℝ)⁻¹ < 1 := inv_lt_one_of_one_lt₀ (by linarith)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
⊢ deriv (qaryEntropy q) p < 0
have zero_lt_1_sub_p : 0 < 1 - p
Tactic: have zero_lt_1_sub_p : 0 < 1 - p := by simp_all only [sub_pos, interior_Icc, mem_Ioo]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
hp : p ∈ interior (Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1)
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
⊢ deriv (qaryEntropy q) p < 0
have hp₁ : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
Tactic: simp only [one_div, interior_Icc, mem_Ioo] at hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ p ≠ 0
have linarith : p = 0 →
  HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1 +
        (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
      (p - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ deriv (qaryEntropy q) p < 0
have rw : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p < 0
Tactic: rw [deriv_qaryEntropy (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
rw : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p < 0
⊢ deriv (qaryEntropy q) p < 0
have rw₁ : p ≠ 1
Tactic: rw [deriv_qaryEntropy (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) - log p < 0
have simp : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) < log p
Tactic: simp only [sub_neg, gt_iff_lt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 ≠ 0
have linarith : HSub.hSub (α := ℝ) (↑q : ℝ) 1 = 0 →
  HSub.hSub (α := ℝ) 2 (↑q : ℝ) + (HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1) + (0 - (1 - p)) +
        (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
      (HSub.hSub (α := ℝ) (↑q : ℝ) 1 - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ 1 - p ≠ 0
have linarith : 1 - p = 0 → 0 - (1 - p) + (1 - p - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1) + log (1 - p) < log p
have rw : log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)) < log p
Tactic: rw [← log_mul (by linarith) (by linarith)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ 0 < HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)
have nlinarith : HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) ≤ 0 →
  0 - (1 - p) + (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) - 0) + (0 - HSub.hSub (α := ℝ) 2 (↑q : ℝ) * (0 - (1 - p))) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)) < log p
have x : Membership.mem (γ := Set ℝ) (Ioi 0) p
Tactic: apply Real.strictMonoOn_log (mem_Ioi.mpr (show 0 < (↑q - 1) * (1 - p) by nlinarith))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
x : Membership.mem (γ := Set ℝ) (Ioi 0) p
⊢ log (HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p)) < log p
have a : HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) < p
Tactic: apply Real.strictMonoOn_log (mem_Ioi.mpr (show 0 < (↑q - 1) * (1 - p) by nlinarith))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ 0 < p
have linarith : p ≤ 0 →
  HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - HMul.hMul (α := ℝ) 1 1 +
        (HMul.hMul (α := ℝ) 1 1 - HMul.hMul (α := ℝ) 1 (↑q : ℝ)⁻¹ - 1 * p) +
      (p - 0) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) < p
have qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
Tactic: have qpos : 0 < (q : ℝ) := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (goal)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 * (1 - p) < p
have a : HAdd.hAdd (α := ℝ) (-1) (↑q : ℝ) - (↑q : ℝ) * p + p < p
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.BinaryEntropy (hypothesis)
Goal:
q : ℕ
qLe2 : 2 ≤ q
p1 : ℝ
hp1 : p1 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p2 : ℝ
hp2 : p2 ∈ Icc (1 - HDiv.hDiv (α := ℝ) 1 (↑q : ℝ)) 1
p1le2 : p1 < p2
p : ℝ
this : LE.le (α := ℝ) 2 (↑q : ℝ)
qinv_lt_1 : LT.lt (α := ℝ) (↑q : ℝ)⁻¹ 1
zero_lt_1_sub_p : 0 < 1 - p
hp : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ < p ∧ p < 1
qpos : LT.lt (α := ℝ) 0 (↑q : ℝ)
⊢ HSub.hSub (α := ℝ) (↑q : ℝ) 1 < p * (↑q : ℝ)
have h1 : HSub.hSub (α := ℝ) 1 (↑q : ℝ)⁻¹ * (↑q : ℝ) < p * (↑q : ℝ)
Tactic: have h1 := mul_lt_mul_of_pos_right hp.1 qpos