-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- The identity map `LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω` is continuous. -/
lemma LevyProkhorov.continuous_equiv_probabilityMeasure :
    Continuous (LevyProkhorov.equiv (α := ProbabilityMeasure Ω))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto
    ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ levyProkhorovEDist ↑(Ps n) ↑P = ENNReal.ofReal (dist (μs n) ν)

Tactic:
rw [LevyProkhorov.dist_def, levyProkhorovDist, ofReal_toReal (levyProkhorovEDist_ne_top _ _)]

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto
    ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ levyProkhorovEDist ↑(Ps n) ↑P = levyProkhorovEDist ↑(μs n) ↑ν

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
n : ℕ
⊢ 0 < dist (μs n) ν + εs n

Tactic:
linarith [εs_pos n, dist_nonneg (x := μs n) (y := ν)]

Result:
no goals

Proof state:
case h.refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto
    ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
rw [BoundedContinuousFunction.integral_eq_integral_meas_le]

Result:
case h.refine_4
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto
    ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2 + (dist (μs n) ν + εs n) * ‖f‖ ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P {a | t ≤ f a}).toReal) + δ

case h.refine_4.f_nn
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := (equiv (ProbabilityMeasure Ω)) ν
Ps : ℕ → ProbabilityMeasure Ω := fun n => (equiv (ProbabilityMeasure Ω)) (μs n)
f✝ f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left✝ : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto
    ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n)
    atTop (𝓝 (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  ((fun ε => ∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P (thickening ε {a | t ≤ f a}))).toReal) ∘ fun n => dist (μs n) ν + εs n) n <
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑(P {a | t ≤ f a})).toReal) + δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
bound :
  ∫ (ω : Ω), f ω ∂↑(Ps n) ≤
    (∫ (t : ℝ) in Ioc 0 ‖f‖, (↑P (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖
⊢ 0 ≤ᶠ[ae ↑P] ⇑f