case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ↑↑μ s = 0
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]

case neg
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ¬↑↑μ s = 0
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
by_cases hse : μ s = 0
case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : s =ᶠ[ae μ] ∅
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ↑↑μ s = 0
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
rw [← ae_eq_empty] at hse
case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : s =ᶠ[ae μ] ∅
⊢ (⨍ (x : α) in t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : s =ᶠ[ae μ] ∅
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
rw [restrict_congr_set (hse.union EventuallyEq.rfl), empty_union]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : s =ᶠ[ae μ] ∅
⊢ (⨍ (x : α) in t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
exact right_mem_segment _ _ _
case neg
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ¬↑↑μ s = 0
⊢ 0 < ENNReal.toReal (↑↑μ s) + ENNReal.toReal (↑↑μ t)
case neg
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ¬↑↑μ s = 0
⊢ (⨍ (x : α) in s ∪ t, f x ∂μ) ∈ [⨍ (x : α) in s, f x ∂μ-[ℝ]⨍ (x : α) in t, f x ∂μ]
refine'
  mem_segment_iff_div.mpr
    ⟨(μ s).toReal, (μ t).toReal, ENNReal.toReal_nonneg, ENNReal.toReal_nonneg, _,
      (average_union hd ht hsμ htμ hfs hft).symm⟩
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.222922
m0 : MeasurableSpace α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : CompleteSpace E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
μ : Measure α
s✝ : Set E
f : α → E
s t : Set α
hd : AEDisjoint μ s t
ht : NullMeasurableSet t
hsμ : ↑↑μ s ≠ ⊤
htμ : ↑↑μ t ≠ ⊤
hfs : IntegrableOn f s
hft : IntegrableOn f t
hse : ¬↑↑μ s = 0
⊢ 0 < ENNReal.toReal (↑↑μ s) + ENNReal.toReal (↑↑μ t)
calc
  0 < (μ s).toReal := ENNReal.toReal_pos hse hsμ
  _ ≤ _ := le_add_of_nonneg_right ENNReal.toReal_nonneg