-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- A monotone decreasing convergence lemma for integrals of measures of thickenings:
`∫ t in (0, ‖f‖], μ (thickening ε {x | f(x) ≥ t}) dt` tends to
`∫ t in (0, ‖f‖], μ {x | f(x) ≥ t} dt` as `ε → 0`. -/
lemma tendsto_integral_meas_thickening_le (f : Ω →ᵇ ℝ)
    {A : Set ℝ} (A_finmeas : volume A ≠ ∞) (μ : ProbabilityMeasure Ω) :
    Tendsto (fun ε ↦ ∫ t in A, ENNReal.toReal (μ (thickening ε {a | t ≤ f a}))) (𝓝[>] (0 : ℝ))
      (𝓝 (∫ t in A, ENNReal.toReal (μ {a | t ≤ f a})))

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ∃ R > 0, ↑μ (thickening R {a | t ≤ f a}) ≠ ⊤

Tactic:
exact ⟨1, ⟨Real.zero_lt_one, measure_ne_top _ _⟩⟩

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
i t : ℝ
⊢ ↑(μ (thickening i {a | t ≤ f a})) ≤ 1

Tactic:
exact ENNReal.toReal_mono one_ne_top prob_le_one

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
n : ℝ
⊢ Measurable fun x => μ (thickening n {a | x ≤ f a})

Tactic:
apply measurable_toNNReal.comp <| Antitone.measurable (fun s t hst ↦ ?_)

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
n s t : ℝ
hst : s ≤ t
⊢ ↑μ (thickening n {a | t ≤ f a}) ≤ ↑μ (thickening n {a | s ≤ f a})

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
n s t : ℝ
hst : s ≤ t
⊢ ↑μ (thickening n {a | t ≤ f a}) ≤ ↑μ (thickening n {a | s ≤ f a})

Tactic:
exact measure_mono <| thickening_subset_of_subset _ <| fun ω h ↦ hst.trans h

Result:
no goals

Proof state:
case bound_integrable
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
aux : IsFiniteMeasure (volume.restrict A)
⊢ Integrable 1 (volume.restrict A)

Tactic:
apply integrable_const

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun a => ↑μ (thickening a {a | t ≤ f a})) (𝓝[>] 0) (𝓝 (↑μ {a | t ≤ f a}))

Tactic:
apply tendsto_measure_thickening_of_isClosed ?_ ?_

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ∃ R > 0, ↑μ (thickening R {a | t ≤ f a}) ≠ ⊤

Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
t : ℝ
⊢ IsClosed {a | t ≤ f a}

Proof state:
case h_lim
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict A,
    Tendsto (fun n => ↑(μ (thickening n {a_1 | a ≤ f a_1}))) (𝓝[>] 0) (𝓝 ↑(μ {a_1 | a ≤ f a_1}))

Tactic:
apply Eventually.of_forall (fun t ↦ ?_)

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
t : ℝ
⊢ Tendsto (fun n => ↑(μ (thickening n {a | t ≤ f a}))) (𝓝[>] 0) (𝓝 ↑(μ {a | t ≤ f a}))