internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hC_pow : 0 ≤ C ^ p
x : E
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
specialize hC x
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
have hq : q = p * r := by rw [← hr, mul_div, mul_div_cancel_left _ hp.ne']
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-q)
Tactic:
rw [hq]
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Tactic:
have hb_pos : 0 < 1 + ‖x‖
Proof state after:
case hb_pos
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ 0 < 1 + ‖x‖

case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case hb_pos
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ 0 < 1 + ‖x‖

case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Tactic:
. exact add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * (1 + ‖x‖) ^ (-(p * r))
Tactic:
rw [mul_comm p r, ← neg_mul, Real.rpow_mul hb_pos.le]
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * ((1 + ‖x‖) ^ (-r)) ^ p
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C ^ p * ((1 + ‖x‖) ^ (-r)) ^ p
Tactic:
rw [← Real.mul_rpow hC_nonneg (Real.rpow_nonneg hb_pos.le _)]
Proof state after:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ (C * (1 + ‖x‖) ^ (-r)) ^ p
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case h
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
hb_pos : 0 < 1 + ‖x‖
⊢ ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ (C * (1 + ‖x‖) ^ (-r)) ^ p
Tactic:
exact Real.rpow_le_rpow (norm_nonneg _) hC hp.le
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
⊢ q = p * r
Tactic:
rw [← hr, mul_div, mul_div_cancel_left _ hp.ne']
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_pow_one_add_norm
Proof state before:
case hb_pos
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
n : ℕ
r : ℝ
hr : q / p = r
C : ℝ
hC_nonneg : 0 ≤ C
hC_pow : 0 ≤ C ^ p
x : E
hC : ‖iteratedFDeriv ℝ n (⇑f) x‖ ≤ C * (1 + ‖x‖) ^ (-r)
hq : q = p * r
⊢ 0 < 1 + ‖x‖
Tactic:
exact add_pos_of_pos_of_nonneg zero_lt_one (norm_nonneg _)
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
have := pow_norm_iteratedFDeriv_le_pow_one_add_norm f hp 1
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
this : ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-1)
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Theorem: SchwartzMap.pow_norm_iteratedFDeriv_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
this : ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-1)
⊢ ∀ (n : ℕ), ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ n (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
simpa [Real.rpow_neg_one]
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_le_pow_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
have := pow_norm_iteratedFDeriv_le_pow_one_add_norm f hp q 0
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.pow_norm_le_pow_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
q : ℝ
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
simpa
Proof state after:
no goals
Theorem: SchwartzMap.norm_le_pow_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
q : ℝ
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
have := pow_norm_iteratedFDeriv_le_pow_one_add_norm f zero_lt_one q 0
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
q : ℝ
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ 1 ≤ C * (1 + ‖x‖) ^ (-q)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ (-q)
Theorem: SchwartzMap.norm_le_pow_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
q : ℝ
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ 1 ≤ C * (1 + ‖x‖) ^ (-q)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖) ^ (-q)
Tactic:
simpa
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
have := pow_norm_iteratedFDeriv_le_inv_one_add_norm f hp 0
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Theorem: SchwartzMap.pow_norm_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
p : ℝ
hp : 0 < p
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ^ p ≤ C * (1 + ‖x‖)⁻¹
Tactic:
simpa
Proof state after:
no goals
Theorem: SchwartzMap.norm_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖)⁻¹
Tactic:
have := pow_norm_iteratedFDeriv_le_inv_one_add_norm f zero_lt_one 0
Proof state after:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ 1 ≤ C * (1 + ‖x‖)⁻¹
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖)⁻¹
Theorem: SchwartzMap.norm_le_inv_one_add_norm
Proof state before:
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : 𝓢(E, F)
this : ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ^ 1 ≤ C * (1 + ‖x‖)⁻¹
⊢ ∃ C, 0 ≤ C ∧ ∀ (x : E), ‖f x‖ ≤ C * (1 + ‖x‖)⁻¹
Tactic:
simpa
Proof state after:
no goals
Theorem: SchwartzMap.snorm_top_lt_top
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
⊢ snorm ⇑f ⊤ volume < ⊤
Tactic:
rcases f.decay 0 0 with ⟨C, hC⟩
Proof state after:
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
C : ℝ
hC : 0 < C ∧ ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ snorm ⇑f ⊤ volume < ⊤
Theorem: SchwartzMap.snorm_top_lt_top
Proof state before:
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
C : ℝ
hC : 0 < C ∧ ∀ (x : E), ‖x‖ ^ 0 * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤ C
⊢ snorm ⇑f ⊤ volume < ⊤
Tactic:
simp at hC
Proof state after:
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
C : ℝ
hC : 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C
⊢ snorm ⇑f ⊤ volume < ⊤
Theorem: SchwartzMap.snorm_top_lt_top
Proof state before:
case intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
f : 𝓢(E, F)
C : ℝ
hC : 0 < C ∧ ∀ (x : E), ‖f x‖ ≤ C
⊢ snorm ⇑f ⊤ volume < ⊤
Tactic:
exact snormEssSup_lt_top_of_ae_bound (Filter.eventually_of_forall hC.right)
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ snorm (fun x => (1 + ‖x‖) ^ n • f x) (↑p) volume < ⊤
Tactic:
simp [snorm, hp.ne', snorm']
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ (∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p) ^ (↑p)⁻¹ < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ (∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p) ^ (↑p)⁻¹ < ⊤
Tactic:
refine ENNReal_rpow_lt_top (inv_pos_of_pos hp) ?_
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
generalize hr : (FiniteDimensional.finrank ℝ E + 1 : ℝ) = r
Proof state after:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
rcases pow_norm_le_pow_one_add_norm f hp (r + n * p) with ⟨C, ⟨hC_nonneg, hC⟩⟩
Proof state after:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ (fun a => ↑a) p ≤ C * (1 + ‖x‖) ^ (-(r + n * ↑p))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ (fun a => ↑a) p ≤ C * (1 + ‖x‖) ^ (-(r + n * ↑p))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
simp at hC
Proof state after:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
suffices : ∫⁻ (x : E), (‖(1 + ‖x‖) ^ n • f x‖₊ : ENNReal) ^ (p : ℝ) ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Proof state after:
case intro.intro
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤

case this
E : Type u_1
F : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : Measure.IsAddHaarMeasure volume
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))