case pos
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ

case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
by_cases hg : Integrable g (μ.withDensity fun x => f x)
case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ

case pos
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
case pos
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ

case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
swap
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤ →
        (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ)
          (indicator s fun x => c)

case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ ⦃f_1 g : α → E⦄,
    Disjoint (support f_1) (support g) →
      Integrable f_1 →
        Integrable g →
          (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) f_1 →
            (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) g →
              (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) (f_1 + g)

case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}

case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ ⦃f_1 g : α → E⦄,
    f_1 =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g →
      Integrable f_1 →
        (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) f_1 →
          (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) g
case pos
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
refine' Integrable.induction
  (P := fun g => (∫ a, g a ∂μ.withDensity fun x => f x) = ∫ a, f a • g a ∂μ) _ _ _ _ hg
case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ ¬Integrable fun a => f a • g a
case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ
rw [integral_undef hg, integral_undef]
no goals
case neg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : ¬Integrable g
⊢ ¬Integrable fun a => f a • g a
rwa [← integrable_withDensity_iff_integrable_smul f_meas]
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ fun x => ↑(f x)) =
    ∫ (a : α), f a • indicator s (fun x => c) a ∂μ
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ (c : E) ⦃s : Set α⦄,
    MeasurableSet s →
      ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤ →
        (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ)
          (indicator s fun x => c)
intro c s s_meas hs
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, c ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • indicator s (fun x => c) a ∂μ
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (a : α), indicator s (fun x => c) a ∂Measure.withDensity μ fun x => ↑(f x)) =
    ∫ (a : α), f a • indicator s (fun x => c) a ∂μ
rw [integral_indicator s_meas]
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, c ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (x : α) in s, f x • c ∂μ
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, c ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • indicator s (fun x => c) a ∂μ
simp_rw [← indicator_smul_apply, integral_indicator s_meas]
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ ENNReal.toReal (∫⁻ (x : α) in s, ↑(f x) ∂μ) • c = ∫ (x : α) in s, f x • c ∂μ
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, c ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (x : α) in s, f x • c ∂μ
simp only [s_meas, integral_const, Measure.restrict_apply', univ_inter, withDensity_apply]
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, ↑(f x) • c ∂μ) = ∫ (x : α) in s, f x • c ∂μ

case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ 0 ≤ ∫ (a : α) in s, ↑(f a) ∂μ

case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ Integrable fun x => ↑(f x)
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ ENNReal.toReal (∫⁻ (x : α) in s, ↑(f x) ∂μ) • c = ∫ (x : α) in s, f x • c ∂μ
rw [lintegral_coe_eq_integral, ENNReal.toReal_ofReal, ← integral_smul_const]
no goals
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ (∫ (x : α) in s, ↑(f x) • c ∂μ) = ∫ (x : α) in s, f x • c ∂μ
rfl
no goals
case pos.refine'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ 0 ≤ ∫ (a : α) in s, ↑(f a) ∂μ
exact integral_nonneg fun x => NNReal.coe_nonneg _
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ HasFiniteIntegral fun x => ↑(f x)
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ Integrable fun x => ↑(f x)
refine' ⟨f_meas.coe_nnreal_real.aemeasurable.aestronglyMeasurable, _⟩
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
⊢ HasFiniteIntegral fun x => ↑(f x)
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : ↑↑(Measure.withDensity μ fun x => ↑(f x)) s < ⊤
⊢ HasFiniteIntegral fun x => ↑(f x)
rw [withDensity_apply _ s_meas] at hs
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
⊢ (∫⁻ (a : α) in s, ↑‖↑(f a)‖₊ ∂μ) < ⊤
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
⊢ HasFiniteIntegral fun x => ↑(f x)
rw [HasFiniteIntegral]
case h.e'_3.h.e'_4.h.h.e'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
x : α
⊢ ‖↑(f x)‖₊ = f x
case pos.refine'_1.hfi
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
⊢ (∫⁻ (a : α) in s, ↑‖↑(f a)‖₊ ∂μ) < ⊤
convert hs with x
no goals
case h.e'_3.h.e'_4.h.h.e'_1
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
c : E
s : Set α
s_meas : MeasurableSet s
hs : (∫⁻ (a : α) in s, ↑(f a) ∂μ) < ⊤
x : α
⊢ ‖↑(f x)‖₊ = f x
simp only [NNReal.nnnorm_eq]
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), (u + u') a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • (u + u') a ∂μ
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ ⦃f_1 g : α → E⦄,
    Disjoint (support f_1) (support g) →
      Integrable f_1 →
        Integrable g →
          (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) f_1 →
            (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) g →
              (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) (f_1 + g)
intro u u' _ u_int u'_int h h'
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), u a + u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • (u a + u' a) ∂μ
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), (u + u') a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • (u + u') a ∂μ
change
  (∫ a : α, u a + u' a ∂μ.withDensity fun x : α => ↑(f x)) = ∫ a : α, f a • (u a + u' a) ∂μ
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), u a + u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a + f a • u' a ∂μ
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), u a + u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • (u a + u' a) ∂μ
simp_rw [smul_add]
case pos.refine'_2.hf
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ Integrable fun a => f a • u a

case pos.refine'_2.hg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ Integrable fun a => f a • u' a
case pos.refine'_2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ (∫ (a : α), u a + u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a + f a • u' a ∂μ
rw [integral_add u_int u'_int, h, h', integral_add]
no goals
case pos.refine'_2.hf
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ Integrable fun a => f a • u a
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u_int
no goals
case pos.refine'_2.hg
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u u' : α → E
a✝ : Disjoint (support u) (support u')
u_int : Integrable u
u'_int : Integrable u'
h : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
h' : (∫ (a : α), u' a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u' a ∂μ
⊢ Integrable fun a => f a • u' a
exact (integrable_withDensity_iff_integrable_smul f_meas).1 u'_int
case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}
case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}
have C1 :
  Continuous fun u : Lp E 1 (μ.withDensity fun x => f x) =>
    ∫ x, u x ∂μ.withDensity fun x => f x :=
  continuous_integral
case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
C2 : Continuous fun u => ∫ (x : α), f x • ↑↑u x ∂μ
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}
case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}
have C2 : Continuous fun u : Lp E 1 (μ.withDensity fun x => f x) => ∫ x, f x • u x ∂μ := by
  have : Continuous ((fun u : Lp E 1 μ => ∫ x, u x ∂μ) ∘ withDensitySMulLI (E := E) μ f_meas) :=
    continuous_integral.comp (withDensitySMulLI (E := E) μ f_meas).continuous
  convert this with u
  simp only [Function.comp_apply, withDensitySMulLI_apply]
  exact integral_congr_ae (memℒ1_smul_of_L1_withDensity f_meas u).coeFn_toLp.symm
no goals
case pos.refine'_3
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
C2 : Continuous fun u => ∫ (x : α), f x • ↑↑u x ∂μ
⊢ IsClosed {f_1 | (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) ↑↑f_1}
exact isClosed_eq C1 C2
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
⊢ Continuous fun u => ∫ (x : α), f x • ↑↑u x ∂μ
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
⊢ Continuous fun u => ∫ (x : α), f x • ↑↑u x ∂μ
have : Continuous ((fun u : Lp E 1 μ => ∫ x, u x ∂μ) ∘ withDensitySMulLI (E := E) μ f_meas) :=
  continuous_integral.comp (withDensitySMulLI (E := E) μ f_meas).continuous
case h.e'_5.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
u : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α), f x • ↑↑u x ∂μ) = ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas)) u
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
⊢ Continuous fun u => ∫ (x : α), f x • ↑↑u x ∂μ
convert this with u
case h.e'_5.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
u : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α), f x • ↑↑u x ∂μ) =
    ∫ (x : α), ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x ∂μ
case h.e'_5.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
u : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α), f x • ↑↑u x ∂μ) = ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas)) u
simp only [Function.comp_apply, withDensitySMulLI_apply]
no goals
case h.e'_5.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
C1 : Continuous fun u => ∫ (x : α), ↑↑u x ∂Measure.withDensity μ fun x => ↑(f x)
this : Continuous ((fun u => ∫ (x : α), ↑↑u x ∂μ) ∘ ↑(withDensitySMulLI μ f_meas))
u : { x // x ∈ Lp E 1 }
⊢ (∫ (x : α), f x • ↑↑u x ∂μ) =
    ∫ (x : α), ↑↑(Memℒp.toLp (fun x => f x • ↑↑u x) (_ : Memℒp (fun x => f x • ↑↑u x) 1)) x ∂μ
exact integral_congr_ae (memℒ1_smul_of_L1_withDensity f_meas u).coeFn_toLp.symm
case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (∫ (a : α), v a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • v a ∂μ
case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
⊢ ∀ ⦃f_1 g : α → E⦄,
    f_1 =ᵐ[Measure.withDensity μ fun x => ↑(f x)] g →
      Integrable f_1 →
        (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) f_1 →
          (fun g => (∫ (a : α), g a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • g a ∂μ) g
intro u v huv _ hu
case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (∫ (a : α), f a • u a ∂μ) = ∫ (a : α), f a • v a ∂μ
case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (∫ (a : α), v a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • v a ∂μ
rw [← integral_congr_ae huv, hu]
case pos.refine'_4.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (fun a => f a • u a) =ᵐ[μ] fun a => f a • v a
case pos.refine'_4
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (∫ (a : α), f a • u a ∂μ) = ∫ (a : α), f a • v a ∂μ
apply integral_congr_ae
case h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
⊢ f x • u x = f x • v x
case pos.refine'_4.h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
⊢ (fun a => f a • u a) =ᵐ[μ] fun a => f a • v a
filter_upwards [(ae_withDensity_iff f_meas.coe_nnreal_ennreal).1 huv] with x hx
case h.inl
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x = 0
⊢ f x • u x = f x • v x

case h.inr
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ f x • u x = f x • v x
case h
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
⊢ f x • u x = f x • v x
rcases eq_or_ne (f x) 0 with (h'x | h'x)
no goals
case h.inl
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x = 0
⊢ f x • u x = f x • v x
simp only [h'x, zero_smul]
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ ↑(f x) ≠ 0
case h.inr
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ f x • u x = f x • v x
rw [hx _]
no goals
α : Type u_1
β : Type ?u.4336751
E : Type u_2
F : Type ?u.4336757
inst✝⁹ : MeasurableSpace α
ι : Type ?u.4336763
inst✝⁸ : NormedAddCommGroup E
μ : MeasureTheory.Measure α
𝕜 : Type ?u.4451571
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
f_meas : Measurable f
g : α → E
hg : Integrable g
u v : α → E
huv : u =ᵐ[Measure.withDensity μ fun x => ↑(f x)] v
a✝ : Integrable u
hu : (∫ (a : α), u a ∂Measure.withDensity μ fun x => ↑(f x)) = ∫ (a : α), f a • u a ∂μ
x : α
hx : ↑(f x) ≠ 0 → u x = v x
h'x : f x ≠ 0
⊢ ↑(f x) ≠ 0
simpa only [Ne.def, ENNReal.coe_eq_zero] using h'x