α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.308351
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : Countable β
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : C(α, E)
s : β → Compacts α
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
i : β
⊢ (∫ (a : α) in ↑(s i), ‖↑f a‖ ∂μ) ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.308351
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : Countable β
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : C(α, E)
s : β → Compacts α
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
⊢ IntegrableOn (↑f) (⋃ (i : β), ↑(s i))
refine'
  integrableOn_iUnion_of_summable_integral_norm (fun i => (s i).isCompact.isClosed.measurableSet)
    (fun i => (map_continuous f).continuousOn.integrableOn_compact (s i).isCompact)
    (summable_of_nonneg_of_le (fun ι => integral_nonneg fun x => norm_nonneg _) (fun i => _) hf)
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.308351
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : Countable β
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : C(α, E)
s : β → Compacts α
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
i : β
⊢ ‖∫ (x : α) in ↑(s i), ‖↑f x‖ ∂μ‖ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.308351
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : Countable β
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : C(α, E)
s : β → Compacts α
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
i : β
⊢ (∫ (a : α) in ↑(s i), ‖↑f a‖ ∂μ) ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
rw [← (Real.norm_of_nonneg (integral_nonneg fun a => norm_nonneg _) : ‖_‖ = ∫ x in s i, ‖f x‖ ∂μ)]
no goals
α : Type u_1
β : Type u_3
E : Type u_2
F : Type ?u.308351
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : Countable β
inst✝³ : TopologicalSpace α
inst✝² : BorelSpace α
inst✝¹ : MetrizableSpace α
inst✝ : IsLocallyFiniteMeasure μ
f : C(α, E)
s : β → Compacts α
hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
i : β
⊢ ‖∫ (x : α) in ↑(s i), ‖↑f x‖ ∂μ‖ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * ENNReal.toReal (↑↑μ ↑(s i))
exact
  norm_set_integral_le_of_norm_le_const' (s i).isCompact.measure_lt_top
    (s i).isCompact.isClosed.measurableSet fun x hx =>
    (norm_norm (f x)).symm ▸ (f.restrict (s i : Set α)).norm_coe_le_norm ⟨x, hx⟩