awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μs i) L)
    (∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μ)
⊢ limsup (fun (i : ι) ↦ (μs i).real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤
    μ.real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ

Tactic:
simp_rw [f.integral_const_sub ‖f‖] at key

Premises used: Norm.norm, BoundedContinuousFunction.integral_const_sub
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  limsup (fun (i : ι) ↦ (μs i).real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤
    μ.real Set.univ • ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ
⊢ limsup (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ

Tactic:
simp only [probReal_univ, smul_eq_mul, one_mul] at key

Premises used: MeasureTheory.probReal_univ, smul_eq_mul, one_mul
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ
⊢ limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L

Tactic:
have := limsup_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ
this :
  limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
    ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L
rwa :
  ∀
    (key :
      ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L ≤ ‖f‖ - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
    (this :
      limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
        ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (key :
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
        (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L))
    (this :
      limsup (fun (i : ι) ↦ ‖f‖ - (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i) L =
        ‖f‖ - liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L),
    LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)

Tactic:
rwa [this, _root_.sub_le_sub_iff_left ‖f‖] at key

Premises used: Norm.norm, sub_le_sub_iff_left
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
    (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)

Tactic:
have key := h _ (f.add_norm_nonneg)
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
    (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
⊢ limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L ≤
    ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖

Tactic:
simp_rw [f.integral_add_const ‖f‖] at key

Premises used: Norm.norm, BoundedContinuousFunction.integral_add_const
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L ≤
    ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖
⊢ limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖

Tactic:
simp only [probReal_univ, smul_eq_mul, one_mul] at key

Premises used: MeasureTheory.probReal_univ, smul_eq_mul, one_mul
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
⊢ limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖

Tactic:
have := limsup_add_const L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above bdd_below.isCobounded_le
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key : limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖
this :
  limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
    limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖
rwa :
  ∀
    (key :
      limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖ ≤ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖)
    (this :
      limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
        limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (key :
      LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
        (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
    (this :
      limsup (fun (i : ι) ↦ (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → ℝ) x ∂μs i : ℝ)) i + ‖f‖) L =
        limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L + ‖f‖),
    LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)

Tactic:
rwa [this, add_le_add_iff_right] at key

Premises used: add_le_add_iff_right
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
inl :
  ∀
    (h :
      ∀ (f : X →ᵇ ℝ),
        0 ≤ f →
          LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
            (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥)),
    Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥ (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
inr :
  ∀ (hL : L.NeBot),
    Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))

Tactic:
rcases eq_or_neBot L with rfl | hL

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ ℝ
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥ (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))

Tactic:
simp only [tendsto_bot]

Premises used: Filter.tendsto_bot
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
⊢ Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)

Tactic:
have obs := BoundedContinuousFunction.isBounded_range_integral μs f
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
⊢ BddAbove (α := ℝ) ((fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) '' Set.univ)

Tactic:
simpa using obs.bddAbove

Premises used: Bornology.IsBounded.bddAbove
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i

Tactic:
have bdd_above := BddAbove.isBoundedUnder L.univ_mem (by simpa using obs.bddAbove)
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ BddBelow (α := ℝ) ((fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) '' Set.univ)

Tactic:
simpa using obs.bddBelow

Premises used: Bornology.IsBounded.bddBelow
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i

Tactic:
have bdd_below := BddBelow.isBoundedUnder L.univ_mem (by simpa using obs.bddBelow)
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
inr : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
inr₁ :
  LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
inr₂ :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_1
inr₃ :
  autoParam (IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
    tendsto_of_le_liminf_of_limsup_le._auto_3
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))

Tactic:
apply @tendsto_of_le_liminf_of_limsup_le ℝ ι _ _ _ L (fun i ↦ ∫ x, f x ∂(μs i)) (∫ x, f x ∂μ)

Premises used: tendsto_of_le_liminf_of_limsup_le
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
⊢ LE.le (α := ℝ) (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
    (liminf (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)

Tactic:
have key := h _ (f.add_norm_nonneg)
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  LE.le (α := ℝ) (∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μ)
    (liminf (fun (i : ι) ↦ ∫ (x : X), (f + const X ‖f‖ : (a : X) → ℝ) x ∂μs i) L)
⊢ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖ ≤
    liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L

Tactic:
simp_rw [f.integral_add_const ‖f‖] at key

Premises used: Norm.norm, BoundedContinuousFunction.integral_add_const
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
ι : Type u_2
L : Filter ι
μ : Measure X
inst_3 : IsProbabilityMeasure μ
μs : ι → Measure X
inst_4 : ∀ (i : ι), IsProbabilityMeasure (μs i)
h :
  ∀ (f : X →ᵇ ℝ),
    0 ≤ f →
      LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
f : X →ᵇ ℝ
hL : L.NeBot
obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
bdd_above : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
bdd_below : IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) L fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i
key :
  ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • ‖f‖ ≤
    liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + (μs i).real Set.univ • ‖f‖) L
⊢ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + ‖f‖ ≤ liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i + ‖f‖) L

Tactic:
simp only [probReal_univ, smul_eq_mul, one_mul] at key

Premises used: MeasureTheory.probReal_univ, smul_eq_mul, one_mul