awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
z : ℝ
⊢ z < z + δ / 2
have linarith : z + δ / 2 ≤ z → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
z : ℝ
linarith : z + δ / 2 ≤ z → 2 / 2 = 1
⊢ z < z + δ / 2
have linarith₁ : z + δ / 2 ≤ z → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
z : ℝ
linarith : z + δ / 2 ≤ z → 2 / 2 = 1
linarith₁ : z + δ / 2 ≤ z → HMul.hMul (α := ℝ) 1 2 = 2
⊢ z < z + δ / 2
have linarith₂ : z + δ / 2 ≤ z → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
z : ℝ
linarith : z + δ / 2 ≤ z → 2 / 2 = 1
linarith₁ : z + δ / 2 ≤ z → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : z + δ / 2 ≤ z → GT.gt (α := ℝ) 2 0
⊢ z < z + δ / 2
have linarith₃ : z + δ / 2 ≤ z → 0 - δ + (2 * z + 1 * δ - 2 * z) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
Tactic: have aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z := fun z ↦ Iio_mem_nhds (by linarith)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h : ∀ (n : ℕ)
  (hn :
    Membership.mem (γ := Set ℕ)
      (((fun (ε : ℝ) ↦
            @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
              (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
          fun (n : ℕ) ↦ dist (μs n) ν + εs n) ⁻¹'
        Iio
          ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
              (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
            δ / 2))
      n)
  (hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) n),
  ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
Tactic: filter_upwards [key (aux _), ε_of_room <| Iio_mem_nhds <| half_pos <|
                      mul_pos (inv_pos.mpr norm_f_pos) δ_pos]
      with n hn hn'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    (((fun (ε : ℝ) ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
        fun (n : ℕ) ↦ dist (μs n) ν + εs n) ⁻¹'
      Iio
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
          δ / 2))
    n
hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) n
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have hn₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
    (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
    δ / 2
Tactic: simp only [mem_preimage, Function.comp_def, mem_Iio] at *
Cleared hypotheses: hn, hn'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (α := ℕ) (β := ℝ)
    ((fun (ε : ℝ) ↦
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
      fun (n : ℕ) ↦ dist (μs n) ν + εs n)
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  Membership.mem (γ := Set ℕ)
    (((fun (ε : ℝ) ↦
          @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real (thickening ε {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) ∘
        fun (n : ℕ) ↦ dist (μs n) ν + εs n) ⁻¹'
      Iio
        ((@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
          δ / 2))
    n
hn' : Membership.mem (γ := Set ℕ) ((fun (x : ℕ) ↦ dist (μs x) ν + εs x) ⁻¹' Iio (‖f‖⁻¹ * δ / 2)) n
hn₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have hn'₁ : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
Tactic: simp only [mem_preimage, Function.comp_def, mem_Iio] at *
Cleared hypotheses: hn, hn'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_pos : ∀ (n : ℕ), 0 < εs n
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have εs_pos₁ : 0 < εs n
Tactic: specialize εs_pos n
Cleared hypotheses: εs_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h : ∀
  (bound :
    ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
          (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
        (dist (μs n) ν + εs n) * ‖f‖),
  ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
Tactic: have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                    (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
h :
  ∀
    (bound :
      ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
          (dist (μs n) ν + εs n) * ‖f‖),
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h₁ : 0 < dist (μs n) ν + εs n
Tactic: have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                    (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : PseudoMetricSpace Ω
inst_2 : OpensMeasurableSpace Ω
μs : ℕ → LevyProkhorov (ProbabilityMeasure Ω)
ν : LevyProkhorov (ProbabilityMeasure Ω)
hμs : Tendsto μs atTop (𝓝 ν)
P : ProbabilityMeasure Ω := ν.toMeasure
Ps : ℕ → ProbabilityMeasure Ω := toMeasure ∘ μs
f_1 f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
f_zero : ¬‖f‖ = 0
norm_f_pos : 0 < ‖f‖
δ : ℝ
δ_pos : 0 < δ
εs : ℕ → ℝ
left : StrictAnti εs
εs_lim : Tendsto εs atTop (𝓝 0)
ε_of_room : Tendsto (β := ℝ) (fun (x : ℕ) ↦ dist (μs x) ν + εs x) atTop (𝓝 0)
ε_of_room' : Tendsto (β := ℝ) (fun (n : ℕ) ↦ dist (μs n) ν + εs n) atTop (𝓝[>] 0)
key :
  Tendsto (β := ℝ)
    (fun (x : ℕ) ↦
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real (thickening (dist (μs x) ν + εs x) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
    atTop
    (𝓝
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}))
aux : ∀ (z : ℝ), Iio (z + δ / 2) ∈ 𝓝 z
n : ℕ
hn :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
      (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) <
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
        (↑P : Measure Ω).real {a : Ω | t ≤ (f : (a : Ω) → ℝ) a}) +
      δ / 2
hn' : dist (μs n) ν + εs n < ‖f‖⁻¹ * δ / 2
εs_pos : 0 < εs n
h :
  ∀
    (bound :
      ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(Ps n) : Measure Ω) ≤
        (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 ‖f‖)) fun (t : ℝ) ↦
            (↑P : Measure Ω).real (thickening (dist (μs n) ν + εs n) {a : Ω | t ≤ (f : (a : Ω) → ℝ) a})) +
          (dist (μs n) ν + εs n) * ‖f‖),
    ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
h₁ : 0 < dist (μs n) ν + εs n
⊢ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(Ps n) : Measure Ω) ≤ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑P : Measure Ω) + δ
have h₂ : levyProkhorovEDist (↑(Ps n) : Measure Ω) (↑P : Measure Ω) < ENNReal.ofReal (dist (μs n) ν + εs n)
Tactic: have bound := BoundedContinuousFunction.integral_le_of_levyProkhorovEDist_lt
                    (Ps n) P (ε := dist (μs n) ν + εs n) ?_ ?_ f ?_