internlm/Lean-Github huggingface dataset:
Theorem: orderedIteratedFPiDeriv_succ_eq_comp_right
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ((i : ι) → M i) → F
js : Fin (n + 1) → ι
⊢ orderedIteratedFPiDeriv 𝕜 js f =
    ⇑(continuousMultilinearCurryRightEquiv 𝕜 (fun i => M (js i)) F) ∘
      orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f)
Tactic:
ext x m
Proof state after:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ((i : ι) → M i) → F
js : Fin (n + 1) → ι
x : (i : ι) → M i
m : (i : Fin (n + 1)) → M (js i)
⊢ (orderedIteratedFPiDeriv 𝕜 js f x) m =
    ((⇑(continuousMultilinearCurryRightEquiv 𝕜 (fun i => M (js i)) F) ∘
          orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f))
        x)
      m
Theorem: orderedIteratedFPiDeriv_succ_eq_comp_right
Proof state before:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ((i : ι) → M i) → F
js : Fin (n + 1) → ι
x : (i : ι) → M i
m : (i : Fin (n + 1)) → M (js i)
⊢ (orderedIteratedFPiDeriv 𝕜 js f x) m =
    ((⇑(continuousMultilinearCurryRightEquiv 𝕜 (fun i => M (js i)) F) ∘
          orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f))
        x)
      m
Tactic:
rw [orderedIteratedFPiDeriv_succ_apply_right]
Proof state after:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ((i : ι) → M i) → F
js : Fin (n + 1) → ι
x : (i : ι) → M i
m : (i : Fin (n + 1)) → M (js i)
⊢ ((orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f) x) (Fin.init m)) (m (Fin.last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv 𝕜 (fun i => M (js i)) F) ∘
          orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f))
        x)
      m
Theorem: orderedIteratedFPiDeriv_succ_eq_comp_right
Proof state before:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ((i : ι) → M i) → F
js : Fin (n + 1) → ι
x : (i : ι) → M i
m : (i : Fin (n + 1)) → M (js i)
⊢ ((orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f) x) (Fin.init m)) (m (Fin.last n)) =
    ((⇑(continuousMultilinearCurryRightEquiv 𝕜 (fun i => M (js i)) F) ∘
          orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last n)) f))
        x)
      m
Tactic:
rfl
Proof state after:
no goals
Theorem: orderedIteratedFPiDeriv_one_apply
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
js : Fin 1 → ι
x : (i : ι) → M i
m : (i : Fin 1) → M (js i)
⊢ (orderedIteratedFPiDeriv 𝕜 js f x) m = (fpideriv 𝕜 (js 0) f x) (m 0)
Tactic:
rw [orderedIteratedFPiDeriv_succ_apply_right]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
js : Fin 1 → ι
x : (i : ι) → M i
m : (i : Fin 1) → M (js i)
⊢ ((orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last 0)) f) x) (Fin.init m)) (m (Fin.last 0)) =
    (fpideriv 𝕜 (js 0) f x) (m 0)
Theorem: orderedIteratedFPiDeriv_one_apply
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
js : Fin 1 → ι
x : (i : ι) → M i
m : (i : Fin 1) → M (js i)
⊢ ((orderedIteratedFPiDeriv 𝕜 (Fin.init js) (fpideriv 𝕜 (js (Fin.last 0)) f) x) (Fin.init m)) (m (Fin.last 0)) =
    (fpideriv 𝕜 (js 0) f x) (m 0)
Tactic:
rw [orderedIteratedFPiDeriv_zero_apply]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
js : Fin 1 → ι
x : (i : ι) → M i
m : (i : Fin 1) → M (js i)
⊢ (fpideriv 𝕜 (js (Fin.last 0)) f x) (m (Fin.last 0)) = (fpideriv 𝕜 (js 0) f x) (m 0)
Theorem: orderedIteratedFPiDeriv_one_apply
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
js : Fin 1 → ι
x : (i : ι) → M i
m : (i : Fin 1) → M (js i)
⊢ (fpideriv 𝕜 (js (Fin.last 0)) f x) (m (Fin.last 0)) = (fpideriv 𝕜 (js 0) f x) (m 0)
Tactic:
rfl
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
⊢ curryLeft (compContinuousLinearMap g f) =
    ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
      (ContinuousLinearMap.comp (curryLeft g) (f 0))
Tactic:
ext u m
Proof state after:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ ((curryLeft (compContinuousLinearMap g f)) u) m =
    ((ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
          (ContinuousLinearMap.comp (curryLeft g) (f 0)))
        u)
      m
Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap
Proof state before:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ ((curryLeft (compContinuousLinearMap g f)) u) m =
    ((ContinuousLinearMap.comp (compContinuousLinearMapL fun i => f (Fin.succ i))
          (ContinuousLinearMap.comp (curryLeft g) (f 0)))
        u)
      m
Tactic:
simp
Proof state after:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (g fun i => (f i) (Fin.cons u m i)) = g (Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i))
Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap
Proof state before:
case h.H
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (g fun i => (f i) (Fin.cons u m i)) = g (Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i))
Tactic:
congr
Proof state after:
case h.H.h.e_6.h
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (fun i => (f i) (Fin.cons u m i)) = Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i)
Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap
Proof state before:
case h.H.h.e_6.h
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
⊢ (fun i => (f i) (Fin.cons u m i)) = Fin.cons ((f 0) u) fun i => (f (Fin.succ i)) (m i)
Tactic:
ext i
Proof state after:
case h.H.h.e_6.h.h
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
i : Fin (n + 1)
⊢ (f i) (Fin.cons u m i) = Fin.cons ((f 0) u) (fun i => (f (Fin.succ i)) (m i)) i
Theorem: ContinuousMultilinearMap.curryLeft_compContinuousLinearMap
Proof state before:
case h.H.h.e_6.h.h
ι : Type u_1
𝕜 : Type u_2
inst✝¹² : Fintype ι
inst✝¹¹ : DecidableEq ι
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁷ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝³ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝² : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
M₁' : Fin (n + 1) → Type u_7
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁' i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁' i)
g : ContinuousMultilinearMap 𝕜 M₁' F
f : (i : Fin (n + 1)) → M₁ i →L[𝕜] M₁' i
u : M₁ 0
m : (i : Fin n) → M₁ (Fin.succ i)
i : Fin (n + 1)
⊢ (f i) (Fin.cons u m i) = Fin.cons ((f 0) u) (fun i => (f (Fin.succ i)) (m i)) i
Tactic:
refine Fin.cases ?_ ?_ i <;> simp
Proof state after:
no goals
Theorem: continuousMultilinearCurryLeftEquiv_curryLeft
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
⊢ (continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g) = g
Tactic:
ext x
Proof state after:
case H
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
x : (i : Fin (Nat.succ n)) → M₁ i
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g)) x = g x
Theorem: continuousMultilinearCurryLeftEquiv_curryLeft
Proof state before:
case H
ι : Type u_1
𝕜 : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝⁵ : (i : ι) → NormedAddCommGroup (M i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
n : ℕ
M₁ : Fin (n + 1) → Type u_6
inst✝¹ : (i : Fin (n + 1)) → NormedAddCommGroup (M₁ i)
inst✝ : (i : Fin (n + 1)) → NormedSpace 𝕜 (M₁ i)
g : ContinuousMultilinearMap 𝕜 M₁ F
x : (i : Fin (Nat.succ n)) → M₁ i
⊢ ((continuousMultilinearCurryLeftEquiv 𝕜 M₁ F) (ContinuousMultilinearMap.curryLeft g)) x = g x
Tactic:
simp
Proof state after:
no goals
Theorem: HasFTaylorSeriesUpTo.hasFDerivAt_orderedIteratedFPiDeriv'
Proof state before:
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
n : ℕ
hf : HasFTaylorSeriesUpTo (↑n + 1) f f'
js : Fin n → ι
x : (i : ι) → M i
⊢ HasFDerivAt (orderedIteratedFPiDeriv 𝕜 js f)
    (ContinuousLinearMap.comp
      (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
      (ContinuousMultilinearMap.curryLeft (f' x (n + 1))))
    x
Tactic:
induction n generalizing x with
| zero =>
  rw [orderedIteratedFPiDeriv_zero_eq_comp]
  rw [LinearIsometryEquiv.comp_hasFDerivAt_iff']
  refine HasFDerivAt.congr_fderiv (hf.hasFDerivAt (by simp) x) ?_
  ext m
  simp only [continuousMultilinearCurryFin1_apply, Nat.zero_eq, LinearIsometryEquiv.symm_symm,
    ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
    Function.comp_apply, ContinuousMultilinearMap.compContinuousLinearMapL_apply,
    continuousMultilinearIsEmptyEquiv_apply,
    ContinuousMultilinearMap.compContinuousLinearMap_apply, Pi.zero_apply, map_zero,
    ContinuousMultilinearMap.curryLeft_apply]
  congr
  funext i
  rw [Fin.eq_zero i]
  simp only [Fin.cons_zero]
  have : (0 : Fin 1) = Fin.last 0 := rfl
  simp [this]
| succ n ih =>
  rw [← hasFTaylorSeriesUpToOn_univ_iff] at hf
  rw [hasFTaylorSeriesUpToOn_succ_iff_left] at hf
  rcases hf with ⟨hf_pred, hf_diff, _⟩
  rw [hasFTaylorSeriesUpToOn_univ_iff] at hf_pred
  simp at hf_diff
  specialize @ih hf_pred
  rw [orderedIteratedFPiDeriv_succ_eq_comp_left]
  conv =>
    arg 1; intro y; arg 2; intro x
    rw [fpideriv_eq_fderiv_comp_single ih.differentiableAt]
    rw [ih.fderiv]
    rw [ContinuousLinearMap.comp_assoc]
    simp [Fin.tail]
    rw [← ContinuousMultilinearMap.curryLeft_compContinuousLinearMap (f' x (n + 1)) (fun i => ContinuousLinearMap.single (js i))]
  simp
  simp_rw [← ContinuousMultilinearMap.compContinuousLinearMapL_apply]
  refine ((ContinuousLinearMap.hasFDerivAt _).comp _ (hf_diff _)).congr_fderiv ?_
  ext m v
  simp
Proof state after:
no goals
Theorem: HasFTaylorSeriesUpTo.hasFDerivAt_orderedIteratedFPiDeriv'
Proof state before:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
hf : HasFTaylorSeriesUpTo (↑Nat.zero + 1) f f'
js : Fin Nat.zero → ι
x : (i : ι) → M i
⊢ HasFDerivAt (orderedIteratedFPiDeriv 𝕜 js f)
    (ContinuousLinearMap.comp
      (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
      (ContinuousMultilinearMap.curryLeft (f' x (Nat.zero + 1))))
    x
Tactic:
rw [orderedIteratedFPiDeriv_zero_eq_comp]
Proof state after:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
hf : HasFTaylorSeriesUpTo (↑Nat.zero + 1) f f'
js : Fin Nat.zero → ι
x : (i : ι) → M i
⊢ HasFDerivAt (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
    (ContinuousLinearMap.comp
      (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
      (ContinuousMultilinearMap.curryLeft (f' x (Nat.zero + 1))))
    x
Theorem: HasFTaylorSeriesUpTo.hasFDerivAt_orderedIteratedFPiDeriv'
Proof state before:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
hf : HasFTaylorSeriesUpTo (↑Nat.zero + 1) f f'
js : Fin Nat.zero → ι
x : (i : ι) → M i
⊢ HasFDerivAt (⇑(LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F)) ∘ f)
    (ContinuousLinearMap.comp
      (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
      (ContinuousMultilinearMap.curryLeft (f' x (Nat.zero + 1))))
    x
Tactic:
rw [LinearIsometryEquiv.comp_hasFDerivAt_iff']
Proof state after:
case zero
ι : Type u_1
𝕜 : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
M : ι → Type u_4
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace 𝕜 (M i)
F : Type u_5
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) → FormalMultilinearSeries 𝕜 ((i : ι) → M i) F
hf : HasFTaylorSeriesUpTo (↑Nat.zero + 1) f f'
js : Fin Nat.zero → ι
x : (i : ι) → M i
⊢ HasFDerivAt f
    (ContinuousLinearMap.comp
      (↑(ContinuousLinearEquiv.mk
          (LinearIsometryEquiv.symm
              (LinearIsometryEquiv.symm (continuousMultilinearIsEmptyEquiv 𝕜 (fun i => M (js i)) F))).toLinearEquiv))
      (ContinuousLinearMap.comp
        (ContinuousMultilinearMap.compContinuousLinearMapL fun i => ContinuousLinearMap.single (js i))
        (ContinuousMultilinearMap.curryLeft (f' x (Nat.zero + 1)))))
    x