awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop)
have same : ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
  liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
Tactic: have same := lintegral_le_liminf_lintegral_of_forall_isOpen_measure_le_liminf_measure
                  f.continuous f_nn h_opens
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop)
have rw : (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μ).toReal ≤
  liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop
Tactic: rw [@integral_eq_lintegral_of_nonneg_ae Ω _ μ f (Eventually.of_forall f_nn)
        f.continuous.measurable.aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μ).toReal ≤
    liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop
have h : liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop =
  ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
Tactic: convert! ENNReal.toReal_mono ?_ same
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
h :
  liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
⊢ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μ).toReal ≤
    liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop
have convert! : Ne (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
Tactic: convert! ENNReal.toReal_mono ?_ same
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μs i) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
have h : liminf (fun (i : ℕ) ↦ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μs i).toReal) atTop =
  ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
Tactic: simp only [fun i ↦ @integral_eq_lintegral_of_nonneg_ae Ω _ (μs i) f (Eventually.of_forall f_nn)
                        f.continuous.measurable.aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
g : Ω →ᵇ ℝ≥0 := comp Real.toNNReal Real.lipschitzWith_toNNReal f
⊢ liminf (fun (i : ℕ) ↦ (∫⁻ (a : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) a) ∂μs i).toReal) atTop =
    ENNReal.toReal (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop)
have bound : ∀ (i : ℕ), ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑(nndist 0 g) : ℝ≥0∞)
Tactic: have bound : ∀ i, ∫⁻ x, ENNReal.ofReal (f x) ∂(μs i) ≤ nndist 0 g := fun i ↦ by
      simpa only [coe_nnreal_ennreal_nndist, measure_univ, mul_one, ge_iff_le] using
            BoundedContinuousFunction.lintegral_le_edist_mul (μ := μs i) g
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ Ne (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
have h : LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
have obs : ∀ (i : ℕ),
  ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤
    HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: have obs := fun (i : ℕ) ↦ @BoundedContinuousFunction.lintegral_nnnorm_le Ω _ _ (μs i) ℝ _ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs :
  ∀ (i : ℕ),
    ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤
      HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μs i : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
have obs₁ : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
Tactic: simp only [measure_univ, mul_one] at obs
Cleared hypotheses: obs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop) ∞
have apply : liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop ≤ (↑‖f‖₊ : ℝ≥0∞)
Tactic: apply lt_of_le_of_lt _ (show (‖f‖₊ : ℝ≥0∞) < ∞ from ENNReal.coe_lt_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop ≤ (↑‖f‖₊ : ℝ≥0∞)
have hf : autoParam
  (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
    ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i)
  liminf_le_of_le._auto_1
Tactic: apply liminf_le_of_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
hf :
  autoParam
    (IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (i : ℕ) ↦
      ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i)
    liminf_le_of_le._auto_1
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop ≤ (↑‖f‖₊ : ℝ≥0∞)
have h : ∀ (b : ℝ≥0∞), (∀ᶠ (n : ℕ) in atTop, b ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n) → b ≤ (↑‖f‖₊ : ℝ≥0∞)
Tactic: apply liminf_le_of_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
⊢ x ≤ (↑‖f‖₊ : ℝ≥0∞)
have h : ∀ (i : ℕ) (hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i), x ≤ (↑‖f‖₊ : ℝ≥0∞)
Tactic: obtain ⟨i, hi⟩ := hx.exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
⊢ x ≤ (↑‖f‖₊ : ℝ≥0∞)
have h : ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
Tactic: apply le_trans hi
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
⊢ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
have h : ∀ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
Tactic: convert! obs i with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
⊢ ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
have aux : ENNReal.ofReal ((fun (f : Ω →ᵇ ℝ) ↦ f.toFun) f x) = (↑(NNReal.mk ((fun (f : Ω →ᵇ ℝ) ↦ f.toFun) f x) sorry) : ℝ≥0∞)
Tactic: have aux := ENNReal.ofReal_eq_coe_nnreal (f_nn x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
⊢ ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
have h : (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) sorry) : ℝ≥0∞) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
Tactic: rw [aux]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
μs : ℕ → Measure Ω
inst_3 : ∀ (i : ℕ), IsProbabilityMeasure (μs i)
f : Ω →ᵇ ℝ
f_nn : 0 ≤ f
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
same :
  ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μ ≤
    liminf (fun (i : ℕ) ↦ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i) atTop
obs : ∀ (i : ℕ), ∫⁻ (x : Ω), (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞) ∂μs i ≤ (↑‖f‖₊ : ℝ≥0∞)
x_1 : ℝ≥0∞
hx : ∀ᶠ (n : ℕ) in atTop, x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs n
i : ℕ
hi : x_1 ≤ ∫⁻ (x : Ω), ENNReal.ofReal ((f : (a : Ω) → ℝ) x) ∂μs i
x : Ω
aux : ENNReal.ofReal ((f : (a : Ω) → ℝ) x) = (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞)
⊢ (↑(NNReal.mk ((f : (a : Ω) → ℝ) x) ⋯) : ℝ≥0∞) = (↑(NNNorm.nnnorm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)) : ℝ≥0∞)
have h : (f : (a : Ω) → ℝ) x = norm (E := ℝ) ((f : (a : Ω) → ℝ) x : ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)
have refine : ∀ (f : Ω →ᵇ ℝ),
  Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) atTop
    (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))
Tactic: refine ProbabilityMeasure.tendsto_iff_forall_integral_tendsto.mpr ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
        (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
⊢ ∀ (f : Ω →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : ℕ) ↦ ∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑(μs i) : Measure Ω)) atTop
      (𝓝 (∫ (ω : Ω), (f : (a : Ω) → ℝ) ω ∂(↑μ : Measure Ω)))
have refine : ∀ (f : Ω →ᵇ ℝ) (f_nn : 0 ≤ f),
  LE.le (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑μ : Measure Ω))
    (liminf (fun (i : ℕ) ↦ ∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂(↑(μs i) : Measure Ω)) atTop)
Tactic: refine tendsto_integral_of_forall_integral_le_liminf_integral fun f f_nn ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
⊢ Tendsto (fun (i : ℕ) ↦ μs i) atTop (𝓝 μ)
have refine : ∀ (G : Set Ω) (G_open : IsOpen[inst_1] G),
  LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
Tactic: refine tendsto_of_forall_isOpen_le_liminf_nat' fun G G_open ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
h_opens :
  ∀ (G : Set Ω),
    IsOpen[inst_1] G →
      LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0)
        (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
G : Set Ω
G_open : IsOpen[inst_1] G
⊢ LE.le (α := ℝ≥0∞) (((↑μ : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞)
    (liminf (fun (i : ℕ) ↦ ((↑(μs i) : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G) atTop : ℝ≥0∞)
have h_opens₁ : LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
Tactic: specialize h_opens G G_open
Cleared hypotheses: h_opens
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
⊢ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
have refine_1 : ContinuousAt ENNReal.ofNNReal (liminf (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop)
Tactic: refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Portmanteau (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : ProbabilityMeasure Ω
μs : ℕ → ProbabilityMeasure Ω
G : Set Ω
G_open : IsOpen[inst_1] G
h_opens :
  LE.le (α := ℝ≥0) ((μ : (a : Set Ω) → ℝ≥0) G : ℝ≥0) (liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop : ℝ≥0)
refine_1 : ContinuousAt ENNReal.ofNNReal (liminf (fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G) atTop)
⊢ (↑(liminf (fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop) : ℝ≥0∞) =
    liminf (β := ℕ) (ENNReal.ofNNReal ∘ fun (i : ℕ) ↦ (μs i : (a : Set Ω) → ℝ≥0) G) atTop
have refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0) ↦ x1 ≥ x2) atTop fun (x : ℕ) ↦ (μs x : (a : Set Ω) → ℝ≥0) G
Tactic: refine Monotone.map_liminf_of_continuousAt (F := atTop) ENNReal.coe_mono (μs · G) ?_ ?_ ?_