-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem integrable_withDensity_iff_integrable_coe_smul {f : α → ℝ≥0} (hf : Measurable f)
    {g : α → E} :
    Integrable g (μ.withDensity fun x => f x) ↔ Integrable (fun x => (f x : ℝ) • g x) μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable (fun a => ‖g a‖ₑ) (μ.withDensity fun x => ↑(f x))

Tactic:
simpa [aemeasurable_withDensity_ennreal_iff hf, enorm_smul] using H.enorm

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable (fun x => ↑(f x) • g x) μ

Tactic:
by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable (fun x => ↑(f x) • g x) μ

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable (fun x => ↑(f x) • g x) μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ ∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ‖g a‖ₑ) a ∂μ < ⊤ ↔ ∫⁻ (a : α), ‖↑(f a) • g a‖ₑ ∂μ < ⊤

Tactic:
simp [enorm_smul]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable (fun x => ↑(f x) • g x) μ

Tactic:
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, hasFiniteIntegral_iff_enorm, H,
  true_and]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun x => ↑(f x)) < ⊤ ↔ ∫⁻ (a : α), ‖↑(f a) • g a‖ₑ ∂μ < ⊤

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g (μ.withDensity fun x => ↑(f x)) ↔ Integrable (fun x => ↑(f x) • g x) μ

Tactic:
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ‖g a‖ₑ ∂μ.withDensity fun x => ↑(f x)) < ⊤ ↔ ∫⁻ (a : α), ‖↑(f a) • g a‖ₑ ∂μ < ⊤

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ ∫⁻ (a : α), ((fun x => ↑(f x)) * fun a => ‖g a‖ₑ) a ∂μ < ⊤ ↔ ∫⁻ (a : α), ‖↑(f a) • g a‖ₑ ∂μ < ⊤

case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_6
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable (fun a => ‖g a‖ₑ) (μ.withDensity fun x => ↑(f x))