-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
    [NormedSpace ℝ E] [OpensMeasurableSpace X] [T2Space X] {f : X → ℝ} (hf : LocallyIntegrable f μ)
    {g : X → E} (hg : Continuous g) (h'g : HasCompactSupport g) :
    Integrable (fun x ↦ f x • g x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ (support fun x => f x • g x) ⊆ K

Tactic:
apply support_subset_iff'.2

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ ∀ x ∉ K, f x • g x = 0

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ ∀ x ∉ K, f x • g x = 0

Tactic:
intros x hx

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
x : X
hx : x ∉ K
⊢ f x • g x = 0

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (fun x => f x • g x) μ

Tactic:
rw [← this, indicator_smul_left]

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (fun a => K.indicator f a • g a) μ

Proof state:
case hφ
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ IntegrableOn f K μ

Tactic:
exact hf.integrableOn_isCompact hK

Result:
no goals

Proof state:
case hφ
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (K.indicator f) μ

Tactic:
rw [integrable_indicator_iff hK.measurableSet]

Result:
case hφ
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ IntegrableOn f K μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (fun a => K.indicator f a • g a) μ

Tactic:
apply Integrable.smul_of_top_left

Result:
case hφ
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (K.indicator f) μ

case hf
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ MemLp g ⊤ μ

Proof state:
case hf
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ MemLp g ⊤ μ

Tactic:
exact hg.memLp_top_of_hasCompactSupport h'g μ

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
⊢ Integrable (fun x => f x • g x) μ

Tactic:
have hK : IsCompact K := h'g

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Integrable (fun x => f x • g x) μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
⊢ Integrable (fun x => f x • g x) μ

Tactic:
have : K.indicator (fun x ↦ f x • g x) = (fun x ↦ f x • g x) := by
  apply indicator_eq_self.2
  apply support_subset_iff'.2
  intros x hx
  simp [image_eq_zero_of_nmem_tsupport hx]

Result:
X : Type u_1
E : Type u_3
inst✝⁵ : MeasurableSpace X
inst✝⁴ : TopologicalSpace X
inst✝³ : NormedAddCommGroup E
μ : Measure X
inst✝² : NormedSpace ℝ E
inst✝¹ : OpensMeasurableSpace X
inst✝ : T2Space X
f : X → ℝ
hf : LocallyIntegrable f μ
g : X → E
hg : Continuous g
h'g : HasCompactSupport g
K : Set X := tsupport g
hK : IsCompact K
this : (K.indicator fun x => f x • g x) = fun x => f x • g x
⊢ Integrable (fun x => f x • g x) μ