-- 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 h
Ω : 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))
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
⊢ ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

Tactic:
specialize εs_pos n

Result:
case h
Ω : 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
⊢ ∫ (x : Ω), f x ∂↑((⇑(equiv (ProbabilityMeasure Ω)) ∘ μs) n) ≤ ∫ (x : Ω), f x ∂↑P + δ

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
⊢ 0 ≤ εs n

Tactic:
positivity

Result:
no goals

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))
⊢ Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝[>] 0)

Tactic:
rw [tendsto_nhdsWithin_iff]

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_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (fun x => dist (μs x) ν + εs x) atTop (𝓝 (0 + 0))
⊢ Tendsto (fun n => dist (μs n) ν + εs n) atTop (𝓝 0) ∧ ∀ᶠ (n : ℕ) in atTop, dist (μs n) ν + εs n ∈ Ioi 0

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)
ε_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))
z : ℝ
⊢ z < z + δ / 2

Tactic:
linarith

Result:
no goals

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 only [norm_eq_zero] at f_zero

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