internlm/Lean-Github huggingface dataset:
Theorem: ContinuousLinearMap.opNorm_apply_le
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖((apply 𝕜 G) u) c‖ ≤ ‖u‖ * ‖c‖
Tactic:
rw [apply_apply, mul_comm]
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖c u‖ ≤ ‖c‖ * ‖u‖
Theorem: ContinuousLinearMap.opNorm_apply_le
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
u : E
c : E →L[𝕜] G
⊢ ‖c u‖ ≤ ‖c‖ * ‖u‖
Tactic:
exact le_opNorm c u
Proof state after:
no goals
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ContinuousLinearMap.comp (c y) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
conv => lhs; arg 1; arg 3; intro y; rw [← ContinuousLinearMap.compL_apply]
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ((ContinuousLinearMap.compL 𝕜 E F G) (c y)) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n (fun y => ((ContinuousLinearMap.compL 𝕜 E F G) (c y)) u) x‖ ≤ ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
change ‖iteratedFDeriv 𝕜 n (fun y => (ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G) u).comp (ContinuousLinearMap.compL 𝕜 E F G) (c y)) x‖ ≤ _
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n
        (fun y =>
          (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G))
            (c y))
        x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖iteratedFDeriv 𝕜 n
        (fun y =>
          (ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G))
            (c y))
        x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
refine le_trans (norm_iteratedFDeriv_clm_const_apply hc) ?_
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ *
      ‖iteratedFDeriv 𝕜 n (fun y => c y) x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ *
      ‖iteratedFDeriv 𝕜 n (fun y => c y) x‖ ≤
    ‖u‖ * ‖iteratedFDeriv 𝕜 n c x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ ≤ ‖u‖
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖ContinuousLinearMap.comp ((ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u) (ContinuousLinearMap.compL 𝕜 E F G)‖ ≤ ‖u‖
Tactic:
refine le_trans (ContinuousLinearMap.opNorm_comp_le _ _) ?_
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖
Tactic:
rw [← mul_one ‖u‖]
Proof state after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖ * 1
Theorem: norm_iteratedFDeriv_clm_comp_const
Proof state before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : ℕ
c : α → F →L[𝕜] G
u : E →L[𝕜] F
x : α
hc : ContDiff 𝕜 (↑n) c
⊢ ‖(ContinuousLinearMap.apply 𝕜 (E →L[𝕜] G)) u‖ * ‖ContinuousLinearMap.compL 𝕜 E F G‖ ≤ ‖u‖ * 1
Tactic:
exact mul_le_mul ContinuousLinearMap.opNorm_apply_le (ContinuousLinearMap.norm_compL_le 𝕜 E F G) (norm_nonneg _) (norm_nonneg _)
Proof state after:
no goals
Theorem: ContinuousLinearMap.proj_single_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x : φ i
⊢ (proj i) ((single i) x) = x
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.proj_comp_single
Proof state before:
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
⊢ comp (proj i) (single i) = id R (φ i)
Tactic:
ext
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x✝ : φ i
⊢ (comp (proj i) (single i)) x✝ = (id R (φ i)) x✝
Theorem: ContinuousLinearMap.proj_comp_single
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x✝ : φ i
⊢ (comp (proj i) (single i)) x✝ = (id R (φ i)) x✝
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.pi_apply'
Proof state before:
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
⊢ pi f = ∑ i : ι, comp (single i) (f i)
Tactic:
ext
Proof state after:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi f) x✝¹ x✝ = (∑ i : ι, comp (single i) (f i)) x✝¹ x✝
Theorem: ContinuousLinearMap.pi_apply'
Proof state before:
case h.h
𝕜 : Type u_1
ι : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
M : Type u_3
inst✝⁸ : TopologicalSpace M
inst✝⁷ : AddCommGroup M
φ : ι → Type u_4
inst✝⁶ : (i : ι) → TopologicalSpace (φ i)
inst✝⁵ : (i : ι) → AddCommGroup (φ i)
inst✝⁴ : ∀ (i : ι), TopologicalAddGroup (φ i)
inst✝³ : NormedField 𝕜
inst✝² : Module 𝕜 M
inst✝¹ : (i : ι) → Module 𝕜 (φ i)
inst✝ : ∀ (i : ι), ContinuousConstSMul 𝕜 (φ i)
f : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi f) x✝¹ x✝ = (∑ i : ι, comp (single i) (f i)) x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.pi_eq_sum_single_proj
Proof state before:
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
⊢ pi = ⇑(∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i))
Tactic:
ext
Proof state after:
case h.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
x✝² : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi x✝²) x✝¹ x✝ = ((∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i)) x✝²) x✝¹ x✝
Theorem: ContinuousLinearMap.pi_eq_sum_single_proj
Proof state before:
case h.h.h
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
x✝² : (i : ι) → M →L[𝕜] φ i
x✝¹ : M
x✝ : ι
⊢ (pi x✝²) x✝¹ x✝ = ((∑ i : ι, comp ((compL 𝕜 M (φ i) ((i : ι) → φ i)) (single i)) (proj i)) x✝²) x✝¹ x✝
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.continuous_pi
Proof state before:
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => pi fun i => f i x
Tactic:
simp only [← piL_apply]
Proof state after:
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piL 𝕜 M fun i => φ i) fun i => f i x
Theorem: ContinuousLinearMap.continuous_pi
Proof state before:
𝕜 : Type u_1
ι : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : DecidableEq ι
X : Type u_3
inst✝⁵ : TopologicalSpace X
M : Type u_4
inst✝⁴ : NormedAddCommGroup M
φ : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (φ i)
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 M
inst✝ : (i : ι) → NormedSpace 𝕜 (φ i)
f : (i : ι) → X → M →L[𝕜] φ i
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piL 𝕜 M fun i => φ i) fun i => f i x
Tactic:
refine .clm_apply continuous_const (_root_.continuous_pi hf)
Proof state after:
no goals
Theorem: ContinuousLinearMap.continuous_piMap
Proof state before:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => piMap fun i => f i x
Tactic:
simp only [← piMapL_apply]
Proof state after:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piMapL 𝕜 (fun i => E) fun i => F) fun i => f i x
Theorem: ContinuousLinearMap.continuous_piMap
Proof state before:
𝕜 : Type u_1
inst✝¹⁵ : NontriviallyNormedField 𝕜
ι : Type u_2
inst✝¹⁴ : Fintype ι
inst✝¹³ : DecidableEq ι
X : Type u_3
inst✝¹² : TopologicalSpace X
D : ι → Type u_4
inst✝¹¹ : (i : ι) → NormedAddCommGroup (D i)
inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (D i)
D₁ : ι → Type u_5
inst✝⁹ : (i : ι) → NormedAddCommGroup (D₁ i)
inst✝⁸ : (i : ι) → NormedSpace 𝕜 (D₁ i)
E : Type u_6
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
E₁ : Type u_7
inst✝⁵ : NormedAddCommGroup E₁
inst✝⁴ : NormedSpace 𝕜 E₁
F : Type u_8
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_9
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : ι → X → E →L[𝕜] F
hf : ∀ (i : ι), Continuous fun x => f i x
⊢ Continuous fun x => (piMapL 𝕜 (fun i => E) fun i => F) fun i => f i x
Tactic:
exact .clm_apply continuous_const (_root_.continuous_pi hf)
Proof state after:
no goals
Theorem: HasFDerivAt.hasFPiDerivAt
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ HasFPiDerivAt i f (ContinuousLinearMap.comp f' (ContinuousLinearMap.single i)) x
Tactic:
rw [HasFPiDerivAt]
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun y => f (Function.update x i y)) (ContinuousLinearMap.comp f' (ContinuousLinearMap.single i)) (x i)
Theorem: HasFDerivAt.hasFPiDerivAt
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun y => f (Function.update x i y)) (ContinuousLinearMap.comp f' (ContinuousLinearMap.single i)) (x i)
Tactic:
refine HasFDerivAt.comp _ (by simpa) ?_
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun y => Function.update x i y) (ContinuousLinearMap.single i) (x i)
Theorem: HasFDerivAt.hasFPiDerivAt
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun y => Function.update x i y) (ContinuousLinearMap.single i) (x i)
Tactic:
refine HasFDerivAt.congr_fderiv (hasFDerivAt_update _ _) ?_
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (M i))) = ContinuousLinearMap.single i
Theorem: HasFDerivAt.hasFPiDerivAt
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
⊢ ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (M i))) = ContinuousLinearMap.single i
Tactic:
ext m j
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
m : M i
j : ι
⊢ (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (M i)))) m j = (ContinuousLinearMap.single i) m j
Theorem: HasFDerivAt.hasFPiDerivAt
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
m : M i
j : ι
⊢ (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (M i)))) m j = (ContinuousLinearMap.single i) m j
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
i : ι
f : ((i : ι) → M i) → F
f' : ((i : ι) → M i) →L[𝕜] F
x : (i : ι) → M i
hf : HasFDerivAt f f' x
m : M i
j : ι
⊢ (Pi.single i (ContinuousLinearMap.id 𝕜 (M i)) j) m = Pi.single i m j