Theorem: SchwartzMap.snorm_top_lt_top (ForML/SchwartzLp.lean)

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⟩
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 < ⊤

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
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 < ⊤

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)
State after:
no goals