-- 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
⊢ ∫ (ω : Ω), f ω ∂μ ≤ (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖f‖

Tactic:
rw [BoundedContinuousFunction.integral_eq_integral_meas_le f μ f_nn]

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 : ℝ) in Ioc 0 ‖f‖, (μ {a | t ≤ f a}).toReal ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (ν (thickening ε {a | t ≤ f a})).toReal) + ε * ‖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 + ε
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

Tactic:
exact intble₂.add <| integrable_const ε

Result:
no goals

Proof state:
case hg
Ω : 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
⊢ Integrable (fun x => ε) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
exact integrable_const ε

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
t : ℝ
⊢ (fun t => (μ {a | t ≤ f a}).toReal) t ≤ (fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε) t

Tactic:
convert ENNReal.toReal_mono ?_ <| left_measure_le_of_levyProkhorovEDist_lt hμν
  (B := {a | t ≤ f a}) (f.continuous.measurable measurableSet_Ici)

Result:
case h.e'_4
Ω : 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 => (ν (thickening ε {a | t ≤ f a})).toReal + ε) t =
    (ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε).toReal

Ω : 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 : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ⊤

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
t : ℝ
⊢ ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε ≠ ⊤

Tactic:
exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩

Result:
no goals

Proof state:
case h.e'_4
Ω : 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 => (ν (thickening ε {a | t ≤ f a})).toReal + ε) t =
    (ν (thickening (ENNReal.ofReal ε).toReal {a | t ≤ f a}) + ENNReal.ofReal ε).toReal

Tactic:
rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]

Result:
no goals

Proof state:
case hf
Ω : 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
⊢ Integrable (fun x => (ν (thickening ε {a | x ≤ f a})).toReal) (volume.restrict (Ioc 0 ‖f‖))

Tactic:
exact intble₂

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
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

Tactic:
exact intble₁

Result:
no goals

Proof state:
case f_bdd
Ω : 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 + ε
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict (Ioc 0 ‖f‖), ‖(μ {a_1 | a ≤ f a_1}).toReal‖ ≤ (μ univ).toReal

Tactic:
apply Eventually.of_forall <| fun 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
key : (fun t => (μ {a | t ≤ f a}).toReal) ≤ fun t => (ν (thickening ε {a | t ≤ f a})).toReal + ε
t : ℝ
⊢ ‖(μ {a | t ≤ f a}).toReal‖ ≤ (μ univ).toReal