Theorem: periodic_deriv (Carleson/Theorem1_1/Approximation.lean)

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
⊢ Function.Periodic (deriv f) T
Tactic:
intro x
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
⊢ deriv f (x + T) = deriv f x
Tactic:
set g : 𝕜 → 𝕜 := fun x ↦ x + T with gdef
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ deriv f (x + T) = deriv f x
Tactic:
have diff_g : Differentiable 𝕜 g := by
  apply differentiable_id.add_const
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv f (x + T) = deriv f x
Tactic:
have : deriv (f ∘ g) x = ((deriv f) ∘ g) x := by
  calc deriv (f ∘ g) x
    _ = deriv g x • deriv f (g x) := deriv.scomp x (diff_f.differentiable (by norm_num)).differentiableAt diff_g.differentiableAt
    _ = deriv f (g x) := by rw [gdef, deriv_add_const, deriv_id'']; simp
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ g) x = (deriv f ∘ g) x
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ g) x = (deriv f ∘ g) x
⊢ deriv f (x + T) = deriv f x
Tactic:
rw [gdef] at this
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = (deriv f ∘ fun x => x + T) x
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = (deriv f ∘ fun x => x + T) x
⊢ deriv f (x + T) = deriv f x
Tactic:
simp at this
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ deriv f (x + T) = deriv f x

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ deriv f (x + T) = deriv f x
Tactic:
convert this.symm
State after:
case h.e'_3.h.e'_6
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ f = f ∘ fun x => x + T

State before:
case h.e'_3.h.e'_6
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
⊢ f = f ∘ fun x => x + T
Tactic:
ext y
State after:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = (f ∘ fun x => x + T) y

State before:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = (f ∘ fun x => x + T) y
Tactic:
simp
State after:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = f (y + T)

State before:
case h.e'_3.h.e'_6.h
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
this : deriv (f ∘ fun x => x + T) x = deriv f (x + T)
y : 𝕜
⊢ f y = f (y + T)
Tactic:
exact (periodic_f y).symm
State after:
no goals

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
⊢ Differentiable 𝕜 g
Tactic:
apply differentiable_id.add_const
State after:
no goals

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv (f ∘ g) x = (deriv f ∘ g) x
Tactic:
calc deriv (f ∘ g) x
  _ = deriv g x • deriv f (g x) := deriv.scomp x (diff_f.differentiable (by norm_num)).differentiableAt diff_g.differentiableAt
  _ = deriv f (g x) := by rw [gdef, deriv_add_const, deriv_id'']; simp
State after:
no goals

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ 1 ≤ 1
Tactic:
norm_num
State after:
no goals

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ deriv g x • deriv f (g x) = deriv f (g x)
Tactic:
rw [gdef, deriv_add_const, deriv_id'']
State after:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ (fun x => 1) x • deriv f ((fun x => x + T) x) = deriv f ((fun x => x + T) x)

State before:
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
F : Type
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
T : 𝕜
diff_f : ContDiff 𝕜 1 f
periodic_f : Function.Periodic f T
x : 𝕜
g : 𝕜 → 𝕜 := fun x => x + T
gdef : g = fun x => x + T
diff_g : Differentiable 𝕜 g
⊢ (fun x => 1) x • deriv f ((fun x => x + T) x) = deriv f ((fun x => x + T) x)
Tactic:
simp
State after:
no goals