awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
⊢ (1 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2

Tactic:
have hy₄ : (1 - y) * (1 + y) = 1 - y ^ 2 := by ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
hy₄ : (1 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2
refine_2 :
  (1 - y - (-y + -1)) * (HPow.hPow (β := ℕ) y 2 - 1) -
      (1 - HPow.hPow (β := ℕ) y 2) * 2 * (HPow.hPow (β := ℕ) y 2 ^ n - 1) =
    (HPow.hPow (β := ℕ) y 2 - 1) * 2 * HPow.hPow (β := ℕ) y 2 ^ n
⊢ 1 / 2 *
        ((1 * (1 - y) - (1 + y) * -1) / HPow.hPow (β := ℕ) (1 - y) 2 /
          HDiv.hDiv (α := ℝ → ℝ) (β := ℝ → ℝ) (HAdd.hAdd (α := ℝ) 1) (HSub.hSub (α := ℝ) 1) y) -
      ∑ i ∈ Finset.range n, (↑(2 * i + 1) : ℝ) * y ^ (2 * i + 1 - 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) =
    HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)

Tactic:
simp [this, field, geom_sum_eq hy₃, hy₄, sub_ne_zero_of_ne, hy₃.symm]

Premises used: geom_sum_eq, Ne.symm, sub_ne_zero_of_ne
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
y : ℝ
n : ℕ
hy₁ : -1 < y
hy₂ : y < 1
this :
  Eq (α := ℝ)
    (∑ i ∈ Finset.range n, (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) * y ^ (2 * i) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1))
    (∑ i ∈ Finset.range n, HPow.hPow (β := ℕ) y 2 ^ i)
hy₃ : HPow.hPow (β := ℕ) y 2 ≠ 1
hy₄ : (1 - y) * (1 + y) = 1 - HPow.hPow (β := ℕ) y 2
⊢ (1 - y - (-y + -1)) * (HPow.hPow (β := ℕ) y 2 - 1) -
      (1 - HPow.hPow (β := ℕ) y 2) * 2 * (HPow.hPow (β := ℕ) y 2 ^ n - 1) =
    (HPow.hPow (β := ℕ) y 2 - 1) * 2 * HPow.hPow (β := ℕ) y 2 ^ n

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
⊢ -1 < -|x|

Tactic:
simp [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
⊢ Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1

Tactic:
have hI : Icc (-|x|) |x| ⊆ Ioo (-1 : ℝ) 1 := Icc_subset_Ioo (by simp [h]) h
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
⊢ -1 < y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
⊢ y < 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
y : ℝ
hy : Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y
⊢ HasDerivAt F (F' y) y

Tactic:
exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)

Premises used: Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
⊢ ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y

Tactic:
have A : ∀ y ∈ Ioo (-1 : ℝ) 1, HasDerivAt F (F' y) y := by
    intro y hy
    exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
⊢ HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
have : y ^ 2 ≤ x ^ 2 := sq_le_sq.2 (abs_le.2 hy)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
⊢ ‖F' y‖ = HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2|

Tactic:
simp [F']
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) y 2

Tactic:
simpa [abs_lt] using hI hy

Premises used: abs_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
rw rw₁ :
  HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
⊢ HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2| = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)

Tactic:
rw [abs_of_pos (by simpa [abs_lt] using hI hy)]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
hd : 0 < 1 - HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) ≤ HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
gcongr ?_ ^ n / (1 - ?_)

Premises used: HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
⊢ 0 < 1 - HPow.hPow (β := ℕ) x 2

Tactic:
simpa [abs_lt] using h

Premises used: abs_lt
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
⊢ HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2) ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ Set.Icc (-|x|) |x|
this : HPow.hPow (β := ℕ) y 2 ≤ HPow.hPow (β := ℕ) x 2
n₁ : ‖F' y‖ = HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2|
n₂ :
  HPow.hPow (β := ℕ) y 2 ^ n / |1 - HPow.hPow (β := ℕ) y 2| = HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
n₃ :
  HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2) ≤ HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2)
n₄ : HPow.hPow (β := ℕ) x 2 ^ n / (1 - HPow.hPow (β := ℕ) x 2) ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
calc
      ‖F' y‖ = (y ^ 2) ^ n / |1 - y ^ 2| := by simp [F']
      _ = (y ^ 2) ^ n / (1 - y ^ 2) := by rw [abs_of_pos (by simpa [abs_lt] using hI hy)]
      _ ≤ (x ^ 2) ^ n / (1 - x ^ 2) := by gcongr ?_ ^ n / (1 - ?_); simpa [abs_lt] using h
      _ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := by simp [pow_mul]

Premises used: HMul.hMul, HSub.hSub, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
⊢ ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
have B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := fun y hy ↦ by
    have : y ^ 2 ≤ x ^ 2 := sq_le_sq.2 (abs_le.2 hy)
    calc
      ‖F' y‖ = (y ^ 2) ^ n / |1 - y ^ 2| := by simp [F']
      _ = (y ^ 2) ^ n / (1 - y ^ 2) := by rw [abs_of_pos (by simpa [abs_lt] using hI hy)]
      _ ≤ (x ^ 2) ^ n / (1 - x ^ 2) := by gcongr ?_ ^ n / (1 - ?_); simpa [abs_lt] using h
      _ ≤ |x| ^ (2 * n) / (1 - x ^ 2) := by simp [pow_mul]
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ 0 ∈ Set.Icc (-|x|) |x|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ x ∈ Set.Icc (-|x|) |x|

Tactic:
simp [le_abs_self, neg_le, neg_le_abs x]

Premises used: neg_le, le_abs_self, neg_le_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
⊢ ‖F x - F 0‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2) * ‖x - 0‖

Tactic:
have C : ‖F x - F 0‖ ≤ |x| ^ (2 * n) / (1 - x ^ 2) * ‖x - 0‖ :=
    (convex_Icc (-|x|) |x|).norm_image_sub_le_of_norm_hasDerivWithin_le
      (fun y hy ↦ (A _ (hI hy)).hasDerivWithinAt) B
      (by simp) (by simp [le_abs_self, neg_le, neg_le_abs x])
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h : |x| < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
hI : Set.Icc (-|x|) |x| ⊆ Set.Ioo (-1) 1
A : ∀ (y : ℝ), Membership.mem (γ := Set ℝ) (Set.Ioo (-1) 1) y → HasDerivAt F (F' y) y
B : ∀ y ∈ Set.Icc (-|x|) |x|, ‖F' y‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2)
C : ‖F x - F 0‖ ≤ |x| ^ (2 * n) / (1 - HPow.hPow (β := ℕ) x 2) * ‖x - 0‖
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
simpa [F, pow_succ, div_mul_eq_mul_div] using C

Premises used: pow_succ, div_mul_eq_mul_div
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
y : ℝ
hy : y ∈ Set.Icc 0 x
⊢ -1 < y

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
y : ℝ
hy : y ∈ Set.Icc 0 x
⊢ y < 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
y : ℝ
hy : y ∈ Set.Icc 0 x
⊢ HasDerivAt F (F' y) y

Tactic:
exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)

Premises used: Real.hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
⊢ ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y

Tactic:
have A : ∀ y ∈ Icc 0 x, HasDerivAt F (F' y) y := by
    intro y hy
    exact hasDerivAt_half_log_one_add_div_one_sub_sub_sum_range _ (by grind) (by grind)
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
this : MonotoneOn F (Set.Icc 0 x)
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
simpa [F] using this ⟨le_rfl, h₀⟩ ⟨h₀, le_rfl⟩ h₀

Premises used: le_rfl, And.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
suffices : MonotoneOn F (Set.Icc 0 x)
⊢ ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1) ≤ 1 / 2 * log ((1 + x) / (1 - x))

Tactic:
suffices MonotoneOn F (Icc 0 x) by simpa [F] using this ⟨le_rfl, h₀⟩ ⟨h₀, le_rfl⟩ h₀
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
⊢ MonotoneOn F (Set.Icc 0 x)

Tactic:
monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc 0 x)
    (fun y hy ↦ (A y hy).continuousAt.continuousWithinAt)
    (fun y hy ↦ (A y (interior_subset hy)).hasDerivWithinAt) ?_

Premises used: HasDerivAt.hasDerivWithinAt, interior_subset, ContinuousAt.continuousWithinAt, monotoneOn_of_hasDerivWithinAt_nonneg, convex_Icc, HasDerivAt.continuousAt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
refine : ∀ x_1 ∈ interior (Set.Icc 0 x), 0 ≤ F' x_1
⊢ MonotoneOn F (Set.Icc 0 x)

Tactic:
refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Icc 0 x)
    (fun y hy ↦ (A y hy).continuousAt.continuousWithinAt)
    (fun y hy ↦ (A y (interior_subset hy)).hasDerivWithinAt) ?_

Premises used: HasDerivAt.hasDerivWithinAt, interior_subset, ContinuousAt.continuousWithinAt, monotoneOn_of_hasDerivWithinAt_nonneg, convex_Icc, HasDerivAt.continuousAt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : y ∈ interior (Set.Icc 0 x)
⊢ 0 < y ∧ y < x

Tactic:
simp only [interior_Icc, Set.mem_Ioo] at hy

Premises used: Set.mem_Ioo, interior_Icc
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) x 2

Tactic:
simp [abs_of_nonneg h₀, h.le]

Premises used: LT.lt.le, abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
⊢ 1 - HPow.hPow (β := ℕ) x 2 ≤ 1 - HPow.hPow (β := ℕ) y 2

Tactic:
sub_le_sub_left (pow_le_pow_left₀ hy.1.le hy.2.le 2) 1

Premises used: pow_le_pow_left₀, LT.lt.le, And.right, And.left, sub_le_sub_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
x₁ : 0 ≤ 1 - HPow.hPow (β := ℕ) x 2
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) y 2

Tactic:
calc
    0 ≤ 1 - x ^ 2 := by simp [abs_of_nonneg h₀, h.le]
    _ ≤ 1 - y ^ 2 := sub_le_sub_left (pow_le_pow_left₀ hy.1.le hy.2.le 2) 1

Premises used: pow_le_pow_left₀, LT.lt.le, And.right, And.left, sub_le_sub_left, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
⊢ 0 ≤ 1 - HPow.hPow (β := ℕ) y 2

Tactic:
have : 0 ≤ 1 - y ^ 2 := by calc
    0 ≤ 1 - x ^ 2 := by simp [abs_of_nonneg h₀, h.le]
    _ ≤ 1 - y ^ 2 := sub_le_sub_left (pow_le_pow_left₀ hy.1.le hy.2.le 2) 1
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
F : (x : ℝ) → ℝ :=
  fun (x : ℝ) ↦
    1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)
F' : (y : ℝ) → ℝ := fun (y : ℝ) ↦ HPow.hPow (β := ℕ) y 2 ^ n / (1 - HPow.hPow (β := ℕ) y 2)
A : ∀ y ∈ Set.Icc 0 x, HasDerivAt F (F' y) y
y : ℝ
hy : 0 < y ∧ y < x
this : 0 ≤ 1 - HPow.hPow (β := ℕ) y 2
⊢ 0 ≤ F' y

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
rwa rwa₁ rwa₂ rwa₃ : x < 1
⊢ |x| < 1

Tactic:
rwa [abs_of_nonneg h₀]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Log.Deriv
Goal:
x : ℝ
h₀ : 0 ≤ x
h : x < 1
n : ℕ
⊢ |1 / 2 * log ((1 + x) / (1 - x)) - ∑ i ∈ Finset.range n, x ^ (2 * i + 1) / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)| ≤
    |x| ^ (2 * n + 1) / (1 - HPow.hPow (β := ℕ) x 2)

Tactic:
have h₁ := sum_range_sub_log_div_le (by rwa [abs_of_nonneg h₀]) n