case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x

case neg
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ↑‖g a‖₊ ∂Measure.withDensity μ fun x => ↑(f x)) < ⊤ ↔ (∫⁻ (a : α), ↑‖↑(f a) • g a‖₊ ∂μ) < ⊤
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, HasFiniteIntegral, H,
  true_and_iff]
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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‖₊
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (∫⁻ (a : α), ↑‖g a‖₊ ∂Measure.withDensity μ fun x => ↑(f x)) < ⊤ ↔ (∫⁻ (a : α), ↑‖↑(f a) • g a‖₊ ∂μ) < ⊤
rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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‖₊ ∂μ) < ⊤
rw [iff_iff_eq]
case pos.e_a.e_f
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun a => ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) a) = fun a => ↑‖↑(f a) • g a‖₊
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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‖₊ ∂μ) < ⊤)
congr
case pos.e_a.e_f.h
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) x = ↑‖↑(f x) • g x‖₊
case pos.e_a.e_f
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun a => ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) a) = fun a => ↑‖↑(f a) • g a‖₊
ext1 x
no goals
case pos.e_a.e_f.h
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ((fun x => ↑(f x)) * fun a => ↑‖g a‖₊) x = ↑‖↑(f x) • g x‖₊
simp only [nnnorm_smul, NNReal.nnnorm_eq, coe_mul, Pi.mul_apply]
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable fun x => ↑(f x) * ↑‖g x‖₊
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
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‖₊
rw [aemeasurable_withDensity_ennreal_iff hf]
case h.e'_5
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun x => ↑(f x) * ↑‖g x‖₊) = fun a => ↑‖↑(f a) • g a‖₊
case pos
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ AEMeasurable fun x => ↑(f x) * ↑‖g x‖₊
convert H.ennnorm using 1
case h.e'_5.h
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ↑(f x) * ↑‖g x‖₊ = ↑‖↑(f x) • g x‖₊
case h.e'_5
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ (fun x => ↑(f x) * ↑‖g x‖₊) = fun a => ↑‖↑(f a) • g a‖₊
ext1 x
no goals
case h.e'_5.h
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
x : α
⊢ ↑(f x) * ↑‖g x‖₊ = ↑‖↑(f x) • g x‖₊
simp only [nnnorm_smul, NNReal.nnnorm_eq, coe_mul]
no goals
case neg
α : Type u_1
β : Type ?u.1006363
γ : Type ?u.1006366
δ : Type ?u.1006369
m : MeasurableSpace α
μ ν : Measure α
inst✝⁴ : MeasurableSpace δ
inst✝³ : NormedAddCommGroup β
inst✝² : NormedAddCommGroup γ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0
hf : Measurable f
g : α → E
H : ¬AEStronglyMeasurable (fun x => ↑(f x) • g x) μ
⊢ Integrable g ↔ Integrable fun x => ↑(f x) • g x
simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and_iff]