case h.e'_3
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ ↑↑μ E = lintegral μ (indicator E fun x => 1)

α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (indicator E fun x => 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ ↑↑μ E ≤ ∫⁻ (a : α), thickenedIndicatorAux δ E a ∂μ
convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)
case h.e'_3
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ ↑↑μ E = ∫⁻ (a : α) in E, 1 ∂μ
case h.e'_3
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ ↑↑μ E = lintegral μ (indicator E fun x => 1)
rw [lintegral_indicator _ E_mble]
no goals
case h.e'_3
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ ↑↑μ E = ∫⁻ (a : α) in E, 1 ∂μ
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]
case hfg
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ (fun a => indicator E (fun x => 1) a) ≤ fun a => thickenedIndicatorAux δ E a
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (indicator E fun x => 1) ≤ lintegral μ (thickenedIndicatorAux δ E)
apply lintegral_mono
no goals
case hfg
α : Type u_1
β : Type ?u.4893923
E✝ : Type ?u.4893926
F : Type ?u.4893929
inst✝² : MeasurableSpace α
ι : Type ?u.4893935
inst✝¹ : NormedAddCommGroup E✝
inst✝ : PseudoEMetricSpace α
μ : MeasureTheory.Measure α
E : Set α
E_mble : MeasurableSet E
δ : ℝ
⊢ (fun a => indicator E (fun x => 1) a) ≤ fun a => thickenedIndicatorAux δ E a
apply indicator_le_thickenedIndicatorAux