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

State before:
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Integrable (f * g)
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✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)

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

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

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

State before:
case hcf
α : Type u_1
inst✝⁴ : NormedAddCommGroup α
inst✝³ : NormedSpace ℝ α
inst✝² : MeasurableSpace α
inst✝¹ : OpensMeasurableSpace α
f✝ : α → ℝ
hf✝ : IsBump f✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ HasCompactSupport (f * g)
Tactic:
. apply HasCompactSupport.mul_right 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✝
f g : α → ℝ
hf : IsBump f
hg : Continuous g
μ : autoParam (Measure α) _auto✝
inst✝ : IsLocallyFiniteMeasure μ
⊢ Continuous (f * g)
Tactic:
exact Continuous.mul hf.continuous hg
State after:
no goals

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