internlm/Lean-Github huggingface dataset:
Theorem: ContinuousLinearMap.coprod_eq_comp_fst_add_comp_snd
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ →L[R] F
g : M₂ →L[R] F
⊢ coprod f g = comp f (fst R M₁ M₂) + comp g (snd R M₁ M₂)
Tactic:
ext x <;> simp [coprod_apply, comp_apply]
Proof state after:
no goals
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ (coprodL R M₁ M₂ F) f = coprod f.1 f.2
Tactic:
refine ContinuousLinearMap.ext ?_
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ ∀ (x : M₁ × M₂), ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ ∀ (x : M₁ × M₂), ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Tactic:
intro x
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((coprodL R M₁ M₂ F) f) x = (coprod f.1 f.2) x
Tactic:
simp [coprodL]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂) +
          bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂))
        f)
      x =
    f.1 x.1 + f.2 x.2
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂) +
          bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂))
        f)
      x =
    f.1 x.1 + f.2 x.2
Tactic:
rw [add_apply, add_apply]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂)) f) x +
      ((bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂)) f) x =
    f.1 x.1 + f.2 x.2
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((bilinearComp (flip (apply R F)) (fst R (M₁ →L[R] F) (M₂ →L[R] F)) (fst R M₁ M₂)) f) x +
      ((bilinearComp (flip (apply R F)) (snd R (M₁ →L[R] F) (M₂ →L[R] F)) (snd R M₁ M₂)) f) x =
    f.1 x.1 + f.2 x.2
Tactic:
rw [bilinearComp_apply, bilinearComp_apply]
Proof state after:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((flip (apply R F)) ((fst R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((fst R M₁ M₂) x) +
      ((flip (apply R F)) ((snd R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((snd R M₁ M₂) x) =
    f.1 x.1 + f.2 x.2
Theorem: ContinuousLinearMap.coprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
x : M₁ × M₂
⊢ ((flip (apply R F)) ((fst R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((fst R M₁ M₂) x) +
      ((flip (apply R F)) ((snd R (M₁ →L[R] F) (M₂ →L[R] F)) f)) ((snd R M₁ M₂) x) =
    f.1 x.1 + f.2 x.2
Tactic:
simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.invcoprod_fst_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ × M₂ →L[R] F
x : M₁
⊢ (invcoprod f).1 x = f (x, 0)
Tactic:
simp [invcoprod]
Proof state after:
no goals
Theorem: ContinuousLinearMap.invcoprod_snd_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ × M₂ →L[R] F
x : M₂
⊢ (invcoprod f).2 x = f (0, x)
Tactic:
simp [invcoprod]
Proof state after:
no goals
Theorem: ContinuousLinearMap.coprod_invcoprod_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ × M₂ →L[R] F
⊢ coprod (invcoprod f).1 (invcoprod f).2 = f
Tactic:
ext x <;> simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.invcoprod_coprod_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : (M₁ →L[R] F) × (M₂ →L[R] F)
⊢ invcoprod (coprod f.1 f.2) = f
Tactic:
ext x <;> simp
Proof state after:
no goals
Theorem: ContinuousLinearMap.invcoprodL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ × M₂ →L[R] F
⊢ (invcoprodL R M₁ M₂ F) f = invcoprod f
Tactic:
ext x <;> simp [invcoprodL]
Proof state after:
no goals
Theorem: ContinuousLinearMap.updateL_apply
Proof state before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
⊢ (updateL R M i) (x, xi) = Function.update x i xi
Tactic:
ext j
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ (updateL R M i) (x, xi) j = Function.update x i xi j
Theorem: ContinuousLinearMap.updateL_apply
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ (updateL R M i) (x, xi) j = Function.update x i xi j
Tactic:
simp [updateL]
Proof state after:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ Pi.single i xi j + (if j = i then 0 else comp (proj j) (fst R ((i : ι) → M i) (M i))) (x, xi) =
    Function.update x i xi j
Theorem: ContinuousLinearMap.updateL_apply
Proof state before:
case h
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
⊢ Pi.single i xi j + (if j = i then 0 else comp (proj j) (fst R ((i : ι) → M i) (M i))) (x, xi) =
    Function.update x i xi j
Tactic:
by_cases h : j = i <;> simp [h]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ Pi.single i xi j = Function.update x i xi j
Theorem: ContinuousLinearMap.updateL_apply
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ Pi.single i xi j = Function.update x i xi j
Tactic:
rw [h]
Proof state after:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ Pi.single i xi i = Function.update x i xi i
Theorem: ContinuousLinearMap.updateL_apply
Proof state before:
case pos
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
i : ι
x : (i : ι) → M i
xi : M i
j : ι
h : j = i
⊢ Pi.single i xi i = Function.update x i xi i
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
suffices : ‖e.symm.toContinuousLinearMap (e x)‖ ≤ ‖e.symm.toContinuousLinearMap‖ * ‖e x‖
Proof state after:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖

case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
. simpa
Proof state after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
refine le_trans (ContinuousLinearMap.le_opNorm _ _) ?_
Proof state after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
refine mul_le_mul_of_nonneg_left ?_ (norm_nonneg _)
Proof state after:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖e x‖ ≤ ‖e x‖
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
case this
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
⊢ ‖e x‖ ≤ ‖e x‖
Tactic:
simp [le_add_iff_nonneg_left]
Proof state after:
no goals
Theorem: SchwartzMap.ContinuousLinearEquiv.norm_le_norm_symm_mul_norm_apply
Proof state before:
𝕜 : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝⁹ : IsROrC 𝕜
inst✝⁸ : NormedAddCommGroup D
inst✝⁷ : NormedSpace ℝ D
inst✝⁶ : NormedSpace 𝕜 D
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : NormedSpace 𝕜 F
e : E ≃L[𝕜] D
x : E
this : ‖↑(ContinuousLinearEquiv.symm e) (e x)‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
⊢ ‖x‖ ≤ ‖↑(ContinuousLinearEquiv.symm e)‖ * ‖e x‖
Tactic:
simpa
Proof state after:
no goals
Theorem: ContinuousMultilinearMap.integral_apply
Proof state before:
α : Type u_1
inst✝¹⁰ : MeasurableSpace α
inst✝⁹ : TopologicalSpace α
inst✝⁸ : OpensMeasurableSpace α
inst✝⁷ : SecondCountableTopology α
ι : Type u_2
inst✝⁶ : Fintype ι
ι' : Type u_3
inst✝⁵ : Fintype ι'
D : ι → Type u_4
inst✝⁴ : (i : ι) → NormedAddCommGroup (D i)
inst✝³ : (i : ι) → NormedSpace ℝ (D i)
F : Type u_5
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
c : α → ContinuousMultilinearMap ℝ D F
μ : Measure α
hc : Integrable c
m : (i : ι) → D i
⊢ ∫ (x : α), (c x) m ∂μ = (∫ (x : α), c x ∂μ) m
Tactic:
simpa using ContinuousLinearMap.integral_comp_comm (apply ℝ D F m) hc
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegrand_eq_hasTemperateGrowth_smul
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
x : ℝ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    ((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f)
      x
Tactic:
simp [hasTemperateGrowth_smul_apply]
Proof state after:
no goals
Theorem: SchwartzMap.Real.integrable_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ Integrable fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x
Tactic:
simp [fourierIntegrand_eq_hasTemperateGrowth_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_add
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f g : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => f x + g x) ξ = 𝓕 (fun x => f x) ξ + 𝓕 (fun x => g x) ξ
Tactic:
simpa [Real.fourierIntegral_def] using
  integral_add (integrable_fourierIntegrand f ξ) (integrable_fourierIntegrand g ξ)
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_smul
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
c : ℝ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => c • f x) ξ = c • 𝓕 (fun x => f x) ξ
Tactic:
simpa [Real.fourierIntegral_def, smul_comm _ c] using integral_smul c _
Proof state after:
no goals