-- Mathlib/MeasureTheory/Measure/LevyProkhorovMetric.lean
/-- A simple sufficient condition for bounding `levyProkhorovEDist` between probability measures
from above. The condition involves only one of two natural bounds, the other bound is for free. -/
lemma levyProkhorovEDist_le_of_forall_le
    (μ ν : Measure Ω) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] (δ : ℝ≥0∞)
    (h : ∀ ε B, δ < ε → ε < ∞ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε) :
    levyProkhorovEDist μ ν ≤ δ

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
apply (tsub_le_tsub_right almost _).trans

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))
⊢ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B)) -
      ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤
    μ (thickening ε.toReal B) + ε

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h : 1 - μ (thickening ε.toReal B) ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
almost : 1 ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B))
⊢ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + (ε + μ (thickening ε.toReal B)) -
      ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤
    μ (thickening ε.toReal B) + ε

Tactic:
rw [ENNReal.add_sub_cancel_left (measure_ne_top ν _), add_comm ε]

Result:
no goals

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
have Tc_mble := (isOpen_thickening (δ := ε.toReal) (E := B)).isClosed_compl.measurableSet

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
⊢ ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε

Tactic:
intro ε B ε_gt ε_lt_top B_mble

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
⊢ μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
⊢ levyProkhorovEDist μ ν ≤ δ

Tactic:
apply levyProkhorovEDist_le_of_forall μ ν δ

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
⊢ ∀ (ε : ℝ≥0∞) (B : Set Ω),
    δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε ∧ ν B ≤ μ (thickening ε.toReal B) + ε

Proof state:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ : ℝ≥0∞
h : ∀ (ε : ℝ≥0∞) (B : Set Ω), δ < ε → ε < ⊤ → MeasurableSet B → μ B ≤ ν (thickening ε.toReal B) + ε
ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε

Tactic:
specialize h ε (thickening ε.toReal B)ᶜ ε_gt ε_lt_top Tc_mble

Result:
Ω : Type u_1
inst✝⁴ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace Ω
inst✝² : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
δ ε : ℝ≥0∞
B : Set Ω
ε_gt : δ < ε
ε_lt_top : ε < ⊤
B_mble : MeasurableSet B
B_subset : B ⊆ (thickening ε.toReal (thickening ε.toReal B)ᶜ)ᶜ
Tc_mble : MeasurableSet (thickening ε.toReal B)ᶜ
h : μ (thickening ε.toReal B)ᶜ ≤ ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) + ε
⊢ 1 - ν (thickening ε.toReal (thickening ε.toReal B)ᶜ) ≤ μ (thickening ε.toReal B) + ε