awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
x : E
⊢ g x ≤ (K n)ᶜ.indicator 1 x
have pos : ∀ (hx : x ∈ (K n)ᶜ), g x ≤ (K n)ᶜ.indicator 1 x
Tactic: by_cases hx : x ∈ (K n)ᶜ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
x : E
pos : ∀ (hx : x ∈ (K n)ᶜ), g x ≤ (K n)ᶜ.indicator 1 x
⊢ g x ≤ (K n)ᶜ.indicator 1 x
have neg : ∀ (hx : x ∉ (K n)ᶜ), g x ≤ (K n)ᶜ.indicator 1 x
Tactic: by_cases hx : x ∈ (K n)ᶜ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
x : E
hx : x ∉ (K n)ᶜ
⊢ g x ≤ (K n)ᶜ.indicator 1 x
have neg : g x ≤ 0
Tactic: simp only [hx, not_false_eq_true, indicator_of_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
x : E
hx : x ∉ (K n)ᶜ
⊢ g x ≤ 0
have neg : g x = 0
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
x : E
hx : x ∉ (K n)ᶜ
⊢ g x = 0
have neg : x ∈ K n
Tactic: apply gK
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
⊢ ∫ (x : E), g x ∂(↑ρ : Measure E) ≤ (↑(u n) : ℝ)
have calc : LE.le (α := ℝ) (∫ (x : E), g x ∂(↑ρ : Measure E)) (∫ (x : E), (K n)ᶜ.indicator 1 x ∂(↑ρ : Measure E))
Tactic: calc ∫ x, g x ∂ρ
    _ ≤ ∫ x, indicator (K n)ᶜ 1 x ∂ρ := by
      apply integral_mono_of_nonneg
      · filter_upwards [] with x using g_nonneg x
      · apply Integrable.indicator (integrable_const _) (hK n).measurableSet.compl
      · filter_upwards [] with x
        by_cases hx : x ∈ (K n)ᶜ
        · simpa [hx] using g_le x
        · simp only [hx, not_false_eq_true, indicator_of_notMem]
          apply le_of_eq
          apply gK
          simpa using hx
    _ = ρ (K n)ᶜ := by simp [integral_indicator (hK n).measurableSet.compl]
    _ ≤ u n := mod_cast hρ.2 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : NormalSpace E
this_1 : (↑μ : Measure E).InnerRegular
g : E → ℝ
g_cont : Continuous[inst_1, _] g
gK : EqOn g 0 (K n)
g_nonneg : 0 ≤ g
g_le : g ≤ 1
this :
  Tendsto (β := ℝ) (fun (ρ : FiniteMeasure E) ↦ ∫ (x : E), g x ∂(↑ρ : Measure E)) (↑f : Filter (FiniteMeasure E))
    (𝓝 (∫ (x : E), g x ∂(↑μ : Measure E)))
ρ : FiniteMeasure E
hρ : ρ.mass ≤ C ∧ ∀ (n : ℕ), (ρ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
calc : LE.le (α := ℝ) (∫ (x : E), g x ∂(↑ρ : Measure E)) (∫ (x : E), (K n)ᶜ.indicator 1 x ∂(↑ρ : Measure E))
⊢ ∫ (x : E), g x ∂(↑ρ : Measure E) ≤ (↑(u n) : ℝ)
have calc₁ : ∫ (x : E), (K n)ᶜ.indicator 1 x ∂(↑ρ : Measure E) = (↑((ρ : (a : Set E) → ℝ≥0) (K n)ᶜ) : ℝ)
Tactic: calc ∫ x, g x ∂ρ
    _ ≤ ∫ x, indicator (K n)ᶜ 1 x ∂ρ := by
      apply integral_mono_of_nonneg
      · filter_upwards [] with x using g_nonneg x
      · apply Integrable.indicator (integrable_const _) (hK n).measurableSet.compl
      · filter_upwards [] with x
        by_cases hx : x ∈ (K n)ᶜ
        · simpa [hx] using g_le x
        · simp only [hx, not_false_eq_true, indicator_of_notMem]
          apply le_of_eq
          apply gK
          simpa using hx
    _ = ρ (K n)ᶜ := by simp [integral_indicator (hK n).measurableSet.compl]
    _ ≤ u n := mod_cast hρ.2 n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
have apply : (↑((μ : (a : Set E) → ℝ≥0) (K n)ᶜ) : ℝ≥0∞) ≤ (↑(u n) : ℝ≥0∞)
Tactic: apply ENNReal.coe_le_coe.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
⊢ (↑((μ : (a : Set E) → ℝ≥0) (K n)ᶜ) : ℝ≥0∞) ≤ (↑(u n) : ℝ≥0∞)
have h₁ : (↑((μ : (a : Set E) → ℝ≥0) (K n)ᶜ) : ℝ≥0∞) = ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ
Tactic: convert! this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n
have refine_2 : ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
Tactic: suffices (μ : Measure E) (K n)ᶜ ≤ u n by
      apply ENNReal.coe_le_coe.1
      convert! this
      simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ ((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
have refine_2 : ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
Tactic: simp only [toMeasure_mk, (hK n).measurableSet.compl, Measure.sum_apply, μ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (hypothesis)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
⊢ ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
have this : Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ) atTop
  (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
Tactic: have : Tendsto (fun m ↦ ∑ i ∈ Finset.range (m + 1), (ν i : Measure E) (K n)ᶜ) atTop
        (𝓝 (∑' i, (ν i : Measure E) (K n)ᶜ)) :=
      (ENNReal.tendsto_nat_tsum _).comp (tendsto_add_atTop_nat 1)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
u : ℕ → ℝ≥0
K : ℕ → Set E
C : ℝ≥0
hu : Tendsto u atTop (𝓝 0)
hK : ∀ (n : ℕ), IsCompact (K n)
I :
  ∀ (μ : FiniteMeasure E) (n : ℕ),
    ∑ i ∈ Finset.range (n + 1), μ.restrict (disjointed K i) = μ.restrict ((partialSups K : (a : ℕ) → Set E) n)
A : ∀ (n : ℕ), IsCompact.{u_1} (X := E) ((partialSups K : (a : ℕ) → Set E) n)
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C ∧ ∀ (n : ℕ), (μ : (a : Set E) → ℝ≥0) (K n)ᶜ ≤ u n} ∈ f
ν : (n : ℕ) → FiniteMeasure E
ν_reg : ∀ (n : ℕ), (↑(ν n) : Measure E).InnerRegular
νK : ∀ (n : ℕ), Eq (α := ℝ≥0) ((ν n : (a : Set E) → ℝ≥0) ((partialSups K : (a : ℕ) → Set E) n)ᶜ : ℝ≥0) (0 : ℝ≥0)
hν :
  ∀ (n : ℕ), Tendsto (fun (ρ : FiniteMeasure E) ↦ ρ.restrict (disjointed K n)) (↑f : Filter (FiniteMeasure E)) (𝓝 (ν n))
B : ((Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E) : Measure E) : (a : Set E) → ℝ≥0∞) univ ≤ (↑C : ℝ≥0∞)
μ : FiniteMeasure E :=
  Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) (Measure.sum fun (n : ℕ) ↦ (↑(ν n) : Measure E)) ⋯
L : Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μ)
n : ℕ
h : Monotone K
this :
  Tendsto (β := ℝ≥0∞) (fun (m : ℕ) ↦ ∑ i ∈ Finset.range (m + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ)
    atTop (𝓝 (∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ))
⊢ ∑' (i : ℕ), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
have refine_2 : ∀ᶠ (c : ℕ) in atTop, ∑ i ∈ Finset.range (c + 1), ((↑(ν i) : Measure E) : (a : Set E) → ℝ≥0∞) (K n)ᶜ ≤ (↑(u n) : ℝ≥0∞)
Tactic: apply le_of_tendsto this