-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
While it is most natural to give the recursive formula for `I (n + 2) θ`, as well as give the second
base case of `I 1 θ`, it is in fact more convenient to give the recursive formula for `I (n + 1) θ`
in terms of `I n θ` and `I (n - 1) θ` (note the natural subtraction!).
Despite the usually inconvenient subtraction, this in fact allows deducing both of the above facts
with significantly fewer analysis computations.
In addition, note the `0 ^ n` on the right hand side - this is intentional, and again allows
combining the proof of the "usual" recursion formula and the base case `I 1 θ`.
-/
private lemma recursion' (n : ℕ) :
    I (n + 1) θ * θ ^ 2 = - (2 * 2 * ((n + 1) * (0 ^ n * cos θ))) +
      2 * (n + 1) * (2 * n + 1) * I n θ - 4 * (n + 1) * n * I (n - 1) θ

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
let v₁' (x : ℝ) : ℝ := cos (x * θ) * θ

Result:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Proof state:
case convert_2.convert_2.hf
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ IntervalIntegrable (fun x => (2 * ↑n + 1) * (f x ^ n * v₂ x)) volume (-1) 1

case convert_2.convert_2.hg
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
this✝ : ∀ (x : ℝ), u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)
this : Continuous v₂
⊢ IntervalIntegrable (fun x => 2 * ↑n * (f x ^ (n - 1) * v₂ x)) volume (-1) 1

Tactic:
all_goals exact Continuous.intervalIntegrable (by fun_prop) _ _

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
⊢ u₂' x = (2 * ↑n + 1) * f x ^ n - 2 * ↑n * f x ^ (n - 1)

Tactic:
cases n with
| zero => simp [u₂']
| succ n => ring!

Result:
no goals

Proof state:
case zero
θ : ℝ
f : ℝ → ℝ := fun x => 1 - x ^ 2
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hv₁d : Continuous v₁'
hv₂d : Continuous v₂'
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' x) x
hv₂ : ∀ (x : ℝ), HasDerivAt v₂ (v₂' x) x
x : ℝ
u₁ : ℝ → ℝ := fun x => f x ^ (0 + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑0 + 1) * x * f x ^ 0)
u₂ : ℝ → ℝ := fun x => x * f x ^ 0
u₂' : ℝ → ℝ := fun x => f x ^ 0 - 2 * ↑0 * x ^ 2 * f x ^ (0 - 1)
hu₁d : Continuous u₁'
hu₂d : Continuous u₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ 0 * cos θ)
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hu₂ : ∀ (x : ℝ), HasDerivAt u₂ (u₂' x) x
⊢ u₂' x = (2 * ↑0 + 1) * f x ^ 0 - 2 * ↑0 * f x ^ (0 - 1)

Tactic:
simp [u₂']

Result:
no goals

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have hf (x) : HasDerivAt f (- 2 * x) x := by
  convert (hasDerivAt_pow 2 x).const_sub 1 using 1
  simp

Result:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
hu₁_eval_neg_one : u₁ (-1) = 0
t : u₂ 1 * v₂ 1 - u₂ (-1) * v₂ (-1) = 2 * (0 ^ n * cos θ)
hf : ∀ (x : ℝ), HasDerivAt f (-2 * x) x
⊢ (∫ (x : ℝ) in -1 ..1, (1 - x ^ 2) ^ (n + 1) * cos (x * θ)) * θ ^ 2 =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Proof state:
θ : ℝ
n : ℕ
f : ℝ → ℝ := fun x => 1 - x ^ 2
u₁ : ℝ → ℝ := fun x => f x ^ (n + 1)
u₁' : ℝ → ℝ := fun x => -(2 * (↑n + 1) * x * f x ^ n)
v₁ : ℝ → ℝ := fun x => sin (x * θ)
v₁' : ℝ → ℝ := fun x => cos (x * θ) * θ
u₂ : ℝ → ℝ := fun x => x * f x ^ n
u₂' : ℝ → ℝ := fun x => f x ^ n - 2 * ↑n * x ^ 2 * f x ^ (n - 1)
v₂ : ℝ → ℝ := fun x => cos (x * θ)
v₂' : ℝ → ℝ := fun x => -sin (x * θ) * θ
hfd : Continuous f
hu₁d : Continuous u₁'
⊢ Continuous v₁'

Tactic:
fun_prop

Result:
no goals