internlm/Lean-Github huggingface dataset:
Theorem: ContinuousMultilinearMap.compContinuousLinearMap_update
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ (compContinuousLinearMap g (Function.update f j b)) x = (q b) x
Tactic:
rw [compContinuousLinearMap_apply, ← compContinuousLinearMapContinuousMultilinear_apply]
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ((((compContinuousLinearMapContinuousMultilinear 𝕜 (fun i => E i) E₁ G) fun i => Function.update f j b i) g) fun i =>
      x i) =
    (q b) x
Theorem: ContinuousMultilinearMap.compContinuousLinearMap_update
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
j : ι
b : E j →L[𝕜] E₁ j
q : (E j →L[𝕜] E₁ j) →L[𝕜] ContinuousMultilinearMap 𝕜 E G
x : (i : ι) → E i
⊢ ((((compContinuousLinearMapContinuousMultilinear 𝕜 (fun i => E i) E₁ G) fun i => Function.update f j b i) g) fun i =>
      x i) =
    (q b) x
Tactic:
sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap_fin
Proof state before:
𝕜 : 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'
n : ℕ
E : Fin n → Type u_9
inst✝³ : (i : Fin n) → NormedAddCommGroup (E i)
inst✝² : (i : Fin n) → NormedSpace 𝕜 (E i)
E₁ : Fin n → Type u_10
inst✝¹ : (i : Fin n) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin n) → NormedSpace 𝕜 (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : Fin n) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : Fin n, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
Tactic:
induction n with
| zero =>
  simp [Subsingleton.elim _ (0 : (i : Fin 0) → E i →L[𝕜] E₁ i), hasFDerivAt_const]
| succ n =>
  sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap_fin
Proof state before:
case zero
𝕜 : 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'
E : Fin Nat.zero → Type u_9
inst✝³ : (i : Fin Nat.zero) → NormedAddCommGroup (E i)
inst✝² : (i : Fin Nat.zero) → NormedSpace 𝕜 (E i)
E₁ : Fin Nat.zero → Type u_10
inst✝¹ : (i : Fin Nat.zero) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin Nat.zero) → NormedSpace 𝕜 (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : Fin Nat.zero) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : Fin Nat.zero, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
Tactic:
simp [Subsingleton.elim _ (0 : (i : Fin 0) → E i →L[𝕜] E₁ i), hasFDerivAt_const]
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap_fin
Proof state before:
case succ
𝕜 : 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'
n : ℕ
n_ih✝ :
  ∀ {E : Fin n → Type u_9} [inst : (i : Fin n) → NormedAddCommGroup (E i)] [inst_1 : (i : Fin n) → NormedSpace 𝕜 (E i)]
    {E₁ : Fin n → Type u_10} [inst_2 : (i : Fin n) → NormedAddCommGroup (E₁ i)]
    [inst_3 : (i : Fin n) → NormedSpace 𝕜 (E₁ i)] {g : ContinuousMultilinearMap 𝕜 E₁ G}
    {f : (i : Fin n) → E i →L[𝕜] E₁ i},
    HasFDerivAt (fun f => compContinuousLinearMap g f)
      (∑ i : Fin n, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
E : Fin (Nat.succ n) → Type u_9
inst✝³ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E i)
inst✝² : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E i)
E₁ : Fin (Nat.succ n) → Type u_10
inst✝¹ : (i : Fin (Nat.succ n)) → NormedAddCommGroup (E₁ i)
inst✝ : (i : Fin (Nat.succ n)) → NormedSpace 𝕜 (E₁ i)
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : Fin (Nat.succ n)) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : Fin (Nat.succ n),
      ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
    f
Tactic:
sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
Tactic:
have (x : (i : ι) → E i) := (g.hasFDerivAt (fun i ↦ f i (x i))).hasFDerivAtFilter (le_refl _)
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ HasFDerivAt (fun f => compContinuousLinearMap g f)
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) f
Tactic:
refine HasFDerivAtFilter.of_isLittleO ?_
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ (fun x' =>
      compContinuousLinearMap g x' - compContinuousLinearMap g f -
        (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
          (x' - f)) =o[nhds f]
    fun x' => x' - f
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ (fun x' =>
      compContinuousLinearMap g x' - compContinuousLinearMap g f -
        (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
          (x' - f)) =o[nhds f]
    fun x' => x' - f
Tactic:
rw [Asymptotics.isLittleO_iff]
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
        ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
              (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
                (x - f)‖ ≤
          c * ‖x - f‖
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
⊢ ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
        ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
              (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
                (x - f)‖ ≤
          c * ‖x - f‖
Tactic:
intro c hc
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
    ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
          (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
            (x - f)‖ ≤
      c * ‖x - f‖
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
    ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
          (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i))
            (x - f)‖ ≤
      c * ‖x - f‖
Tactic:
simp
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
    ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
          (∑ x_1 : ι, compContinuousLinearMap g (Function.update f x_1 (x x_1)) -
            Finset.univ.card • compContinuousLinearMap g f)‖ ≤
      c * ‖x - f‖
Theorem: ContinuousMultilinearMap.hasFDerivAt_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
this :
  ∀ (x : (i : ι) → E i),
    HasFDerivAtFilter (⇑g) (linearDeriv g fun i => (f i) (x i)) (fun i => (f i) (x i)) (nhds fun i => (f i) (x i))
c : ℝ
hc : 0 < c
⊢ ∀ᶠ (x : (i : ι) → E i →L[𝕜] E₁ i) in nhds f,
    ‖compContinuousLinearMap g x - compContinuousLinearMap g f -
          (∑ x_1 : ι, compContinuousLinearMap g (Function.update f x_1 (x x_1)) -
            Finset.univ.card • compContinuousLinearMap g f)‖ ≤
      c * ‖x - f‖
Tactic:
sorry
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ fderiv 𝕜 (fun f => compContinuousLinearMap g f) f =
    ∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ ∀ (x : (i : ι) → E i →L[𝕜] E₁ i),
    (fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) x =
      (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) x
Theorem: ContinuousMultilinearMap.fderiv_compContinuousLinearMap
Proof state before:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f : (i : ι) → E i →L[𝕜] E₁ i
⊢ ∀ (x : (i : ι) → E i →L[𝕜] E₁ i),
    (fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) x =
      (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) x
Tactic:
intro df
Proof state after:
𝕜 : 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'
g : ContinuousMultilinearMap 𝕜 E₁ G
f df : (i : ι) → E i →L[𝕜] E₁ i
⊢ (fderiv 𝕜 (fun f => compContinuousLinearMap g f) f) df =
    (∑ i : ι, ContinuousLinearMap.comp (compContinuousLinearMapUpdate g i f) (ContinuousLinearMap.proj i)) df