internlm/Lean-Github huggingface dataset:
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
⊢ ∀ (x : E), ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
intro x
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 * (1 + ‖x‖) ^ 1
Tactic:
simp
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
n : ℕ
x : E
⊢ ‖iteratedFDeriv ℝ n (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero => simp
| succ n =>
  simp [iteratedFDeriv_succ_eq_comp_right]
  simp_rw [fderiv_innerSL_apply]
  cases n with
  | zero =>
    simp
    refine le_trans (norm_innerSL_le_one ℝ) (by simp)
  | succ n =>
    rw [iteratedFDeriv_const_of_ne]
    . change ‖0‖ ≤ _
      simp
    . simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) (fun x => (innerSL ℝ) x) x‖ ≤ 1 + ‖x‖
Tactic:
simp [iteratedFDeriv_succ_eq_comp_right]
Proof state after:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => fderiv ℝ (fun x => (innerSL ℝ) x) y) x‖ ≤ 1 + ‖x‖
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => fderiv ℝ (fun x => (innerSL ℝ) x) y) x‖ ≤ 1 + ‖x‖
Tactic:
simp_rw [fderiv_innerSL_apply]
Proof state after:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ n (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
cases n with
| zero =>
  simp
  refine le_trans (norm_innerSL_le_one ℝ) (by simp)
| succ n =>
  rw [iteratedFDeriv_const_of_ne]
  . change ‖0‖ ≤ _
    simp
  . simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖iteratedFDeriv ℝ Nat.zero (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖innerSL ℝ‖ ≤ 1 + ‖x‖
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.zero
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ ‖innerSL ℝ‖ ≤ 1 + ‖x‖
Tactic:
refine le_trans (norm_innerSL_le_one ℝ) (by simp)
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
⊢ 1 ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖iteratedFDeriv ℝ (Nat.succ n) (fun y => innerSL ℝ) x‖ ≤ 1 + ‖x‖
Tactic:
rw [iteratedFDeriv_const_of_ne]
Proof state after:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖

case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖

case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
. change ‖0‖ ≤ _
  simp
Proof state after:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
. simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0 x‖ ≤ 1 + ‖x‖
Tactic:
change ‖0‖ ≤ _
Proof state after:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0‖ ≤ 1 + ‖x‖
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ ‖0‖ ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_innerSL
Proof state before:
case succ.succ.hn
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x : E
n : ℕ
⊢ Nat.succ n ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: innerSL_smul_comm
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ((innerSL_smul F x) c) u = ((innerSL_smul F u) c) x
Tactic:
simp [innerSL_smul_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ⟪x, u⟫_ℝ • c = ⟪u, x⟫_ℝ • c
Theorem: innerSL_smul_comm
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
x u : E
c : F
⊢ ⟪x, u⟫_ℝ • c = ⟪u, x⟫_ℝ • c
Tactic:
rw [real_inner_comm]
Proof state after:
no goals
Theorem: SchwartzMap.innerSL_smul_one_eq_id_smul
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(ℝ, F)
x : ℝ
⊢ ((innerSL_smul φ) x) 1 = (id_smul φ) x
Tactic:
simp [innerSL_smul_apply, id_smul_apply]
Proof state after:
no goals
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ‖(innerSL_smul φ) x‖ ≤ ‖x‖ * ‖φ x‖
Tactic:
rw [ContinuousLinearMap.opNorm_le_iff (mul_nonneg (norm_nonneg x) (norm_nonneg (φ x)))]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ∀ (x_1 : E), ‖((innerSL_smul φ) x) x_1‖ ≤ ‖x‖ * ‖φ x‖ * ‖x_1‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ∀ (x_1 : E), ‖((innerSL_smul φ) x) x_1‖ ≤ ‖x‖ * ‖φ x‖ * ‖x_1‖
Tactic:
intro m
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖((innerSL_smul φ) x) m‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖((innerSL_smul φ) x) m‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Tactic:
rw [SchwartzMap.innerSL_smul_apply, norm_smul]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Tactic:
rw [← mul_rotate]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖m‖ * ‖x‖ * ‖φ x‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖m‖ * ‖x‖ * ‖φ x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (φ x))
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖m‖ * ‖x‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖m‖ * ‖x‖
Tactic:
rw [mul_comm]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖x‖ * ‖m‖
Theorem: SchwartzMap.norm_innerSL_smul_le
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖x‖ * ‖m‖
Tactic:
exact norm_inner_le_norm x m
Proof state after:
no goals
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ (ofHasTemperateGrowth hg) φ = ∫ (x : E), g x • φ x
Tactic:
rw [ofHasTemperateGrowth, ContinuousLinearMap.comp_apply, integralCLM_apply]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ ∫ (x : E), ((hasTemperateGrowth_smul hg) φ) x = ∫ (x : E), g x • φ x
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
g : E → 𝕜
hg : Function.HasTemperateGrowth g
φ : 𝓢(E, F)
⊢ ∫ (x : E), ((hasTemperateGrowth_smul hg) φ) x = ∫ (x : E), g x • φ x
Tactic:
rfl
Proof state after:
no goals
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_const
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
⊢ ofHasTemperateGrowth (_ : Function.HasTemperateGrowth fun x => c) = const E F c
Tactic:
ext φ
Proof state after:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ (ofHasTemperateGrowth (_ : Function.HasTemperateGrowth fun x => c)) φ = (const E F c) φ
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_const
Proof state before:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ (ofHasTemperateGrowth (_ : Function.HasTemperateGrowth fun x => c)) φ = (const E F c) φ
Tactic:
rw [ofHasTemperateGrowth_apply]
Proof state after:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ ∫ (x : E), c • φ x = (const E F c) φ
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_const
Proof state before:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ ∫ (x : E), c • φ x = (const E F c) φ
Tactic:
rw [const_apply]
Proof state after:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ ∫ (x : E), c • φ x = c • ∫ (x : E), φ x
Theorem: SchwartzMap.Distribution.ofHasTemperateGrowth_const
Proof state before:
case h
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace ℝ E
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace ℝ F
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAlgebra ℝ 𝕜
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : IsScalarTower ℝ 𝕜 F
inst✝³ : CompleteSpace F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
c : 𝕜
φ : 𝓢(E, F)
⊢ ∫ (x : E), c • φ x = c • ∫ (x : E), φ x
Tactic:
rw [integral_smul]
Proof state after:
no goals
Theorem: Finset.prod_update_one_of_mem
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
i : α
hi : i ∈ s
f : α → β
⊢ ∏ j in s, Function.update f i 1 j = ∏ j in s \ {i}, f j
Tactic:
simp [prod_update_of_mem hi]
Proof state after:
no goals
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in erase (attach s) i, f ↑j = ∏ j in erase s ↑i, f j
Tactic:
simp only [erase_eq]
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x in attach s \ {i}, f ↑x = ∏ x in s \ {↑i}, f x
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ x in attach s \ {i}, f ↑x = ∏ x in s \ {↑i}, f x
Tactic:
rw [← prod_update_one_of_mem i.prop, ← prod_update_one_of_mem (mem_attach s i)]
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j = ∏ j in s, Function.update (fun x => f x) (↑i) 1 j
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j = ∏ j in s, Function.update (fun x => f x) (↑i) 1 j
Tactic:
rw [← prod_coe_sort s]
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j =
    ∏ i_1 : { x // x ∈ s }, Function.update (fun x => f x) (↑i) 1 ↑i_1
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∏ j in attach s, Function.update (fun x => f ↑x) i 1 j =
    ∏ i_1 : { x // x ∈ s }, Function.update (fun x => f x) (↑i) 1 ↑i_1
Tactic:
refine prod_congr rfl ?_
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∀ x ∈ univ, Function.update (fun x => f ↑x) i 1 x = Function.update (fun x => f x) (↑i) 1 ↑x
Theorem: Finset.prod_erase_attach
Proof state before:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i : { x // x ∈ s }
⊢ ∀ x ∈ univ, Function.update (fun x => f ↑x) i 1 x = Function.update (fun x => f x) (↑i) 1 ↑x
Tactic:
intro j _
Proof state after:
ι : Type u_1
β : Type u
α : Type v
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
s : Finset ι
f : ι → α
i j : { x // x ∈ s }
a✝ : j ∈ univ
⊢ Function.update (fun x => f ↑x) i 1 j = Function.update (fun x => f x) (↑i) 1 ↑j