awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
have apply : EqOn.{0, u_1} (β := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ)
  (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
Tactic: apply eventuallyEq_of_mem self_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (y : ℝ) ↦ ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
have this : EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
  ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
Tactic: have :
      (fun b => ∫ x in b₁..b, f x ∂μ) =ᶠ[𝓝[Icc b₁ b₂] b₀] fun b =>
        ∫ x in b₁..b₂, indicator {x | x ≤ b} f x ∂μ := by
      apply eventuallyEq_of_mem self_mem_nhdsWithin
      exact fun b b_in => (integral_indicator b_in).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (y : ℝ) ↦ ∫ (x : ℝ) in b₁..y, f x ∂μ) (Icc b₁ b₂) b₀
have apply : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
  b₀
Tactic: apply ContinuousWithinAt.congr_of_eventuallyEq _ this (integral_indicator h₀).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀
have this₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
Tactic: have : IntervalIntegrable (fun x => ‖f x‖) μ b₁ b₂ :=
      IntervalIntegrable.norm (h_int' <| right_mem_Icc.mpr h₁₂)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀
have refine_1 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
Tactic: refine continuousWithinAt_of_dominated_interval ?_ ?_ this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
refine_1 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀
have refine_2 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
Tactic: refine continuousWithinAt_of_dominated_interval ?_ ?_ this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ ‖f x‖) μ b₁ b₂
refine_1 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
refine_2 : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ) (Icc b₁ b₂)
    b₀
have refine_3 : ∀ᵐ (t : ℝ) ∂μ,
  t ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
Tactic: refine continuousWithinAt_of_dominated_interval ?_ ?_ this ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
have h : ∀ a ∈ Icc b₁ b₂, AEStronglyMeasurable (indicator {x : ℝ | x ≤ a} f) (μ.restrict (Ι b₁ b₂))
Tactic: filter_upwards [self_mem_nhdsWithin]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
have h : AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))
Tactic: rw [aestronglyMeasurable_indicator_iff, Measure.restrict_restrict, uIoc, Iic_def,
        Iic_inter_Ioc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
h : AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))
⊢ AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
have h₁ : x ≤ max b₁ b₂
Tactic: rw [aestronglyMeasurable_indicator_iff, Measure.restrict_restrict, uIoc, Iic_def,
        Iic_inter_Ioc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
h : AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))
h₁ : x ≤ max b₁ b₂
⊢ AEStronglyMeasurable (indicator {x_1 : ℝ | x_1 ≤ x} f) (μ.restrict (Ι b₁ b₂))
have h₂ : MeasurableSet (α := ℝ) {x_1 : ℝ | x_1 ≤ x}
Tactic: rw [aestronglyMeasurable_indicator_iff, Measure.restrict_restrict, uIoc, Iic_def,
        Iic_inter_Ioc_of_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x : ℝ
hx : x ∈ Icc b₁ b₂
⊢ AEStronglyMeasurable f (μ.restrict (Ioc (min b₁ b₂) x))
have h : AEStronglyMeasurable f (μ.restrict (Ioc b₁ x))
Tactic: rw [min₁₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
have refine_2 : ∀ (x : ℝ), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x : ℝ
⊢ ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
have refine_2 : ∀ t ∈ Ι b₁ b₂, ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
Tactic: filter_upwards with t
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖indicator {x_1 : ℝ | x_1 ≤ x} f t‖ ≤ ‖f t‖
have refine_2 : t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
Tactic: dsimp [indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x t : ℝ
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
have pos : t ≤ x → t ∈ Ι b₁ b₂ → ‖f t‖ ≤ ‖f t‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
x t : ℝ
pos : t ≤ x → t ∈ Ι b₁ b₂ → ‖f t‖ ≤ ‖f t‖
⊢ t ∈ Ι b₁ b₂ → ‖if t ≤ x then f t else 0‖ ≤ ‖f t‖
have neg : ¬t ≤ x → t ∈ Ι b₁ b₂ → norm.{u_1} (E := E) 0 ≤ ‖f t‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {b₀}ᶜ x → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (t : ℝ) ↦ t < b₀ ∨ b₀ < t) x} x}
    a
Tactic: filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_gt hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {b₀}ᶜ x → Membership.mem (γ := Set ℝ) {x : ℝ | (fun (t : ℝ) ↦ t < b₀ ∨ b₀ < t) x} x}
      a
⊢ ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
have h₁ : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) {b₀}ᶜ a → a < b₀ ∨ b₀ < a
Tactic: filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_gt hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
⊢ ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
have this₁ : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
Tactic: have : ∀ᵐ t ∂μ, t < b₀ ∨ b₀ < t := by
        filter_upwards [compl_mem_ae_iff.mpr hb₀] with x hx using Ne.lt_or_gt hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
⊢ ∀ᵐ (t : ℝ) ∂μ,
    t ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f t) (Icc b₁ b₂) b₀
have refine_3 : ∀ (x : ℝ),
  x < b₀ ∨ b₀ < x →
    x ∈ Ι b₁ b₂ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (x_1 : ℝ) ↦ indicator {x : ℝ | x ≤ x_1} f x) (Icc b₁ b₂) b₀
Tactic: apply this.mono
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀
have h : {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀
Tactic: apply mem_nhdsWithin_of_mem_nhds
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = f x₀) x} ∈ 𝓝 b₀
have h : ∀ (x : ℝ), x₀ < x → indicator {t : ℝ | t ≤ x} f x₀ = f x₀
Tactic: apply Eventually.mono (Ioi_mem_nhds hx₀)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have this₁ : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀
Tactic: have : ∀ᶠ x in 𝓝[Icc b₁ b₂] b₀, {t : ℝ | t ≤ x}.indicator f x₀ = f x₀ := by
          apply mem_nhdsWithin_of_mem_nhds
          apply Eventually.mono (Ioi_mem_nhds hx₀)
          intro x hx
          simp [hx.le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this_2 : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : x₀ < b₀
this : ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = f x₀
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (x : ℝ) ↦ indicator {x_1 : ℝ | x_1 ≤ x} f x₀) (Icc b₁ b₂) b₀
have refine_3 : indicator {t : ℝ | t ≤ b₀} f x₀ = f x₀
Tactic: apply continuousWithinAt_const.congr_of_eventuallyEq this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
a b₀ b₁ b₂ : ℝ
μ : Measure ℝ
f : ℝ → E
hb₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set ℝ) → ℝ≥0∞) {b₀} : ℝ≥0∞) (0 : ℝ≥0∞)
h_int : IntervalIntegrable f μ (min a b₁) (max a b₂)
h₀ : b₀ ∈ Icc b₁ b₂
h₁₂ : b₁ ≤ b₂
min₁₂ : min b₁ b₂ = b₁
h_int' : ∀ {x : ℝ}, x ∈ Icc b₁ b₂ → IntervalIntegrable f μ b₁ x
this_1 :
  EventuallyEq.{0, u_1} (β := E) (𝓝[Icc b₁ b₂] b₀) (fun (b : ℝ) ↦ ∫ (x : ℝ) in b₁..b, f x ∂μ) fun (b : ℝ) ↦
    ∫ (x : ℝ) in b₁..b₂, indicator {x : ℝ | x ≤ b} f x ∂μ
this : ∀ᵐ (t : ℝ) ∂μ, t < b₀ ∨ b₀ < t
x₀ : ℝ
hx₀ : b₀ < x₀
⊢ ∀ᶠ (x : ℝ) in 𝓝[Icc b₁ b₂] b₀, indicator {t : ℝ | t ≤ x} f x₀ = 0
have h : {x : ℝ | (fun (x : ℝ) ↦ indicator {t : ℝ | t ≤ x} f x₀ = 0) x} ∈ 𝓝 b₀
Tactic: apply mem_nhdsWithin_of_mem_nhds