Theorem: fderiv_innerSL_apply (ForML/IntegralAgainst.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ fderiv ℝ (fun x => (innerSL ℝ) x) x = innerSL ℝ
Tactic:
refine ContinuousLinearMap.ext ?_
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ∀ (x_1 : E), (fderiv ℝ (fun x => (innerSL ℝ) x) x) x_1 = (innerSL ℝ) x_1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ∀ (x_1 : E), (fderiv ℝ (fun x => (innerSL ℝ) x) x) x_1 = (innerSL ℝ) x_1
Tactic:
intro u
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ (fderiv ℝ (fun x => (innerSL ℝ) x) x) u = (innerSL ℝ) u

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ (fderiv ℝ (fun x => (innerSL ℝ) x) x) u = (innerSL ℝ) u
Tactic:
refine ContinuousLinearMap.ext ?_
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ ∀ (x_1 : E), ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) x_1 = ((innerSL ℝ) u) x_1

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
⊢ ∀ (x_1 : E), ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) x_1 = ((innerSL ℝ) u) x_1
Tactic:
intro dx
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) dx = ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((fderiv ℝ (fun x => (innerSL ℝ) x) x) u) dx = ((innerSL ℝ) u) dx
Tactic:
rw [fderiv_clm_apply (differentiableAt_const _) differentiableAt_id']
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x) +
          (ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x)
        u)
      dx =
    ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x) +
          (ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x)
        u)
      dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.add_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u +
        ((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u)
      dx =
    ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u +
        ((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u)
      dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.add_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u) dx =
    ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((ContinuousLinearMap.flip (fderiv ℝ (fun x => innerSL ℝ) x)) x) u) dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.flip_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((fderiv ℝ (fun x => innerSL ℝ) x) u) x) dx =
    ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx +
      (((fderiv ℝ (fun x => innerSL ℝ) x) u) x) dx =
    ((innerSL ℝ) u) dx
Tactic:
rw [fderiv_const]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + (((0 x) u) x) dx = ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + (((0 x) u) x) dx = ((innerSL ℝ) u) dx
Tactic:
change _ + 0 = _
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + 0 = ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (fderiv ℝ (fun x => x) x)) u) dx + 0 = ((innerSL ℝ) u) dx
Tactic:
simp
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (ContinuousLinearMap.id ℝ E)) u) dx = ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((ContinuousLinearMap.comp (innerSL ℝ) (ContinuousLinearMap.id ℝ E)) u) dx = ((innerSL ℝ) u) dx
Tactic:
rw [ContinuousLinearMap.comp_apply]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((innerSL ℝ) ((ContinuousLinearMap.id ℝ E) u)) dx = ((innerSL ℝ) u) dx

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u dx : E
⊢ ((innerSL ℝ) ((ContinuousLinearMap.id ℝ E) u)) dx = ((innerSL ℝ) u) dx
Tactic:
rfl
State after:
no goals