-- 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:
case bound_integrable
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
⊢ Integrable 1 (volume.restrict A)

Tactic:
have aux : IsFiniteMeasure (volume.restrict A) := ⟨by simp [lt_top_iff_ne_top, A_finmeas]⟩

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

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

Tactic:
exact measure_ne_top _ _

Result:
no goals

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

Tactic:
apply Eventually.of_forall fun n ↦ Measurable.aestronglyMeasurable ?_

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

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

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 Ω
i t : ℝ
⊢ ‖↑(μ (thickening i {a | t ≤ f a}))‖ ≤ 1 t

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 t

Tactic:
simp only [Real.norm_eq_abs, NNReal.abs_eq, Pi.one_apply]

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

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

Tactic:
apply tendsto_integral_filter_of_dominated_convergence (G := ℝ) (μ := volume.restrict A)
      (F := fun ε t ↦ (μ (thickening ε {a | t ≤ f a}))) (f := fun t ↦ (μ {a | t ≤ f a})) 1

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

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

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

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}))

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

Tactic:
exact isClosed_le continuous_const f.continuous

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
⊢ (volume.restrict A) univ < ⊤

Tactic:
simp [lt_top_iff_ne_top, A_finmeas]

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 t => ↑(μ (thickening n {a | t ≤ f a}))

Tactic:
simp only [measurable_coe_nnreal_real_iff]

Result:
Ω : 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})

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 (ENNReal.tendsto_toNNReal _).comp

Result:
Ω : 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}))

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

Proof state:
Ω : 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}))

Tactic:
simp only [NNReal.tendsto_coe]

Result:
Ω : 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}))

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

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

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : PseudoMetricSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : volume A ≠ ⊤
μ : ProbabilityMeasure Ω
i : ℝ
⊢ ∀ᵐ (a : ℝ) ∂volume.restrict A, ‖↑(μ (thickening i {a_1 | a ≤ f a_1}))‖ ≤ 1 a