-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- Assuming `levyProkhorovEDist μ ν < ε`, we can bound `∫ f ∂μ` in terms of
`∫ t in (0, ‖f‖], ν (thickening ε {x | f(x) ≥ t}) dt` and `‖f‖`. -/
lemma BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt (μ ν : Measure Ω)
    [IsFiniteMeasure μ] [IsFiniteMeasure ν] {ε : ℝ} (ε_pos : 0 < ε)
    (hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε) (f : Ω →ᵇ ℝ) (f_nn : 0 ≤ᵐ[μ] f) :
    ∫ ω, f ω ∂μ
      ≤ (∫ t in Ioc 0 ‖f‖, ENNReal.toReal (ν (thickening ε {a | t ≤ f a}))) + ε * ‖f‖

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
t : ℝ
⊢ ‖(μ {a | t ≤ f a}).toReal‖ ≤ (μ univ).toReal

Tactic:
simp only [Real.norm_eq_abs, abs_toReal]

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
t : ℝ
⊢ (μ {a | t ≤ f a}).toReal ≤ (μ univ).toReal

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
⊢ Antitone fun x => μ {a | x ≤ f a}

Tactic:
exact fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)

Result:
no goals

Proof state:
case bc
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume
⊢ ∫ (a : ℝ) in Ioc 0 ‖f‖, ε ≤ ε * ‖f‖

Tactic:
simp only [integral_const, MeasurableSet.univ, Measure.restrict_apply, univ_inter,
            Real.volume_Ioc, sub_zero, norm_nonneg, toReal_ofReal, smul_eq_mul,
            (mul_comm _ ε).le]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
⊢ (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε

Tactic:
intro t

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
t : ℝ
⊢ (fun t => (μ {a | t ≤ f a}).toReal) t ≤ (fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε) t

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
t : ℝ
⊢ (μ {a | t ≤ f a}).toReal ≤ (μ univ).toReal

Tactic:
exact ENNReal.toReal_mono (measure_ne_top _ _) <| measure_mono (subset_univ _)

Result:
no goals

Proof state:
case f_mble
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
⊢ AEStronglyMeasurable (fun t => (μ {a | t ≤ f a}).toReal) volume

Tactic:
apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
⊢ Antitone fun x => μ {a | x ≤ f a}

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume
⊢ ∫ (t : ℝ) in Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖

Tactic:
apply le_trans (setIntegral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key)

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume
⊢ ∫ (x : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | x ≤ f a})).toReal + ε ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖

Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume

Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : 0 ≤ᶠ[ae μ] ⇑f
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
intble₁ : IntegrableOn (fun t => (μ {a | t ≤ f a}).toReal) (Ioc 0 ‖f‖) volume
intble₂ : IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal) (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε) (Ioc 0 ‖f‖) volume