Theorem: IsBump.integrable (ForML/Bump.lean)

State before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable f
Tactic:
apply Continuous.integrable_of_hasCompactSupport
State after:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f

State before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f

case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
. exact ContDiff.continuous hf.right
State after:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f

State before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
. exact hf.left
State after:
no goals

State before:
case hf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous f
Tactic:
exact ContDiff.continuous hf.right
State after:
no goals

State before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f : α → ℝ
hf : IsBump f
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport f
Tactic:
exact hf.left
State after:
no goals