awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
t : ℝ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      ((ν : (a : Set Ω) → ℝ≥0∞) (thickening (ENNReal.ofReal ε).toReal {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (ENNReal.ofReal ε) ≠
    ∞

Tactic:
exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩

Premises used: Iff.mpr, MeasureTheory.measure_ne_top, And.intro, ENNReal.ofReal_ne_top, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
⊢ LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε

Tactic:
have key : (fun (t : ℝ) ↦ μ.real {a | t ≤ f a})
              ≤ (fun (t : ℝ) ↦ ν.real (thickening ε {a | t ≤ f a}) + ε) := by
    intro t
    simp only [measureReal_def]
    convert!
      ENNReal.toReal_mono ?_ <|
        left_measure_le_of_levyProkhorovEDist_lt hμν (B := {a | t ≤ f a})
          (f.continuous.measurable measurableSet_Ici)
    · rw [ENNReal.toReal_add (measure_ne_top ν _) ofReal_ne_top, ENNReal.toReal_ofReal ε_pos.le]
    · exact ENNReal.add_ne_top.mpr ⟨measure_ne_top ν _, ofReal_ne_top⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
f_mble :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) volume
f_bdd : ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖), ‖μ.real {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}‖ ≤ μ.real univ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume

Tactic:
apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne

Premises used: MeasureTheory.Measure.integrableOn_of_bounded, measure_Ioc_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
apply : Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) volume

Tactic:
apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, Antitone.measurable, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}

Tactic:
fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)

Premises used: Antitone, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0∞) {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}

Tactic:
exact fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
apply : ∀ (t : ℝ), ‖μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}‖ ≤ μ.real univ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖), ‖μ.real {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}‖ ≤ μ.real univ

Tactic:
apply Eventually.of_forall <| fun t ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
t : ℝ
simp : μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} ≤ μ.real univ
⊢ ‖μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}‖ ≤ μ.real univ

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Premises used: MeasureTheory.measureReal_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
t : ℝ
⊢ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} ≤ μ.real univ

Tactic:
measureReal_mono (subset_univ _)

Premises used: MeasureTheory.measureReal_mono, Set.subset_univ
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
t : ℝ
⊢ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} ≤ μ.real univ

Tactic:
exact measureReal_mono (subset_univ _)

Premises used: MeasureTheory.measureReal_mono, Set.subset_univ
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume

Tactic:
have intble₁ : IntegrableOn (fun t ↦ μ.real {a | t ≤ f a}) (Ioc 0 ‖f‖) := by
    apply Measure.integrableOn_of_bounded (M := μ.real univ) measure_Ioc_lt_top.ne
    · apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ hst ↦ measure_mono (fun _ h ↦ hst.trans h)
    · apply Eventually.of_forall <| fun t ↦ ?_
      simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
      exact measureReal_mono (subset_univ _)
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
f_mble :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) volume
f_bdd :
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖),
    ‖ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})‖ ≤ ν.real univ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume

Tactic:
apply Measure.integrableOn_of_bounded (M := ν.real univ) measure_Ioc_lt_top.ne

Premises used: MeasureTheory.Measure.integrableOn_of_bounded, measure_Ioc_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
apply : Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) volume

Tactic:
apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, Antitone.measurable, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})

Tactic:
fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)

Premises used: Antitone, MeasureTheory.measure_mono, LE.le.trans, Metric.thickening_subset_of_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ Antitone (β := ℝ≥0∞) fun (x : ℝ) ↦ (ν : (a : Set Ω) → ℝ≥0∞) (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})

Tactic:
exact fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)

Premises used: MeasureTheory.measure_mono, Metric.thickening_subset_of_subset
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
apply : ∀ (t : ℝ), ‖ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})‖ ≤ ν.real univ
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume (Ioc 0 ‖f‖),
    ‖ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})‖ ≤ ν.real univ

Tactic:
apply Eventually.of_forall <| fun t ↦ ?_

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
t : ℝ
simp : ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤ ν.real univ
⊢ ‖ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})‖ ≤ ν.real univ

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]

Premises used: MeasureTheory.measureReal_nonneg, abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
t : ℝ
⊢ Ne (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
t : ℝ
⊢ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤ ν.real univ

Tactic:
exact ENNReal.toReal_mono (by finiteness) <| measure_mono (subset_univ _)

Premises used: Set.subset_univ, MeasureTheory.measure_mono, ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume

Tactic:
have intble₂ : IntegrableOn (fun t ↦ ν.real (thickening ε {a | t ≤ f a})) (Ioc 0 ‖f‖) := by
    apply Measure.integrableOn_of_bounded (M := ν.real univ) measure_Ioc_lt_top.ne
    · apply (Measurable.ennreal_toReal (Antitone.measurable ?_)).aestronglyMeasurable
      exact fun _ _ hst ↦ measure_mono <| thickening_subset_of_subset ε (fun _ h ↦ hst.trans h)
    · apply Eventually.of_forall <| fun t ↦ ?_
      simp only [Real.norm_eq_abs, abs_of_nonneg measureReal_nonneg]
      exact ENNReal.toReal_mono (by finiteness) <| measure_mono (subset_univ _)
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
apply :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
apply₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
apply₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε) (Ioc 0 ‖f‖) volume
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖

Tactic:
apply le_trans (setIntegral_mono (s := Ioc 0 ‖f‖) ?_ ?_ key)

Premises used: MeasureTheory.setIntegral_mono, le_trans
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_3 : IsFiniteMeasure μ
inst_4 : IsFiniteMeasure ν
ε : ℝ
ε_pos : 0 < ε
hμν : levyProkhorovEDist μ ν < ENNReal.ofReal ε
f : Ω →ᵇ ℝ
f_nn : (ae μ).EventuallyLE (β := ℝ) 0 (⇑f : (a : Ω) → ℝ)
key :
  LE.le (α := (t : ℝ) → ℝ) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) fun (t : ℝ) ↦
    ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε
intble₁ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume
intble₂ :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) (Ioc 0 ‖f‖) volume
rw :
  HAdd.hAdd (α := ℝ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦
        ν.real (thickening ε {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}))
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (a : ℝ) ↦ ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖
hf :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})) (Measure.restrict volume (Ioc 0 ‖f‖))
hg : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ε) (Measure.restrict volume (Ioc 0 ‖f‖))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (x : ℝ) ↦
      ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a}) + ε) ≤
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
      ε * ‖f‖

Tactic:
rw [integral_add]

Premises used: MeasureTheory.integral_add