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 : Ω) → ℝ)
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
⊢ 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‖

Tactic:
simp [(mul_comm _ ε).le]

Premises used: Eq.le, mul_comm
-- 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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})) (Measure.restrict volume (Ioc 0 ‖f‖))

Tactic:
intble₂

Premises used: MeasureTheory.IntegrableOn
-- 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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    (fun (x : ℝ) ↦ ν.real (thickening ε {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})) (Measure.restrict volume (Ioc 0 ‖f‖))

Tactic:
exact intble₂
-- 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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ε) (Measure.restrict volume (Ioc 0 ‖f‖))

Tactic:
integrable_const ε

Premises used: MeasureTheory.integrable_const
-- 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
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (x : ℝ) ↦ ε) (Measure.restrict volume (Ioc 0 ‖f‖))

Tactic:
exact integrable_const ε

Premises used: MeasureTheory.integrable_const
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume

Tactic:
intble₁
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ μ.real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})
    (Ioc 0 ‖f‖) volume

Tactic:
exact intble₁
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
intble₂.add <| integrable_const ε

Premises used: MeasureTheory.IntegrableOn.add, MeasureTheory.integrable_const
-- 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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (t : ℝ) ↦ ν.real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) + ε) (Ioc 0 ‖f‖) volume

Tactic:
exact intble₂.add <| integrable_const ε

Premises used: MeasureTheory.IntegrableOn.add, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
hF_meas :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)
h_bound :
  ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
bound_integrable : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace 1 (Measure.restrict volume A)
h_lim :
  ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ))
      (𝓝[>] 0) (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}) : ℝ))
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    (𝓝[>] 0)
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume A) fun (t : ℝ) ↦
        (↑μ : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))

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

Premises used: MeasureTheory.tendsto_integral_filter_of_dominated_convergence, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
apply :
  ∀ (n : ℝ),
    Measurable (β := ℝ) fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
      (fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ))
      (Measure.restrict volume A)

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

Premises used: Measurable.aestronglyMeasurable, Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n : ℝ
simp : Measurable (β := ℝ≥0) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})
⊢ Measurable (β := ℝ) fun (t : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)

Tactic:
simp only [measurable_coe_nnreal_real_iff]

Premises used: measurable_coe_nnreal_real_iff
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n : ℝ
apply :
  ∀ (s t : ℝ) (hst : s ≤ t),
    LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | s ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
⊢ Measurable (β := ℝ≥0) fun (x : ℝ) ↦ (μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | x ≤ (f : (a : Ω) → ℝ) a})

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

Premises used: Measurable.comp, ENNReal.measurable_toNNReal, Antitone.measurable
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n s t : ℝ
hst : s ≤ t
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | s ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)

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

Premises used: 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 Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
n s t : ℝ
hst : s ≤ t
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
    (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening n {a : Ω | s ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)

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

Premises used: 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 Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
apply :
  ∀ (i : ℝ),
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a
⊢ ∀ᶠ (n : ℝ) in 𝓝[>] 0,
    ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
      ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a

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

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i : ℝ
apply : ∀ (t : ℝ), ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)‖ ≤ 1 t
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ)‖ ≤ 1 a

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 Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i t : ℝ
simp : (↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ) ≤ 1
⊢ ‖(↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)‖ ≤ 1 t

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

Premises used: Pi.one_apply, NNReal.abs_eq, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i t : ℝ
⊢ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ) ≤ 1

Tactic:
ENNReal.toReal_mono one_ne_top prob_le_one

Premises used: MeasureTheory.prob_le_one, ENNReal.toReal, ENNReal.toReal_mono, NNReal.toReal, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
i t : ℝ
⊢ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening i {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ) ≤ 1

Tactic:
exact ENNReal.toReal_mono one_ne_top prob_le_one

Premises used: MeasureTheory.prob_le_one, ENNReal.toReal_mono, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ LT.lt (α := ℝ≥0∞) ((Measure.restrict volume A : (a : Set ℝ) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [lt_top_iff_ne_top, A_finmeas]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
⊢ IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume A)

Tactic:
have aux : IsFiniteMeasure (volume.restrict A) := ⟨by simp [lt_top_iff_ne_top, A_finmeas]⟩
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
aux : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume A)
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace 1 (Measure.restrict volume A)

Tactic:
apply integrable_const

Premises used: MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
apply :
  ∀ (t : ℝ),
    Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)) (𝓝[>] 0)
      (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ))
⊢ ∀ᵐ (a : ℝ) ∂Measure.restrict volume A,
    Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1})) : ℝ))
      (𝓝[>] 0) (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a_1 : Ω | a ≤ (f : (a : Ω) → ℝ) a_1}) : ℝ))

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 Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
simp :
  Tendsto (β := ℝ≥0) (fun (a : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0)
⊢ Tendsto (fun (n : ℝ) ↦ (↑((μ : (a : Set Ω) → ℝ≥0) (thickening n {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) : ℝ)) (𝓝[>] 0)
    (𝓝 (↑((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ))

Tactic:
simp only [NNReal.tendsto_coe]

Premises used: NNReal.tendsto_coe
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
apply :
  Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)
apply₁ : Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Tendsto (β := ℝ≥0) (fun (a : ℝ) ↦ ((μ : (a : Set Ω) → ℝ≥0) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0))
    (𝓝[>] 0) (𝓝 ((μ : (a : Set Ω) → ℝ≥0) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0)

Tactic:
apply (ENNReal.tendsto_toNNReal _).comp

Premises used: ENNReal.tendsto_toNNReal, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
apply :
  ∃ R > 0,
    Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening R {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)
apply₁ : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}
⊢ Tendsto (β := ℝ≥0∞)
    (fun (a : ℝ) ↦ (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening a {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞))
    (𝓝[>] 0) (𝓝 (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : Filter ℝ≥0∞)

Tactic:
apply tendsto_measure_thickening_of_isClosed ?_ ?_

Premises used: tendsto_measure_thickening_of_isClosed
-- Module: Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ
A : Set ℝ
A_finmeas : Ne (α := ℝ≥0∞) ((volume : (a : Set ℝ) → ℝ≥0∞) A : ℝ≥0∞) (∞ : ℝ≥0∞)
μ : ProbabilityMeasure Ω
t : ℝ
⊢ ∃ R > 0,
    Ne (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening R {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) : ℝ≥0∞)
      (∞ : ℝ≥0∞)

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

Premises used: MeasureTheory.measure_ne_top, Real.zero_lt_one, And.intro, Exists.intro, OfNat.ofNat