Theorem: SchwartzMap.snorm_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)
p : ENNReal
⊢ snorm (⇑f) p volume < ⊤
Tactic:
cases p with
| none => exact snorm_top_lt_top f
| some p =>
  simp
  cases eq_or_lt_of_le (zero_le p) with
  | inl hp => simp [← hp]
  | inr hp => exact snorm_nnreal_lt_top f hp
State after:
no goals

State before:
case none
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) none volume < ⊤
Tactic:
exact snorm_top_lt_top f
State after:
no goals

State before:
case some
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)
p : NNReal
⊢ snorm (⇑f) (some p) volume < ⊤
Tactic:
simp
State after:
case some
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)
p : NNReal
⊢ snorm (⇑f) (↑p) volume < ⊤

State before:
case some
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)
p : NNReal
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
cases eq_or_lt_of_le (zero_le p) with
| inl hp => simp [← hp]
| inr hp => exact snorm_nnreal_lt_top f hp
State after:
no goals

State before:
case some.inl
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)
p : NNReal
hp : 0 = p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
simp [← hp]
State after:
no goals

State before:
case some.inr
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)
p : NNReal
hp : 0 < p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
exact snorm_nnreal_lt_top f hp
State after:
no goals