-- Mathlib/MeasureTheory/Measure/Portmanteau.lean
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F). -/
lemma limsup_measure_closed_le_of_forall_tendsto_measure
    {Ω ι : Type*} {L : Filter ι} [MeasurableSpace Ω] [PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
    {μ : Measure Ω} [IsFiniteMeasure μ] {μs : ι → Measure Ω}
    (h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 →
            Tendsto (fun i ↦ μs i E) L (𝓝 (μ E)))
    (F : Set Ω) (F_closed : IsClosed F) :
    L.limsup (fun i ↦ μs i F) ≤ μ F

Proof state:
case inr.h
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
rs_lim : ∃ a, ∀ (b : ℕ), a ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Tactic:
obtain ⟨m, hm⟩ := rs_lim

Result:
case inr.h.intro
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Proof state:
case inr.h.intro
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Tactic:
have aux : (fun i ↦ (μs i F)) ≤ᶠ[L] (fun i ↦ μs i (Metric.thickening (rs m) F)) :=
  .of_forall <| fun i ↦ measure_mono (Metric.self_subset_thickening (rs_pos m) F)

Result:
case inr.h.intro
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
nhd : Iio (μ F + ↑ε) ∈ 𝓝 (μ F)
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → μ (Metric.cthickening (rs b) F) < μ F + ↑ε
aux : (fun i => (μs i) F) ≤ᶠ[L] fun i => (μs i) (Metric.thickening (rs m) F)
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Proof state:
case inr.h
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_lim : Tendsto rs atTop (𝓝 0)
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Tactic:
have keyB := tendsto_measure_cthickening_of_isClosed (μ := μ) (s := F)
              ⟨1, ⟨by simp only [gt_iff_lt, zero_lt_one], measure_ne_top _ _⟩⟩ F_closed

Result:
case inr.h
Ω : Type u_2
ι : Type u_3
L : Filter ι
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) L (𝓝 (μ E))
F : Set Ω
F_closed : IsClosed F
h✝ : L.NeBot
ex : ∃ rs, Tendsto rs atTop (𝓝 0) ∧ ∀ (n : ℕ), 0 < rs n ∧ μ (frontier (Metric.thickening (rs n) F)) = 0
rs : ℕ → ℝ := Classical.choose ex
rs_lim : Tendsto rs atTop (𝓝 0)
rs_pos : ∀ (n : ℕ), 0 < rs n
rs_null : ∀ (n : ℕ), μ (frontier (Metric.thickening (rs n) F)) = 0
Fthicks_open : ∀ (n : ℕ), IsOpen (Metric.thickening (rs n) F)
key : ∀ (n : ℕ), Tendsto (fun i => (μs i) (Metric.thickening (rs n) F)) L (𝓝 (μ (Metric.thickening (rs n) F)))
ε : ℝ≥0
ε_pos : 0 < ε
μF_finite : μ F < ⊤
keyB : Tendsto (fun r => μ (Metric.cthickening r F)) (𝓝 0) (𝓝 (μ F))
⊢ limsup (fun i => (μs i) F) L ≤ μ F + ↑ε

Proof state:
case inl
Ω : Type u_2
ι : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
μs : ι → Measure Ω
F : Set Ω
F_closed : IsClosed F
h : ∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Tendsto (fun i => (μs i) E) ⊥ (𝓝 (μ E))
⊢ limsup (fun i => (μs i) F) ⊥ ≤ μ F

Tactic:
simp only [limsup_bot, bot_eq_zero', zero_le]

Result:
no goals