internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => (compContinuousLinearMap g y) x) f) df =
    (∑ j : ι, compContinuousLinearMap g (Function.update f j (df j))) x
Tactic:
simp only [sum_apply, compContinuousLinearMap_apply]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => g fun i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
⊢ (fderiv 𝕜 (fun y => g fun i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
have : HasFDerivAt (𝕜 := 𝕜) (fun (f : (i : ι) → E i →L[𝕜] E₁ i) (i : ι) ↦ f i (x i))
    (.pi fun i ↦ .comp (.apply 𝕜 (E₁ i) (x i)) (.proj i)) f :=
  hasFDerivAt_pi.mpr fun i ↦ by
    simp only [← ContinuousLinearMap.proj_apply (R := 𝕜) (φ := fun i ↦ E i →L[𝕜] E₁ i) i]
    simp only [← ContinuousLinearMap.apply_apply (x i)]
    simp only [← ContinuousLinearMap.comp_apply]
    exact ContinuousLinearMap.hasFDerivAt _
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (fderiv 𝕜 (fun y => g fun i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (fderiv 𝕜 (fun y => g fun i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
rw [← Function.comp_def g]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (fderiv 𝕜 (⇑g ∘ fun y i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (fderiv 𝕜 (⇑g ∘ fun y i => (y i) (x i)) f) df = ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
rw [((ContinuousMultilinearMap.hasFDerivAt g _).comp f this).fderiv]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (ContinuousLinearMap.comp (linearDeriv g fun i => (f i) (x i))
        (ContinuousLinearMap.pi fun i =>
          ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)))
      df =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ (ContinuousLinearMap.comp (linearDeriv g fun i => (f i) (x i))
        (ContinuousLinearMap.pi fun i =>
          ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i)))
      df =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
simp only [ContinuousLinearMap.strongUniformity_topology_eq, ContinuousLinearMap.coe_comp',
  ContinuousLinearMap.coe_pi', Function.comp_apply, ContinuousLinearMap.proj_apply,
  ContinuousLinearMap.apply_apply]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ((linearDeriv g fun i => (f i) (x i)) fun i => (df i) (x i)) =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ((linearDeriv g fun i => (f i) (x i)) fun i => (df i) (x i)) =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
rw [linearDeriv_apply]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ∑ i : ι, g (Function.update (fun i => (f i) (x i)) i ((df i) (x i))) =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ∑ i : ι, g (Function.update (fun i => (f i) (x i)) i ((df i) (x i))) =
    ∑ x_1 : ι, g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
refine Finset.sum_congr rfl ?_
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ∀ x_1 ∈ Finset.univ,
    g (Function.update (fun i => (f i) (x i)) x_1 ((df x_1) (x x_1))) =
      g fun i => (Function.update f x_1 (df x_1) i) (x i)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
⊢ ∀ x_1 ∈ Finset.univ,
    g (Function.update (fun i => (f i) (x i)) x_1 ((df x_1) (x x_1))) =
      g fun i => (Function.update f x_1 (df x_1) i) (x i)
Tactic:
intro i _
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ g (Function.update (fun i => (f i) (x i)) i ((df i) (x i))) = g fun i_1 => (Function.update f i (df i) i_1) (x i_1)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ g (Function.update (fun i => (f i) (x i)) i ((df i) (x i))) = g fun i_1 => (Function.update f i (df i) i_1) (x i_1)
Tactic:
refine congrArg g ?_
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ Function.update (fun i => (f i) (x i)) i ((df i) (x i)) = fun i_1 => (Function.update f i (df i) i_1) (x i_1)
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap_apply
Proof state before:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ Function.update (fun i => (f i) (x i)) i ((df i) (x i)) = fun i_1 => (Function.update f i (df i) i_1) (x i_1)
Tactic:
rw [Function.update_eq_iff]
Proof state after:
case H
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
α : Type u_2
inst✝¹³ : NormedAddCommGroup α
inst✝¹² : NormedSpace 𝕜 α
D : Type u_3
inst✝¹¹ : NormedAddCommGroup D
inst✝¹⁰ : NormedSpace 𝕜 D
ι : Type u_4
inst✝⁹ : Fintype ι
inst✝⁸ : DecidableEq ι
E : ι → Type u_5
inst✝⁷ : (i : ι) → NormedAddCommGroup (E i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)
E₁ : ι → Type u_6
inst✝⁵ : (i : ι) → NormedAddCommGroup (E₁ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E₁ i)
G : Type u_7
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type u_8
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
df : (i : ι) → E i →L[𝕜] E₁ i
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
h : DifferentiableAt 𝕜 (fun f => compContinuousLinearMap g f) f
x : (i : ι) → E i
this :
  HasFDerivAt (fun f i => (f i) (x i))
    (ContinuousLinearMap.pi fun i =>
      ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E₁ i)) (x i)) (ContinuousLinearMap.proj i))
    f
i : ι
a✝ : i ∈ Finset.univ
⊢ (df i) (x i) = (Function.update f i (df i) i) (x i) ∧
    ∀ (x_1 : ι), x_1 ≠ i → (f x_1) (x x_1) = (Function.update f i (df i) x_1) (x x_1)