internlm/Lean-Github huggingface dataset:
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤

case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
. exact Lp.snorm_ne_top _
Proof state after:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤

E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
. exact ENNReal.mul_ne_top (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)
Proof state after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [← hξ]
Proof state after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑(L1_of_mul hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑(L1_of_mul hpq f g)) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
rw [snorm_congr_ae (coeFn_L1_of_mul hpq)]
Proof state after:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f * ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f * ↑↑g) 1 μ ≤ snorm (↑↑f) p μ * snorm (↑↑g) q μ
Tactic:
refine snorm_mul_L1_le_snorm_Lp_mul_snorm_Lq hpq ?_ ?_
Proof state after:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ

case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ

case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp f).aestronglyMeasurable
Proof state after:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
. exact (Lp.memℒp g).aestronglyMeasurable
Proof state after:
no goals
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case ha
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑ξ) 1 μ ≠ ⊤
Tactic:
exact Lp.snorm_ne_top _
Proof state after:
no goals
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case hb
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ snorm (↑↑f) p μ * snorm (↑↑g) q μ ≠ ⊤
Tactic:
exact ENNReal.mul_ne_top (Lp.snorm_ne_top _) (Lp.snorm_ne_top _)
Proof state after:
no goals
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case refine_1
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑f) μ
Tactic:
exact (Lp.memℒp f).aestronglyMeasurable
Proof state after:
no goals
Theorem: norm_L1_of_mul_le_norm_Lp_mul_norm_Lq
Proof state before:
case refine_2
E : Type u_1
inst✝¹ : MeasurableSpace E
μ : Measure E
p q : ℝ≥0∞
hpq : p⁻¹ + q⁻¹ = 1
𝕜 : Type u_2
inst✝ : NormedRing 𝕜
f : ↥(Lp 𝕜 p)
g : ↥(Lp 𝕜 q)
ξ : ↥(Lp 𝕜 1)
hξ : L1_of_mul hpq f g = ξ
⊢ AEStronglyMeasurable (↑↑g) μ
Tactic:
exact (Lp.memℒp g).aestronglyMeasurable
Proof state after:
no goals
Theorem: iteratedDeriv_neg_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (fun x => -f x) x = -iteratedDeriv n f x
Tactic:
change iteratedDeriv n (-f) x = _
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (-f) x = -iteratedDeriv n f x
Theorem: iteratedDeriv_neg_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ iteratedDeriv n (-f) x = -iteratedDeriv n f x
Tactic:
simp only [iteratedDeriv_eq_iteratedFDeriv]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ ((iteratedFDeriv 𝕜 n (-f) x) fun x => 1) = -(iteratedFDeriv 𝕜 n f x) fun x => 1
Theorem: iteratedDeriv_neg_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
⊢ ((iteratedFDeriv 𝕜 n (-f) x) fun x => 1) = -(iteratedFDeriv 𝕜 n f x) fun x => 1
Tactic:
simp [iteratedFDeriv_neg_apply]
Proof state after:
no goals
Theorem: iteratedDeriv_const_mul_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => a * f x) x = a * iteratedDeriv n f x
Tactic:
change iteratedDeriv n (a • f) x = _
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (a • f) x = a * iteratedDeriv n f x
Theorem: iteratedDeriv_const_mul_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (a • f) x = a * iteratedDeriv n f x
Tactic:
simp only [iteratedDeriv_eq_iteratedFDeriv]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ ((iteratedFDeriv 𝕜 n (a • f) x) fun x => 1) = a * (iteratedFDeriv 𝕜 n f x) fun x => 1
Theorem: iteratedDeriv_const_mul_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ ((iteratedFDeriv 𝕜 n (a • f) x) fun x => 1) = a * (iteratedFDeriv 𝕜 n f x) fun x => 1
Tactic:
simp [iteratedFDeriv_const_smul_apply hf]
Proof state after:
no goals
Theorem: iteratedDeriv_mul_const_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => f x * a) x = iteratedDeriv n f x * a
Tactic:
simp_rw [mul_comm _ a]
Proof state after:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => a * f x) x = a * iteratedDeriv n f x
Theorem: iteratedDeriv_mul_const_apply
Proof state before:
𝕜 : Type u_1
𝕜' : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
a : 𝕜'
f : 𝕜 → 𝕜'
hf : ContDiff 𝕜 (↑n) f
x : 𝕜
⊢ iteratedDeriv n (fun x => a * f x) x = a * iteratedDeriv n f x
Tactic:
exact iteratedDeriv_const_mul_apply a hf
Proof state after:
no goals
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (I * cexp (x • I)) x
Tactic:
rw [mul_comm I]
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (cexp (x • I) * I) x
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => cexp (x • I)) (cexp (x • I) * I) x
Tactic:
refine HasDerivAt.cexp ?_
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) I x
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) I x
Tactic:
suffices : HasDerivAt (fun x => x • I) ((1 : ℝ) • I) x
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x

case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x

case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Tactic:
. simpa using this
Proof state after:
case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
case this
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ HasDerivAt (fun x => x • I) (1 • I) x
Tactic:
exact HasDerivAt.smul_const (hasDerivAt_id' x) I
Proof state after:
no goals
Theorem: Complex.hasDerivAt_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
this : HasDerivAt (fun x => x • I) (1 • I) x
⊢ HasDerivAt (fun x => x • I) I x
Tactic:
simpa using this
Proof state after:
no goals
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
Tactic:
induction n with
| zero => simp
| succ n hi =>
  rw [iteratedDeriv_succ', pow_succ]
  conv => lhs; arg 2; intro x; rw [deriv_exp_real_smul_I]
  rw [iteratedDeriv_const_mul_apply I contDiff_exp_real_smul_I]
  rw [hi, mul_assoc]
Proof state after:
no goals
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
case zero
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
⊢ iteratedDeriv Nat.zero (fun x => cexp (x • I)) x = I ^ Nat.zero * cexp (x • I)
Tactic:
simp
Proof state after:
no goals
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv (Nat.succ n) (fun x => cexp (x • I)) x = I ^ Nat.succ n * cexp (x • I)
Tactic:
rw [iteratedDeriv_succ', pow_succ]
Proof state after:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (deriv fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (deriv fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
Tactic:
conv => lhs; arg 2; intro x; rw [deriv_exp_real_smul_I]
Proof state after:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (fun x => I * cexp (x • I)) x = I * I ^ n * cexp (x • I)
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ iteratedDeriv n (fun x => I * cexp (x • I)) x = I * I ^ n * cexp (x • I)
Tactic:
rw [iteratedDeriv_const_mul_apply I contDiff_exp_real_smul_I]
Proof state after:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ I * iteratedDeriv n (fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
Theorem: Complex.iteratedDeriv_exp_real_smul_I
Proof state before:
case succ
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : ℝ
n : ℕ
hi : iteratedDeriv n (fun x => cexp (x • I)) x = I ^ n * cexp (x • I)
⊢ I * iteratedDeriv n (fun x => cexp (x • I)) x = I * I ^ n * cexp (x • I)
Tactic:
rw [hi, mul_assoc]
Proof state after:
no goals
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ Function.HasTemperateGrowth fun x => cexp (x • I)
Tactic:
refine ⟨contDiff_exp_real_smul_I, ?_⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
⊢ ∀ (n : ℕ), ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
intro n
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∃ k C, ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ C * (1 + ‖x‖) ^ k
Tactic:
refine ⟨n, 1, ?_⟩
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
⊢ ∀ (x : ℝ), ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
intro x
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedFDeriv ℝ n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
rw [norm_iteratedFDeriv_eq_norm_iteratedDeriv]
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedDeriv n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖iteratedDeriv n (fun x => cexp (x • I)) x‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
rw [iteratedDeriv_exp_real_smul_I]
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖I ^ n * cexp (x • I)‖ ≤ 1 * (1 + ‖x‖) ^ n
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ ‖I ^ n * cexp (x • I)‖ ≤ 1 * (1 + ‖x‖) ^ n
Tactic:
simp
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ (1 + |x|) ^ n
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ (1 + |x|) ^ n
Tactic:
exact one_le_pow_of_one_le (by simp) n
Proof state after:
no goals
Theorem: Complex.hasTemperateGrowth_exp_real_smul_I
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
n : ℕ
x : ℝ
⊢ 1 ≤ 1 + |x|
Tactic:
simp
Proof state after:
no goals
Theorem: Real.fderiv_fourierChar_apply
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => ↑(fourierChar (Multiplicative.ofAdd x))) x) dx =
    (2 * π * dx) • (I * ↑(fourierChar (Multiplicative.ofAdd x)))
Tactic:
simp [Real.fourierChar]
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (2 * ↑π * ↑x * I)) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Theorem: Real.fderiv_fourierChar_apply
Proof state before:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (2 * ↑π * ↑x * I)) x) dx = 2 * ↑π * ↑dx * (I * cexp (2 * ↑π * ↑x * I))
Tactic:
norm_cast
Proof state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAlgebra 𝕜 ℝ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x dx : ℝ
⊢ (fderiv ℝ (fun x => cexp (↑(2 * π * x) * I)) x) dx = ↑(2 * π * dx) * (I * cexp (↑(2 * π * x) * I))