Theorem: SchwartzMap.Real.norm_integral_pow_smul_iteratedDeriv_bound (ForML/SchwartzRealFourier.lean)

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
generalize hg : hasTemperateGrowth_smul (Function.hasTemperateGrowth_pow k)
    (iteratedPDeriv ℝ (fun _ ↦ 1 : Fin n → ℝ) f) = g
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
have (x : ℝ) : x ^ k • iteratedDeriv n f x = g x := by
  simp [← hg, hasTemperateGrowth_smul_apply, iteratedPDeriv_eq_iteratedFDeriv,
    iteratedDeriv_eq_iteratedFDeriv]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x‖ ≤ C
Tactic:
simp only [this]
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∀ (x : ℝ), x ^ k • iteratedDeriv n (⇑f) x = g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
clear this
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
have := g.integrable.hasFiniteIntegral
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : HasFiniteIntegral fun x => g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : HasFiniteIntegral fun x => g x
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
rw [HasFiniteIntegral, lt_top_iff_ne_top, WithTop.ne_top_iff_exists] at this
State after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∃ a, ↑a = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
this : ∃ a, ↑a = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
rcases this with ⟨C, hC⟩
State after:
case intro
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C

State before:
case intro
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∃ C, 0 ≤ C ∧ ‖∫ (x : ℝ), g x‖ ≤ C
Tactic:
use C.val
State after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ 0 ≤ ↑C ∧ ‖∫ (x : ℝ), g x‖ ≤ ↑C

State before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ 0 ≤ ↑C ∧ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Tactic:
refine And.intro C.prop ?_
State after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ‖∫ (x : ℝ), g x‖ ≤ ↑C

State before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ‖∫ (x : ℝ), g x‖ ≤ ↑C
Tactic:
refine le_trans (norm_integral_le_lintegral_norm _) ?_
State after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ENNReal.toReal (∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖) ≤ ↑C

State before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ENNReal.toReal (∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖) ≤ ↑C
Tactic:
refine ENNReal.toReal_le_of_le_ofReal C.prop ?_
State after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C

State before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (a : ℝ), ENNReal.ofReal ‖g a‖ ≤ ENNReal.ofReal ↑C
Tactic:
refine le_trans (lintegral_ofReal_le_lintegral_nnnorm _) ?_
State after:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (x : ℝ), ↑‖‖g x‖‖₊ ≤ ENNReal.ofReal ↑C

State before:
case h
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
C : NNReal
hC : ↑C = ∫⁻ (a : ℝ), ↑‖g a‖₊
⊢ ∫⁻ (x : ℝ), ↑‖‖g x‖‖₊ ≤ ENNReal.ofReal ↑C
Tactic:
simp [← hC]
State after:
no goals

State before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
g : 𝓢(ℝ, F)
hg : (hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => x ^ k)) ((iteratedPDeriv ℝ fun x => 1) f) = g
x : ℝ
⊢ x ^ k • iteratedDeriv n (⇑f) x = g x
Tactic:
simp [← hg, hasTemperateGrowth_smul_apply, iteratedPDeriv_eq_iteratedFDeriv,
  iteratedDeriv_eq_iteratedFDeriv]
State after:
no goals