awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)

Tactic:
exact Eventually.of_forall (by simp)

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
f : X →ᵇ E
hfg : ∀ (x : X), NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E) ≤ ‖f‖₊
⊢ ∫⁻ (x : X), (↑(NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E)) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
f : X →ᵇ E
x : X
⊢ NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E) ≤ ‖f‖₊

Tactic:
apply nnnorm_coe_le_nnnorm

Premises used: BoundedContinuousFunction.nnnorm_coe_le_nnnorm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
f : X →ᵇ E
rw rw₁ :
  HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ = HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
rw [lintegral_const]

Premises used: MeasureTheory.lintegral_const
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
f : X →ᵇ E
calc : ∫⁻ (x : X), (↑(NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E)) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ
calc₁ : ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ = HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)
⊢ ∫⁻ (x : X), (↑(NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E)) : ℝ≥0∞) ∂μ ≤
    HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
calc  ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ∫⁻ _, ‖f‖₊ ∂μ       := by gcongr; apply nnnorm_coe_le_nnnorm
    _ = ‖f‖₊ * (μ Set.univ) := by rw [lintegral_const]

Premises used: Set.univ, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable.{u_2, u_1} (ε := E) (⇑f : (a : X) → E) μ

Tactic:
⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩

Premises used: MeasureTheory.hasFiniteIntegral_def, Measurable.aestronglyMeasurable, MeasureTheory.Integrable, BoundedContinuousFunction.continuous, And.intro, Continuous.measurable, Iff.mp
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : IsFiniteMeasure μ
f : X →ᵇ E
refine : HasFiniteIntegral.{u_1, u_2} (ε := E) (⇑f : (a : X) → E) μ
⊢ Integrable.{u_2, u_1} (ε := E) (⇑f : (a : X) → E) μ

Tactic:
refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ∫⁻ (x : X), (↑(NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E)) : ℝ≥0∞) ∂μ ≤
    HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
f.lintegral_nnnorm_le μ

Premises used: BoundedContinuousFunction.lintegral_nnnorm_le
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞) < ∞

Tactic:
ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

Premises used: MeasureTheory.measure_lt_top, Set.univ, ENNReal.mul_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ HasFiniteIntegral.{u_1, u_2} (ε := E) (⇑f : (a : X) → E) μ

Tactic:
calc  ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ‖f‖₊ * (μ Set.univ) := f.lintegral_nnnorm_le μ
    _ < ∞                   := ENNReal.mul_lt_top ENNReal.coe_lt_top (measure_lt_top μ Set.univ)

Premises used: MeasureTheory.measure_lt_top, Set.univ, BoundedContinuousFunction.lintegral_nnnorm_le, ENNReal.mul_lt_top, DFunLike.coe, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ norm.{u_2} (E := E) (∫ (x : X), (f : (a : X) → E) x ∂μ) ≤ ∫ (x : X), norm.{u_2} (E := E) ((f : (a : X) → E) x : E) ∂μ

Tactic:
norm_integral_le_integral_norm _

Premises used: MeasureTheory.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ LE.le (α := ℝ) (∫ (x : X), norm.{u_2} (E := E) ((f : (a : X) → E) x : E) ∂μ) (∫ (x : X), ‖f‖ ∂μ)

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
rw rw₁ : μ.real Set.univ • ‖f‖ = μ.real Set.univ • ‖f‖
⊢ ∫ (x : X), ‖f‖ ∂μ = μ.real Set.univ • ‖f‖

Tactic:
rw [integral_const]

Premises used: MeasureTheory.integral_const
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
calc : LE.le (α := ℝ) (∫ (x : X), norm.{u_2} (E := E) ((f : (a : X) → E) x : E) ∂μ) (∫ (x : X), ‖f‖ ∂μ)
⊢ norm.{u_2} (E := E) (∫ (x : X), (f : (a : X) → E) x ∂μ) ≤ μ.real Set.univ * ‖f‖

Tactic:
calc  ‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]

Premises used: Set.univ, MeasureTheory.Measure.real, MeasureTheory.norm_integral_le_integral_norm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
apply : Integrable (ε := ℝ) (fun (x : X) ↦ norm.{u_2} (E := E) ((f : (a : X) → E) x : E)) μ
⊢ LE.le (α := ℝ) (∫ (x : X), norm.{u_2} (E := E) ((f : (a : X) → E) x : E) ∂μ) (∫ (x : X), ‖f‖ ∂μ)

Tactic:
apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x)

Premises used: Norm.norm, MeasureTheory.integral_mono, BoundedContinuousFunction.norm_coe_le_norm, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable (ε := ℝ) (fun (x : X) ↦ norm.{u_2} (E := E) ((f : (a : X) → E) x : E)) μ

Tactic:
(integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ)

Premises used: Iff.mpr, Measurable.aestronglyMeasurable, BoundedContinuousFunction.integrable, BoundedContinuousFunction.continuous, MeasureTheory.integrable_norm_iff, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable (ε := ℝ) (fun (x : X) ↦ norm.{u_2} (E := E) ((f : (a : X) → E) x : E)) μ

Tactic:
exact (integrable_norm_iff f.continuous.measurable.aestronglyMeasurable).mpr (f.integrable μ)

Premises used: Iff.mpr, Measurable.aestronglyMeasurable, BoundedContinuousFunction.integrable, BoundedContinuousFunction.continuous, MeasureTheory.integrable_norm_iff, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ norm.{u_2} (E := E) (∫ (x : X), (f : (a : X) → E) x ∂μ) ≤ μ.real Set.univ * ‖f‖

Tactic:
f.norm_integral_le_mul_norm μ

Premises used: BoundedContinuousFunction.norm_integral_le_mul_norm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsProbabilityMeasure μ
f : X →ᵇ E
h : ‖f‖ = μ.real Set.univ * ‖f‖
⊢ norm.{u_2} (E := E) (∫ (x : X), (f : (a : X) → E) x ∂μ) ≤ ‖f‖

Tactic:
convert! f.norm_integral_le_mul_norm μ

Premises used: BoundedContinuousFunction.norm_integral_le_mul_norm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
inst_8 : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖f‖ = μ.real Set.univ * ‖f‖

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst_8 : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
apply :
  ∀ (v : E) (hv : Membership.mem (γ := Set E) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → E) x ∂μs i) v),
    ‖v‖ ≤ ‖f‖
⊢ Bornology.IsBounded.{u_2} (α := E) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → E) x ∂μs i)

Tactic:
apply isBounded_iff_forall_norm_le.mpr ⟨‖f‖, fun v hv ↦ ?_⟩

Premises used: Iff.mpr, Norm.norm, isBounded_iff_forall_norm_le, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst_8 : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
hv : Membership.mem (γ := Set E) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → E) x ∂μs i) v
obtain : ∀ (i : ι) (hi : (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i = v), ‖v‖ ≤ ‖f‖
⊢ ‖v‖ ≤ ‖f‖

Tactic:
obtain ⟨i, hi⟩ := hv
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst_8 : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i = v
rw : norm.{u_2} (E := E) ((fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i) ≤ ‖f‖
⊢ ‖v‖ ≤ ‖f‖

Tactic:
rw [← hi]
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace X
inst_4 : SecondCountableTopology E
inst_5 : MeasurableSpace E
inst_6 : BorelSpace E
inst_7 : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst_8 : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
v : E
i : ι
hi : (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i = v
⊢ norm.{u_2} (E := E) ((fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i) ≤ ‖f‖

Tactic:
apply f.norm_integral_le_norm (μs i)

Premises used: BoundedContinuousFunction.norm_integral_le_norm
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (f + const X c : (a : X) → ℝ) x ∂μ = ∫ (x : X), (f : (a : X) → ℝ) x ∂μ + μ.real Set.univ • c

Tactic:
simp [integral_add (f.integrable _) (integrable_const c)]

Premises used: BoundedContinuousFunction.integrable, MeasureTheory.integrable_const, MeasureTheory.integral_add
-- Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
μ : Measure X
inst_3 : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (const X c - f : (a : X) → ℝ) x ∂μ = μ.real Set.univ • c - ∫ (x : X), (f : (a : X) → ℝ) x ∂μ

Tactic:
simp [integral_sub (integrable_const c) (f.integrable _)]

Premises used: BoundedContinuousFunction.integrable, MeasureTheory.integral_sub, MeasureTheory.integrable_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 →ᵇ ℝ
inl :
  ∀
    (h :
      ∀ (f : X →ᵇ ℝ),
        0 ≤ f →
          LE.le (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥)
            (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)),
    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 (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) ⊥) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
⊢ 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 (α := ℝ) (limsup (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ)
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 (α := ℝ) (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)
⊢ 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 (α := ℝ) (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)
⊢ 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 (α := ℝ) (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
⊢ 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 (α := ℝ) (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
⊢ 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 (α := ℝ) (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
apply :
  LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
apply₁ :
  LE.le (α := ℝ) (limsup (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:
apply tendsto_of_le_liminf_of_limsup_le _ _ bdd_above bdd_below

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 (α := ℝ) (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), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μs i) L)
    (∫ (x : X), (const X ‖f‖ - f : (a : X) → ℝ) x ∂μ)

Tactic:
have key := h _ (f.norm_sub_nonneg)