α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
let f' := hf.mk _
no goals
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
calc
  (∫ a, g a ∂μ.withDensity fun x => f x) = ∫ a, g a ∂μ.withDensity fun x => f' x := by
    congr 1
    apply withDensity_congr_ae
    filter_upwards [hf.ae_eq_mk] with x hx
    rw [hx]
  _ = ∫ a, f' a • g a ∂μ := (integral_withDensity_eq_integral_smul hf.measurable_mk _)
  _ = ∫ a, f a • g a ∂μ := by
    apply integral_congr_ae
    filter_upwards [hf.ae_eq_mk] with x hx
    rw [hx]
case e_μ
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (Measure.withDensity μ fun x => ↑(f x)) = Measure.withDensity μ fun x => ↑(f' x)
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f' x)
congr 1
case e_μ.h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(f' x)
case e_μ
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (Measure.withDensity μ fun x => ↑(f x)) = Measure.withDensity μ fun x => ↑(f' x)
apply withDensity_congr_ae
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
case e_μ.h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (fun x => ↑(f x)) =ᵐ[μ] fun x => ↑(f' x)
filter_upwards [hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ ↑(f x) = ↑(AEMeasurable.mk f hf x)
rw [hx]
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (fun a => f' a • g a) =ᵐ[μ] fun a => f a • g a
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (∫ (a : α), f' a • g a ∂μ) = ∫ (a : α), f a • g a ∂μ
apply integral_congr_ae
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x • g x = f x • g x
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
⊢ (fun a => f' a • g a) =ᵐ[μ] fun a => f a • g a
filter_upwards [hf.ae_eq_mk] with x hx
no goals
case h
α : Type u_1
β : Type ?u.4515315
E : Type u_2
F : Type ?u.4515321
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4515327
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4630135
inst✝⁷ : IsROrC 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
p : ℝ≥0∞
inst✝³ : CompleteSpace E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace F
inst✝ : NormedSpace ℝ F
f : α → ℝ≥0
hf : AEMeasurable f
g : α → E
f' : α → ℝ≥0 := AEMeasurable.mk f hf
x : α
hx : f x = AEMeasurable.mk f hf x
⊢ AEMeasurable.mk f hf x • g x = f x • g x
rw [hx]