Imports
module
public import Mathlib.Analysis.Distribution.SchwartzSpace.Basic
public import Mathlib.Analysis.Calculus.ContDiff.Bounds
The multiple of a Schwartz map by x
In this module we define the continuous linear map from the Schwartz space
𝓢(ℝ, 𝕜) to itself which takes a Schwartz map η to the Schwartz map x * η.
@[ expose ] public section
lemma norm_iteratedFDeriv_ofRealCLM { x } ( i : ℕ ) :
‖ iteratedFDeriv ℝ i ( RCLike.ofRealCLM ( K := 𝕜 ) ) x ‖ =
if i = 0 then | x | else if i = 1 then 1 else 0 := by 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ iteratedFDeriv ℝ i (⇑ RCLike.ofRealCLM ) x ‖ = if i = 0 then | x | else if i = 1 then 1 else 0
match i with
| 0 => 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ iteratedFDeriv ℝ 0 (⇑ RCLike.ofRealCLM ) x ‖ = if 0 = 0 then | x | else if 0 = 1 then 1 else 0 simp All goals completed! 🐙
| 1 => 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ iteratedFDeriv ℝ 1 (⇑ RCLike.ofRealCLM ) x ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0
rw [ norm_iteratedFDeriv_one , 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ fderiv ℝ (⇑ RCLike.ofRealCLM ) x ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ RCLike.ofRealCLM ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0 RCLike.ofRealCLM . fderiv 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ RCLike.ofRealCLM ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ RCLike.ofRealCLM ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0 ] 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ RCLike.ofRealCLM ‖ = if 1 = 0 then | x | else if 1 = 1 then 1 else 0
simp All goals completed! 🐙
| ( n + 2 ) => 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ ⊢ ‖ iteratedFDeriv ℝ ( n + 2 ) (⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0
have h : fderiv ℝ ⇑ ( RCLike.ofRealCLM ( K := 𝕜 ) ) = fun _ => RCLike.ofRealCLM := by 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ ⊢ ‖ iteratedFDeriv ℝ i (⇑ RCLike.ofRealCLM ) x ‖ = if i = 0 then | x | else if i = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 2 ) (⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0
ext1 y 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ y : ℝ ⊢ fderiv ℝ (⇑ RCLike.ofRealCLM ) y = RCLike.ofRealCLM 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 2 ) (⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0
exact RCLike.ofRealCLM . fderiv 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 2 ) (⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 2 ) (⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0
rw [ ← norm_iteratedFDeriv_fderiv , 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 1 ) ( fderiv ℝ ⇑ RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ 0 x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 h , 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => RCLike.ofRealCLM ) x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ 0 x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 iteratedFDeriv_const_of_ne n . succ_ne_zero 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ 0 x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ 0 x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0 ] 𝕜 : Type inst✝ : RCLike 𝕜 x : ℝ i : ℕ n : ℕ h : fderiv ℝ ⇑ RCLike.ofRealCLM = fun x => RCLike.ofRealCLM ⊢ ‖ 0 x ‖ = if n + 2 = 0 then | x | else if n + 2 = 1 then 1 else 0
simp All goals completed! 🐙
The continuous linear map 𝓢(ℝ, 𝕜) →L[𝕜] 𝓢(ℝ, 𝕜) taking a Schwartz map
η to x * η.
set_option backward.isDefEq.respectTransparency false in
def powOneMul : 𝓢( ℝ , 𝕜 ) →L[ 𝕜 ] 𝓢( ℝ , 𝕜 ) := by 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ 𝓢( ℝ , 𝕜 ) →L[ 𝕜 ] 𝓢( ℝ , 𝕜 )
refine mkCLM ( fun ψ ↦ fun x => x * ψ x ) ? _ ? _ ? _ ? _ refine_1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( f g : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ), ↑ x * ( f + g ) x = ↑ x * f x + ↑ x * g x refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( a : 𝕜 ) ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ), ↑ x * ( a • f ) x = ( RingHom.id 𝕜 ) a • ( ↑ x * f x ) refine_3 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( f : 𝓢( ℝ , 𝕜 ) ), ContDiff ℝ ∞ fun x => ↑ x * f x refine_4 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( n : ℕ × ℕ ),
∃ s C ,
0 ≤ C ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
‖ x ‖ ^ n .1 * ‖ iteratedFDeriv ℝ n .2 (fun x => ↑ x * f x ) x ‖ ≤ C * ( s . sup ( schwartzSeminormFamily 𝕜 ℝ 𝕜 ) ) f
· refine_1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( f g : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ), ↑ x * ( f + g ) x = ↑ x * f x + ↑ x * g x intro ψ1 ψ2 x refine_1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ1 : 𝓢( ℝ , 𝕜 ) ψ2 : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ↑ x * ( ψ1 + ψ2 ) x = ↑ x * ψ1 x + ↑ x * ψ2 x
simp [ mul_add ] All goals completed! 🐙
· refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( a : 𝕜 ) ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ), ↑ x * ( a • f ) x = ( RingHom.id 𝕜 ) a • ( ↑ x * f x ) intro c ψ x refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E c : 𝕜 ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ↑ x * ( c • ψ ) x = ( RingHom.id 𝕜 ) c • ( ↑ x * ψ x )
simp only [ smul_apply , smul_eq_mul , RingHom.id_apply ] refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E c : 𝕜 ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ↑ x * ( c * ψ x ) = c * ( ↑ x * ψ x )
ring All goals completed! 🐙
· refine_3 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( f : 𝓢( ℝ , 𝕜 ) ), ContDiff ℝ ∞ fun x => ↑ x * f x intro ψ refine_3 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ fun x => ↑ x * ψ x
apply ContDiff.mul refine_3.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ RCLike.ofReal hg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ ⇑ ψ
· refine_3.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ RCLike.ofReal change ContDiff ℝ _ RCLike.ofRealCLM refine_3.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ ⇑ RCLike.ofRealCLM
fun_prop All goals completed! 🐙
· hg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ψ : 𝓢( ℝ , 𝕜 ) ⊢ ContDiff ℝ ∞ ⇑ ψ exact SchwartzMap.smooth ψ ⊤ All goals completed! 🐙
· refine_4 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E ⊢ ∀ ( n : ℕ × ℕ ),
∃ s C ,
0 ≤ C ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
‖ x ‖ ^ n .1 * ‖ iteratedFDeriv ℝ n .2 (fun x => ↑ x * f x ) x ‖ ≤ C * ( s . sup ( schwartzSeminormFamily 𝕜 ℝ 𝕜 ) ) f intro ( k , n ) refine_4 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ⊢ ∃ s C ,
0 ≤ C ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
‖ x ‖ ^ ( k , n ) .1 * ‖ iteratedFDeriv ℝ ( k , n ) .2 (fun x => ↑ x * f x ) x ‖ ≤ C * ( s . sup ( schwartzSeminormFamily 𝕜 ℝ 𝕜 ) ) f
use { ( k , n - 1 ) , ( k + 1 , n ) } h 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ⊢ ∃ C ,
0 ≤ C ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
‖ x ‖ ^ ( k , n ) .1 * ‖ iteratedFDeriv ℝ ( k , n ) .2 (fun x => ↑ x * f x ) x ‖ ≤
C * ( { ( k , n - 1 ) , ( k + 1 , n ) } . sup ( schwartzSeminormFamily 𝕜 ℝ 𝕜 ) ) f
simp only [ Real.norm_eq_abs , Finset.sup_insert , schwartzSeminormFamily_apply ,
Finset.sup_singleton , Seminorm.coe_sup , Pi.sup_apply ] h 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ⊢ ∃ C ,
0 ≤ C ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
| x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ↑ x * f x ) x ‖ ≤
C * max ( ( SchwartzMap.seminorm 𝕜 k ( n - 1 ) ) f ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n ) f )
use n + 1 h 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ⊢ 0 ≤ ↑ n + 1 ∧
∀ ( f : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ),
| x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ↑ x * f x ) x ‖ ≤
( ↑ n + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n - 1 ) ) f ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n ) f )
refine ⟨ by 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ⊢ 0 ≤ ↑ n + 1 linarith All goals completed! 🐙 , ? _ ⟩
intro ψ x h 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ ≤
( ↑ n + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n ) ψ )
trans ‖ x ‖ ^ k * ∑ i ∈ Finset.range ( n + 1 ) , ↑ ( n . choose i ) *
‖ iteratedFDeriv ℝ i ( fun ( x : ℝ ) => ( x : 𝕜 ) ) x ‖ *
‖ iteratedFDeriv ℝ ( n - i ) ( fun x => ψ x ) x ‖ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ ≤
‖ x ‖ ^ k *
∑ i ∈ Finset.range ( n + 1 ) ,
↑ ( n . choose i ) * ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖ * ‖ iteratedFDeriv ℝ ( n - i ) (fun x => ψ x ) x ‖ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ‖ x ‖ ^ k *
∑ i ∈ Finset.range ( n + 1 ) ,
↑ ( n . choose i ) * ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖ * ‖ iteratedFDeriv ℝ ( n - i ) (fun x => ψ x ) x ‖ ≤
( ↑ n + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n ) ψ )
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ ≤
‖ x ‖ ^ k *
∑ i ∈ Finset.range ( n + 1 ) ,
↑ ( n . choose i ) * ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖ * ‖ iteratedFDeriv ℝ ( n - i ) (fun x => ψ x ) x ‖ apply mul_le_mul_of_nonneg' h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k ≤ ‖ x ‖ ^ k h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ ≤
∑ i ∈ Finset.range ( n + 1 ) ,
↑ ( n . choose i ) * ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖ * ‖ iteratedFDeriv ℝ ( n - i ) (fun x => ψ x ) x ‖ c0 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ 0 ≤ ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ b0 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ 0 ≤ ‖ x ‖ ^ k
· h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k ≤ ‖ x ‖ ^ k exact Preorder.le_refl ( ‖ x ‖ ^ k ) All goals completed! 🐙
· h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ ≤
∑ i ∈ Finset.range ( n + 1 ) ,
↑ ( n . choose i ) * ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖ * ‖ iteratedFDeriv ℝ ( n - i ) (fun x => ψ x ) x ‖ apply norm_iteratedFDeriv_mul_le ( N := ∞ ) h₂.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ContDiff ℝ ∞ RCLike.ofReal h₂.hg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ContDiff ℝ ∞ ⇑ ψ h₂.hn 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ↑ n ≤ ∞
· h₂.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ContDiff ℝ ∞ RCLike.ofReal change ContDiff ℝ ∞ RCLike.ofRealCLM h₂.hf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ContDiff ℝ ∞ ⇑ RCLike.ofRealCLM
fun_prop All goals completed! 🐙
· h₂.hg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ContDiff ℝ ∞ ⇑ ψ exact SchwartzMap.smooth ( ψ ) ⊤ All goals completed! 🐙
· h₂.hn 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ↑ n ≤ ∞ exact right_eq_inf . mp rfl All goals completed! 🐙
· c0 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ 0 ≤ ‖ iteratedFDeriv ℝ n (fun x => ↑ x * ψ x ) x ‖ exact ContinuousMultilinearMap.opNorm_nonneg _ All goals completed! 🐙
· b0 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ 0 ≤ ‖ x ‖ ^ k refine pow_nonneg ? _ k b0 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ 0 ≤ ‖ x ‖
exact norm_nonneg x All goals completed! 🐙
conv_lhs =>
enter [ 2 , 2 , i , 1 , 2 ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ i : ℕ | ‖ iteratedFDeriv ℝ i (fun x => ↑ x ) x ‖
change ‖ iteratedFDeriv ℝ i RCLike.ofRealCLM x ‖ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ i : ℕ | ‖ iteratedFDeriv ℝ i (⇑ RCLike.ofRealCLM ) x ‖
rw [ norm_iteratedFDeriv_ofRealCLM 𝕜 i ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ i : ℕ | if i = 0 then | x | else if i = 1 then 1 else 0
match n with
| 0 => 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ‖ x ‖ ^ k *
∑ i ∈ Finset.range ( 0 + 1 ) ,
( ↑ ( Nat.choose 0 i ) * if i = 0 then | x | else if i = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( 0 - i ) (fun x => ψ x ) x ‖ ≤
( ↑ 0 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( 0 - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ )
simp only [ Real.norm_eq_abs , zero_add , Finset.range_one , mul_ite , mul_one , mul_zero , ite_mul ,
zero_mul , Finset.sum_singleton , ↓ reduceIte , Nat.choose_self , Nat.cast_one , one_mul ,
Nat.sub_zero , norm_iteratedFDeriv_zero , CharP.cast_eq_zero , ge_iff_le ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ( | x | * ‖ ψ x ‖ ) ≤ max ( ( SchwartzMap.seminorm 𝕜 k ( 0 - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ )
trans ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ( | x | * ‖ ψ x ‖ ) ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ ≤ max ( ( SchwartzMap.seminorm 𝕜 k ( 0 - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ )
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ( | x | * ‖ ψ x ‖ ) ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ apply le_trans ? _ ( ψ . le_seminorm 𝕜 _ _ x ) 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ( | x | * ‖ ψ x ‖ ) ≤ ‖ x ‖ ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ 0 (⇑ ψ ) x ‖
simp only [ Real.norm_eq_abs , norm_iteratedFDeriv_zero ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | ^ k * ( | x | * ‖ ψ x ‖ ) ≤ | x | ^ ( k + 1 ) * ‖ ψ x ‖
ring_nf 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ ⊢ | x | * | x | ^ k * ‖ ψ x ‖ ≤ | x | * | x | ^ k * ‖ ψ x ‖
rfl All goals completed! 🐙
exact le_max_right ( ( SchwartzMap.seminorm 𝕜 k ( 0 - 1 ) ) ψ )
( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) 0 ) ψ ) All goals completed! 🐙
| .succ n => 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
∑ i ∈ Finset.range ( n . succ + 1 ) ,
( ↑ ( n . succ . choose i ) * if i = 0 then | x | else if i = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - i ) (fun x => ψ x ) x ‖ ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ )
rw [ Finset.sum_range_succ' , 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
( ∑ k ∈ Finset.range ( n + 1 ) ,
( ↑ ( n . succ . choose ( k + 1 ) ) * if k + 1 = 0 then | x | else if k + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( k + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose 0 ) * if 0 = 0 then | x | else if 0 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - 0 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ ) 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
( ∑ k ∈ Finset.range n ,
( ↑ ( n . succ . choose ( k + 1 + 1 ) ) * if k + 1 + 1 = 0 then | x | else if k + 1 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( k + 1 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose ( 0 + 1 ) ) * if 0 + 1 = 0 then | x | else if 0 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( 0 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose 0 ) * if 0 = 0 then | x | else if 0 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - 0 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ ) Finset.sum_range_succ' 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
( ∑ k ∈ Finset.range n ,
( ↑ ( n . succ . choose ( k + 1 + 1 ) ) * if k + 1 + 1 = 0 then | x | else if k + 1 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( k + 1 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose ( 0 + 1 ) ) * if 0 + 1 = 0 then | x | else if 0 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( 0 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose 0 ) * if 0 = 0 then | x | else if 0 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - 0 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ ) 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
( ∑ k ∈ Finset.range n ,
( ↑ ( n . succ . choose ( k + 1 + 1 ) ) * if k + 1 + 1 = 0 then | x | else if k + 1 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( k + 1 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose ( 0 + 1 ) ) * if 0 + 1 = 0 then | x | else if 0 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( 0 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose 0 ) * if 0 = 0 then | x | else if 0 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - 0 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ ) ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ‖ x ‖ ^ k *
( ∑ k ∈ Finset.range n ,
( ↑ ( n . succ . choose ( k + 1 + 1 ) ) * if k + 1 + 1 = 0 then | x | else if k + 1 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( k + 1 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose ( 0 + 1 ) ) * if 0 + 1 = 0 then | x | else if 0 + 1 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - ( 0 + 1 ) ) (fun x => ψ x ) x ‖ +
( ↑ ( n . succ . choose 0 ) * if 0 = 0 then | x | else if 0 = 1 then 1 else 0 ) *
‖ iteratedFDeriv ℝ ( n . succ - 0 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n . succ + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k ( n . succ - 1 ) ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) n . succ ) ψ )
simp only [ Real.norm_eq_abs , Nat.succ_eq_add_one , Nat.add_eq_zero_iff , one_ne_zero , and_false ,
and_self , ↓ reduceIte , Nat.add_eq_right , mul_zero , zero_mul , Finset.sum_const_zero ,
zero_add , Nat.choose_one_right , Nat.cast_add , Nat.cast_one , mul_one , Nat.reduceAdd ,
Nat.add_one_sub_one , Nat.choose_zero_right , one_mul , Nat.sub_zero , ge_iff_le ] 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ( ( ↑ n + 1 ) * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ + | x | * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ )
trans ( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n ( fun x => ( ψ ) x ) x ‖ )
+ ( | x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) ( fun x => ( ψ ) x ) x ‖ ) 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ( ( ↑ n + 1 ) * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ + | x | * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ )
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ( ( ↑ n + 1 ) * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ + | x | * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ) ≤
( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ apply le_of_eq 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ( ( ↑ n + 1 ) * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ + | x | * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ) =
( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖
ring All goals completed! 🐙
trans ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k ( n ) ψ )
+ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ψ ) 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤
( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ )
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) +
| x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤
( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ apply add_le_add _ _ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ) ≤ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
apply mul_le_mul_of_nonneg_left _ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ 0 ≤ ↑ n + 1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
refine Left.add_nonneg ? _ ? _ refine_1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ 0 ≤ ↑ n refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ 0 ≤ 1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
· refine_1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ 0 ≤ ↑ n exact Nat.cast_nonneg' n All goals completed! 🐙
· refine_2 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ 0 ≤ 1 exact zero_le_one' ℝ All goals completed! 🐙
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ k * ‖ iteratedFDeriv ℝ n (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 k n ) ψ exact ψ . le_seminorm 𝕜 k n x All goals completed! 🐙
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ | x | ^ ( k + 1 ) * ‖ iteratedFDeriv ℝ ( n + 1 ) (fun x => ψ x ) x ‖ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ exact ψ . le_seminorm 𝕜 ( k + 1 ) ( n + 1 ) x All goals completed! 🐙
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ) by_cases h1 : ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ) <
( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) pos 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ) neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ¬ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ )
· pos 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ) rw [ max_eq_left_of_lt h1 pos 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ pos 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ ] pos 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ
trans ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ
apply add_le_add h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤ ( SchwartzMap.seminorm 𝕜 k n ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ
· h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ simp All goals completed! 🐙
· h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤ ( SchwartzMap.seminorm 𝕜 k n ) ψ exact le_of_lt h1 All goals completed! 🐙
apply le_of_eq 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 k n ) ψ =
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ
ring All goals completed! 🐙
· neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ¬ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ < ( SchwartzMap.seminorm 𝕜 k n ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ) simp at h1 neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * max ( ( SchwartzMap.seminorm 𝕜 k n ) ψ ) ( ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ )
rw [ max_eq_right h1 neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ] neg 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
trans ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ +
( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ apply add_le_add h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
· h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ apply mul_le_mul_of_nonneg_left _ h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ 0 ≤ ↑ n + 1 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
· h₁ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ 0 ≤ ↑ n + 1 linarith All goals completed! 🐙
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ exact h1 All goals completed! 🐙
· h₂ 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ simp All goals completed! 🐙
· 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ≤
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ apply le_of_eq 𝕜 : Type E : Type F : Type inst✝³ : RCLike 𝕜 inst✝² : NormedAddCommGroup E inst✝¹ : NormedAddCommGroup F inst✝ : NormedSpace ℝ E k : ℕ n✝ : ℕ ψ : 𝓢( ℝ , 𝕜 ) x : ℝ n : ℕ h1 : ( SchwartzMap.seminorm 𝕜 k n ) ψ ≤ ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ ⊢ ( ↑ n + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ + ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ =
( ↑ n + 1 + 1 ) * ( SchwartzMap.seminorm 𝕜 ( k + 1 ) ( n + 1 ) ) ψ
ring All goals completed! 🐙
lemma powOneMul_apply ( ψ : 𝓢( ℝ , 𝕜 ) ) ( x : ℝ ) :
powOneMul 𝕜 ψ x = x * ψ x := rfl