awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ
have refine : HasFiniteIntegral (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ
Tactic: refine ⟨(NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ HasFiniteIntegral (NNReal.toReal ∘ (⇑f : (a : X) → ℝ≥0)) μ
have simp : ∫⁻ (a : X), (↑((f : (a : X) → ℝ≥0) a) : ℝ≥0∞) ∂μ < ∞
Tactic: simp only [hasFiniteIntegral_iff_enorm, Function.comp_apply, NNReal.enorm_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
μ : Measure X
inst_2 : IsFiniteMeasure μ
inst_3 : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (x : X), (f : (a : X) → ℝ) x ∂μ =
    HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
      (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
have simp : HSub.hSub (α := ℝ) (∫ (a : X), (NNReal.toReal ∘ (⇑f.nnrealPart : (a : X) → ℝ≥0)) a ∂μ)
    (∫ (a : X), (NNReal.toReal ∘ (⇑(-f).nnrealPart : (a : X) → ℝ≥0)) a ∂μ) =
  HSub.hSub (α := ℝ) (∫ (x : X), (↑((f.nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
    (∫ (x : X), (↑(((-f).nnrealPart : (a : X) → ℝ≥0) x) : ℝ) ∂μ)
Tactic: simp only [f.self_eq_nnrealPart_sub_nnrealPart_neg, Pi.sub_apply, integral_sub,
             integrable_of_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal = ∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ
have rw : (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal =
  (∫⁻ (a : X), ENNReal.ofReal (↑((f : (a : X) → ℝ≥0) a) : ℝ) ∂μ).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
Goal:
X : Type u_1
inst : MeasurableSpace X
inst_1 : TopologicalSpace X
inst_2 : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
rw :
  (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal =
    (∫⁻ (a : X), ENNReal.ofReal (↑((f : (a : X) → ℝ≥0) a) : ℝ) ∂μ).toReal
⊢ (∫⁻ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ).toReal = ∫ (x : X), (↑((f : (a : X) → ℝ≥0) x) : ℝ) ∂μ
have rw₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : X) ↦ (↑((f : (a : X) → ℝ≥0) x) : ℝ)
Tactic: rw [integral_eq_lintegral_of_nonneg_ae _ (by simpa [Function.comp_apply] using
        (NNReal.continuous_coe.comp f.continuous).measurable.aestronglyMeasurable)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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)) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ
have hfg : ∀ (x : X), NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E) ≤ ‖f‖₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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), (↑‖f‖₊ : ℝ≥0∞) ∂μ = HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have 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∞)
Tactic: rw [lintegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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)) : ℝ≥0∞) ∂μ ≤
    HMul.hMul (β := ℝ≥0∞) (↑‖f‖₊ : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have calc : ∫⁻ (x : X), (↑(NNNorm.nnnorm.{u_2} (E := E) ((f : (a : X) → E) x : E)) : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥0∞) ∂μ
Tactic: calc  ∫⁻ x, ‖f x‖₊ ∂μ
    _ ≤ ∫⁻ _, ‖f‖₊ ∂μ       := by gcongr; apply nnnorm_coe_le_nnnorm
    _ = ‖f‖₊ * (μ Set.univ) := by rw [lintegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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∞) ∂μ
⊢ ∫⁻ (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∞)
have calc₁ : ∫⁻ (x : X), (↑‖f‖₊ : ℝ≥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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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) μ
have refine : HasFiniteIntegral.{u_1, u_2} (ε := E) (⇑f : (a : X) → E) μ
Tactic: refine ⟨f.continuous.measurable.aestronglyMeasurable, (hasFiniteIntegral_def _ _).mp ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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
⊢ ∫ (x : X), ‖f‖ ∂μ = μ.real Set.univ • ‖f‖
have rw : μ.real Set.univ • ‖f‖ = μ.real Set.univ • ‖f‖
Tactic: rw [integral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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 ∂μ) ≤ μ.real Set.univ * ‖f‖
have calc : LE.le (α := ℝ) (∫ (x : X), norm.{u_2} (E := E) ((f : (a : X) → E) x : E) ∂μ) (∫ (x : X), ‖f‖ ∂μ)
Tactic: calc  ‖∫ x, f x ∂μ‖
    _ ≤ ∫ x, ‖f x‖ ∂μ := norm_integral_le_integral_norm _
    _ ≤ ∫ _, ‖f‖ ∂μ := ?_
    _ = μ.real Set.univ • ‖f‖ := by rw [integral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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‖ ∂μ)
have apply : Integrable (ε := ℝ) (fun (x : X) ↦ norm.{u_2} (E := E) ((f : (a : X) → E) x : E)) μ
Tactic: apply integral_mono _ (integrable_const ‖f‖) (fun x ↦ f.norm_coe_le_norm x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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 ∂μ) ≤ ‖f‖
have h : ‖f‖ = μ.real Set.univ * ‖f‖
Tactic: convert! f.norm_integral_le_mul_norm μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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
⊢ Bornology.IsBounded.{u_2} (α := E) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → E) x ∂μs i)
have apply : ∀ (v : E) (hv : Membership.mem (γ := Set E) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → E) x ∂μs i) v), ‖v‖ ≤ ‖f‖
Tactic: apply isBounded_iff_forall_norm_le.mpr ⟨‖f‖, fun v hv ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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
⊢ ‖v‖ ≤ ‖f‖
have obtain : ∀ (i : ι) (hi : (fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i = v), ‖v‖ ≤ ‖f‖
Tactic: obtain ⟨i, hi⟩ := hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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
⊢ ‖v‖ ≤ ‖f‖
have rw : norm.{u_2} (E := E) ((fun (i : ι) ↦ (∫ (x : X), (f : (a : X) → E) x ∂μs i : E)) i) ≤ ‖f‖
Tactic: rw [← hi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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 →ᵇ ℝ
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have 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 ∂μ))
Tactic: rcases eq_or_neBot L with rfl | hL
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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 ∂μ))
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have inr : ∀ (hL : L.NeBot),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have obs : Bornology.IsBounded (α := ℝ) (Set.range fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i)
Tactic: have obs := BoundedContinuousFunction.isBounded_range_integral μs f
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have bdd_above : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have bdd_below : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have apply : LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
Tactic: apply tendsto_of_le_liminf_of_limsup_le _ _ bdd_above bdd_below
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (goal)
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)
⊢ Tendsto (β := ℝ) (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L (𝓝 (∫ (x : X), (f : (a : X) → ℝ) x ∂μ))
have apply₁ : LE.le (α := ℝ) (limsup (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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 (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have 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 ∂μ)
Tactic: have key := h _ (f.norm_sub_nonneg)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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 ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have 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 ∂μ
Tactic: simp_rw [f.integral_const_sub ‖f‖] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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 ∂μ
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have key₁ : 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
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.BoundedContinuousFunction (hypothesis)
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 ∂μ
⊢ LE.le (α := ℝ) (∫ (x : X), (f : (a : X) → ℝ) x ∂μ) (liminf (fun (i : ι) ↦ ∫ (x : X), (f : (a : X) → ℝ) x ∂μs i) L)
have 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
Tactic: have := limsup_const_sub L (fun i ↦ ∫ x, f x ∂(μs i)) ‖f‖ bdd_above.isCobounded_ge bdd_below