-- 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:
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:
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
⊢ (∫ (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 hv₁ (x) : HasDerivAt v₁ (v₁' x) x := (hasDerivAt_mul_const θ).sin

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
hu₁ : ∀ (x : ℝ), HasDerivAt u₁ (u₁' x) x
hv₁ : ∀ (x : ℝ), HasDerivAt v₁ (v₁' 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)
⊢ (∫ (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 : ℝ) : ℝ := sin (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 * θ)
⊢ (∫ (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
θ : ℝ
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
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) + 2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, u₂' x * v₂ x =
    -(2 * 2 * ((↑n + 1) * (0 ^ n * cos θ))) + 2 * (↑n + 1) * (2 * ↑n + 1) * I n θ - 4 * (↑n + 1) * ↑n * I (n - 1) θ

Tactic:
have (x) : u₂' x = (2 * n + 1) * f x ^ n - 2 * n * f x ^ (n - 1) := by
  cases n with
  | zero => simp [u₂']
  | succ n => ring!

Result:
case convert_2.convert_2
θ : ℝ
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)
⊢ -(2 * (↑n + 1) * (2 * (0 ^ n * cos θ))) + 2 * (↑n + 1) * ∫ (x : ℝ) in -1 ..1, u₂' x * v₂ x =
    -(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₁'
hv₁d : Continuous v₁'
hu₂d : Continuous u₂'
hv₂d : Continuous v₂'
hu₁_eval_one : u₁ 1 = 0
⊢ (1 - (-1) ^ 2) ^ (n + 1) = 0

Tactic:
simp

Result:
no goals