internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => f x) Filter.atTop (nhds 0)
Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
rcases f.decay₁ 1 0 with ⟨C, hC⟩
Proof state after:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + ‖x‖) ^ 1 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + ‖x‖) ^ 1 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
simp at hC
Proof state after:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => ‖f x‖) Filter.atTop (nhds 0)
Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (h := fun x => C * (1 + |x|)⁻¹) tendsto_const_nhds ?_ ?_ ?_
Proof state after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)

case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)

case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. rw [← mul_zero C]
  refine Filter.Tendsto.const_mul C ?_
  refine Filter.Tendsto.inv_tendsto_atTop ?_
  refine Filter.tendsto_atTop_add_const_left _ 1 ?_
  exact Filter.tendsto_abs_atTop_atTop
Proof state after:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖

case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. intro x
  simp
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
. intro x
  simp
  rw [← div_eq_mul_inv]
  rw [le_div_iff (lt_of_lt_of_le zero_lt_one (by simp))]
  rw [mul_comm]
  exact hC x
Proof state after:
no goals
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds 0)
Tactic:
rw [← mul_zero C]
Proof state after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds (C * 0))
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun x => C * (1 + |x|)⁻¹) Filter.atTop (nhds (C * 0))
Tactic:
refine Filter.Tendsto.const_mul C ?_
Proof state after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => (1 + |k|)⁻¹) Filter.atTop (nhds 0)
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => (1 + |k|)⁻¹) Filter.atTop (nhds 0)
Tactic:
refine Filter.Tendsto.inv_tendsto_atTop ?_
Proof state after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => 1 + |k|) Filter.atTop Filter.atTop
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => 1 + |k|) Filter.atTop Filter.atTop
Tactic:
refine Filter.tendsto_atTop_add_const_left _ 1 ?_
Proof state after:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => |k|) Filter.atTop Filter.atTop
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_1
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ Filter.Tendsto (fun k => |k|) Filter.atTop Filter.atTop
Tactic:
exact Filter.tendsto_abs_atTop_atTop
Proof state after:
no goals
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => 0) ≤ fun x => ‖f x‖
Tactic:
intro x
Proof state after:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => 0) x ≤ (fun x => ‖f x‖) x
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_2
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => 0) x ≤ (fun x => ‖f x‖) x
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
⊢ (fun x => ‖f x‖) ≤ fun x => C * (1 + |x|)⁻¹
Tactic:
intro x
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => ‖f x‖) x ≤ (fun x => C * (1 + |x|)⁻¹) x
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (fun x => ‖f x‖) x ≤ (fun x => C * (1 + |x|)⁻¹) x
Tactic:
simp
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C * (1 + |x|)⁻¹
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C * (1 + |x|)⁻¹
Tactic:
rw [← div_eq_mul_inv]
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C / (1 + |x|)
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ ≤ C / (1 + |x|)
Tactic:
rw [le_div_iff (lt_of_lt_of_le zero_lt_one (by simp))]
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ * (1 + |x|) ≤ C
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ ‖f x‖ * (1 + |x|) ≤ C
Tactic:
rw [mul_comm]
Proof state after:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (1 + |x|) * ‖f x‖ ≤ C
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
case intro.refine_3
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ (1 + |x|) * ‖f x‖ ≤ C
Tactic:
exact hC x
Proof state after:
no goals
Theorem: SchwartzMap.tendsto_atTop_zero_real
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
C : ℝ
hC : ∀ (x : ℝ), (1 + |x|) * ‖f x‖ ≤ C
x : ℝ
⊢ 1 ≤ 1 + |x|
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.tendsto_atBot_zero_real
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => f x) Filter.atBot (nhds 0)
Tactic:
conv => arg 1; intro x; rw [← neg_neg x]; rw [← compNegEquiv_apply]
Proof state after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => (compNegEquiv f) (-x)) Filter.atBot (nhds 0)
Theorem: SchwartzMap.tendsto_atBot_zero_real
Proof state before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(ℝ, F)
⊢ Filter.Tendsto (fun x => (compNegEquiv f) (-x)) Filter.atBot (nhds 0)
Tactic:
exact (tendsto_atTop_zero_real (compNegEquiv f)).comp Filter.tendsto_neg_atBot_atTop
Proof state after:
no goals
Theorem: Function.hasTemperateGrowth_single
Proof state before:
E' : Type ?u.133422
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
i : ι
⊢ HasTemperateGrowth fun u => Pi.single i u
Tactic:
change HasTemperateGrowth (fun u : M i => ContinuousLinearMap.single (R := ℝ) i u)
Proof state after:
E' : Type ?u.133422
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
i : ι
⊢ HasTemperateGrowth fun u => (ContinuousLinearMap.single i) u
Theorem: Function.hasTemperateGrowth_single
Proof state before:
E' : Type ?u.133422
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
i : ι
⊢ HasTemperateGrowth fun u => (ContinuousLinearMap.single i) u
Tactic:
exact hasTemperateGrowth_clm _
Proof state after:
no goals
Theorem: SchwartzMap.norm_vectorFourierIntegrand_apply
Proof state before:
E' : Type ?u.169572
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ξ x : E
⊢ ‖((vectorFourierIntegrand ξ) f) x‖ = ‖f x‖
Tactic:
simp [vectorFourierIntegrand_apply, norm_smul]
Proof state after:
no goals
Theorem: SchwartzMap.nnnorm_vectorFourierIntegrand_apply
Proof state before:
E' : Type ?u.178382
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ξ x : E
⊢ ↑‖((vectorFourierIntegrand ξ) f) x‖₊ = ↑‖f x‖₊
Tactic:
simp
Proof state after:
no goals