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

Proof state:
case pos
Ω : 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
⊢ limsup (fun i => ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) i)) atTop ≤ ∫ (x : Ω), f x ∂↑P

Tactic:
simp [f_zero, limsup_const]

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 (thickening (dist (μs n) ν + εs n) {a | t ≤ f a})).toReal) +
      (dist (μs n) ν + εs n) * ‖f‖ ≤
    ∫ (x : Ω), f x ∂↑P + δ

Tactic:
apply (add_le_add_right hn.le _).trans

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‖ ≤ ∫ (x : Ω), f x ∂↑P + δ

Proof state:
case neg.h.intro.intro.intro
Ω : 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)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
have key := (tendsto_integral_meas_thickening_le f (A := Ioc 0 ‖f‖) (by simp) P).comp ε_of_room'

Result:
case neg.h.intro.intro.intro
Ω : 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)
ε_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))
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Proof state:
case neg.h.intro.intro.intro
Ω : 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))
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
rw [add_zero] at ε_of_room

Result:
case neg.h.intro.intro.intro
Ω : 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)
ε_of_room' : Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)
⊢ ∀ᶠ (n : ℕ) in atTop, ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ