awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
⊢ (∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))) →
    Tendsto μs F (𝓝 μ)
have mpr : ∀
  (h :
    ∀ (f : Ω → ℝ),
      (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
        (∃ (L : ℝ≥0), LipschitzWith L f) →
          Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F
            (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω))))
  (s : Set Ω) (hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s),
  limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s
Tactic: refine fun h ↦ tendsto_of_forall_isClosed_limsup_real_le' fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s
have mpr : ∀ (ε : ℝ) (ε_pos : 0 < ε), limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
Tactic: refine le_of_forall_pos_le_add fun ε ε_pos ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
Tactic: have key₁ : Tendsto (fun n ↦ ∫ ω, fs n ω ∂μ) atTop (𝓝 ((μ : Measure Ω).real s)) :=
    tendsto_integral_thickenedIndicator_of_isClosed μ hs (δs := fun n ↦ (1 : ℝ) / (n + 1))
      (fun _ ↦ by positivity) tendsto_one_div_add_atTop_nhds_zero_nat
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
Tactic: have room₁ : (μ : Measure Ω).real s < (μ : Measure Ω).real s + ε / 2 := by simp [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have mpr : ∀ (M : ℕ) (hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2),
  limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
Tactic: obtain ⟨M, hM⟩ := eventually_atTop.mp <| key₁.eventually_lt_const room₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have mpr : ∀
  (key₂ :
    Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F
      (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))),
  limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
Tactic: have key₂ : Tendsto (fun i ↦ ∫ ω, fs M ω ∂(μs i)) F (𝓝 (∫ ω, fs M ω ∂μ)) :=
    h (fs M) ⟨1, fun x y ↦ ?_⟩
      ⟨_, lipschitzWith_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
mpr :
  ∀
    (key₂ :
      Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F
        (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))),
    limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have mpr₁ : ∀ (x y : Ω), dist (fs M x) (fs M y) ≤ 1
Tactic: have key₂ : Tendsto (fun i ↦ ∫ ω, fs M ω ∂(μs i)) F (𝓝 (∫ ω, fs M ω ∂μ)) :=
    h (fs M) ⟨1, fun x y ↦ ?_⟩
      ⟨_, lipschitzWith_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
x y : Ω
⊢ dist (fs M x) (fs M y) ≤ 1
have mpr : -1 ≤ fs M x - fs M y ∧ fs M x - fs M y ≤ 1
Tactic: simp only [Real.dist_eq, abs_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
x y : Ω
⊢ -1 ≤ fs M x - fs M y ∧ fs M x - fs M y ≤ 1
have h1 : ∀ (x : Ω), fs M x ≤ 1
Tactic: have h1 x : fs M x ≤ 1 := thickenedIndicator_le_one _ _ _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
x y : Ω
h1 : ∀ (x : Ω), fs M x ≤ 1
⊢ -1 ≤ fs M x - fs M y ∧ fs M x - fs M y ≤ 1
have h2 : ∀ (x : Ω), 0 ≤ fs M x
Tactic: have h2 x : 0 ≤ fs M x := by simp [fs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
Tactic: have room₂ : ∫ a, fs M a ∂μ < ∫ a, fs M a ∂μ + ε / 2 := by simp [ε_pos]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
have refine : ∀ (x : γ) (hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2),
  (↑(μs x) : Measure Ω).real s ≤ ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω)
Tactic: refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ (↑(μs x) : Measure Ω).real s ≤ ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω)
have rw : LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))
Tactic: rw [← integral_indicator_one hs.measurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))
have refine_1 : Integrable (ε := ℝ) (s.indicator 1) (↑(μs x) : Measure Ω)
Tactic: refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
refine_1 : Integrable (ε := ℝ) (s.indicator 1) (↑(μs x) : Measure Ω)
⊢ LE.le (α := ℝ) (∫ (x : Ω), s.indicator 1 x ∂(↑(μs x) : Measure Ω)) (∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω))
have refine_2 : s.indicator 1 ≤ fs M
Tactic: refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
x : γ
hx : ∫ (ω : Ω), fs M ω ∂(↑(μs x) : Measure Ω) ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ s.indicator 1 ≤ fs M
have h₁ : (fun (i : Ω) ↦ (↑(s.indicator (fun (x : Ω) ↦ 1) i) : ℝ)) ≤ fs M
Tactic: have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
γ : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
F : Filter γ
inst_2 : F.IsCountablyGenerated
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
hne : F.NeBot
h :
  ∀ (f : Ω → ℝ),
    (∃ (C : ℝ), ∀ (x y : Ω), dist (f x) (f y) ≤ C) →
      (∃ (L : ℝ≥0), LipschitzWith L f) →
        Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), f ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), f ω ∂(↑μ : Measure Ω)))
s : Set Ω
hs : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
ε : ℝ
ε_pos : 0 < ε
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ s : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
key₁ : Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂(↑μ : Measure Ω)) atTop (𝓝 ((↑μ : Measure Ω).real s))
room₁ : (↑μ : Measure Ω).real s < (↑μ : Measure Ω).real s + ε / 2
M : ℕ
hM : ∀ b ≥ M, ∫ (ω : Ω), fs b ω ∂(↑μ : Measure Ω) < (↑μ : Measure Ω).real s + ε / 2
key₂ :
  Tendsto (β := ℝ) (fun (i : γ) ↦ ∫ (ω : Ω), fs M ω ∂(↑(μs i) : Measure Ω)) F (𝓝 (∫ (ω : Ω), fs M ω ∂(↑μ : Measure Ω)))
room₂ : ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) < ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
⊢ limsup (fun (i : γ) ↦ (↑(μs i) : Measure Ω).real s) F ≤ (↑μ : Measure Ω).real s + ε
have ev_near : ∀ᶠ (x : γ) in F, (↑(μs x) : Measure Ω).real s ≤ ∫ (a : Ω), fs M a ∂(↑μ : Measure Ω) + ε / 2
Tactic: have ev_near : ∀ᶠ x in F, (μs x : Measure Ω).real s ≤ ∫ a, fs M a ∂μ + ε / 2 := by
    refine (key₂.eventually_le_const room₂).mono fun x hx ↦ le_trans ?_ hx
    rw [← integral_indicator_one hs.measurableSet]
    refine integral_mono ?_ (integrable_thickenedIndicator _ _) ?_
    · exact (integrable_indicator_iff hs.measurableSet).mpr (integrable_const _).integrableOn
    · have h : _ ≤ fs M :=
        indicator_le_thickenedIndicator (δ := (1 : ℝ) / (M + 1)) (by positivity) s
      simpa using h