awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
⊢ ‖f p x‖ ≤ M + 1
have calc : ‖f p x‖ = ‖f q x + (f p x - f q x)‖
Tactic: calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
        _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
        _ ≤ M + δ := by
            gcongr
            · apply hM
              change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
              apply mem_image_of_mem
              simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
              exact h'δ hx
            · exact le_of_lt (hv _ hp _ (h'δ hx))
        _ ≤ M + 1 := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
calc : ‖f p x‖ = ‖f q x + (f p x - f q x)‖
⊢ ‖f p x‖ ≤ M + 1
have calc₁ : ‖f q x‖ + ‖f p x - f q x‖ ≤ M + δ
Tactic: calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
        _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
        _ ≤ M + δ := by
            gcongr
            · apply hM
              change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
              apply mem_image_of_mem
              simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
              exact h'δ hx
            · exact le_of_lt (hv _ hp _ (h'δ hx))
        _ ≤ M + 1 := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
X : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : TopologicalSpace X
μ : Measure ℝ
inst_3 : NoAtoms μ
inst_4 : IsLocallyFiniteMeasure μ
f : X → ℝ → E
a₀ : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
q : X
b₀ ε : ℝ
εpos : ε > 0
a : ℝ
a_lt : a < a₀ ∧ a < b₀
b : ℝ
lt_b : a₀ < b ∧ b₀ < b
this_1 : IsCompact (SProd.sprod (α := Set X) {q} (Icc a b))
M : ℝ
hM :
  Membership.mem (γ := Set ℝ)
    (upperBounds ((fun (x : X × ℝ) ↦ ‖Function.uncurry f x‖) '' SProd.sprod (α := Set X) {q} (Icc a b))) M
δ : ℝ
δpos : 0 < δ
hδ : δ < 1
h'δ : Icc (b₀ - δ) (b₀ + δ) ⊆ Icc a b
h''δ : (M + 1) * μ.real (Icc (b₀ - δ) (b₀ + δ)) + δ * μ.real (Icc a b) < ε
v : Set X
v_mem : v ∈ 𝓝[univ] q
this : v ×ˢ Ioo (b₀ - δ) (b₀ + δ) ∈ 𝓝 (q, b₀)
p : X
s : ℝ
hp : p ∈ v
hs : s ∈ Ioo (b₀ - δ) (b₀ + δ)
hv : ∀ p ∈ v, ∀ x ∈ Icc a b, ‖f p x - f q x‖ < δ
J : ∀ (r : X) (u v : ℝ), IntervalIntegrable (f r) μ u v
x : ℝ
hx : x ∈ Icc (b₀ - δ) (b₀ + δ)
calc : ‖f p x‖ = ‖f q x + (f p x - f q x)‖
calc₁ : ‖f q x‖ + ‖f p x - f q x‖ ≤ M + δ
⊢ ‖f p x‖ ≤ M + 1
have calc₂ : M + δ ≤ M + 1
Tactic: calc ‖f p x‖ = ‖f q x + (f p x - f q x)‖ := by congr; abel
        _ ≤ ‖f q x‖ + ‖f p x - f q x‖ := norm_add_le _ _
        _ ≤ M + δ := by
            gcongr
            · apply hM
              change (fun x ↦ ‖Function.uncurry f x‖) (q, x) ∈ _
              apply mem_image_of_mem
              simp only [singleton_prod, mem_image, Prod.mk.injEq, true_and, exists_eq_right]
              exact h'δ hx
            · exact le_of_lt (hv _ hp _ (h'δ hx))
        _ ≤ M + 1 := by linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a₀
have simp_rw : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀
Tactic: simp_rw [← integral_indicator measurableSet_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀
have hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀
have h_bound : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀
have bound_integrable : Integrable ((Ioi a₀).indicator (norm ∘ f)) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a
bound_integrable : Integrable ((Ioi a₀).indicator (norm ∘ f)) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Ioi b).indicator f x ∂μ) (Ici a₀) a₀
have h_lim : ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Ioi a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, AEStronglyMeasurable ((Ioi n).indicator f) μ
have h : ∀ (a : ℝ) (ha : a ∈ Ici a₀), AEStronglyMeasurable ((Ioi a).indicator f) μ
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ AEStronglyMeasurable ((Ioi a).indicator f) μ
have h : AEStronglyMeasurable f (μ.restrict (Ioi a))
Tactic: rw [aestronglyMeasurable_indicator_iff measurableSet_Ioi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≥] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Ioi n).indicator f a‖ ≤ (Ioi a₀).indicator (norm ∘ f) a
have h : ∀ (a : ℝ) (ha : a ∈ Ici a₀), ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Ioi a).indicator f a_1‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_1
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
⊢ ∀ᵐ (a_1 : ℝ) ∂μ, ‖(Ioi a).indicator f a_1‖ ≤ (Ioi a₀).indicator (norm ∘ f) a_1
have h : ∀ (x : ℝ), ‖(Ioi a).indicator f x‖ ≤ (Ioi a₀).indicator (norm ∘ f) x
Tactic: refine ae_of_all _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a ∈ Ici a₀
x : ℝ
⊢ ‖(Ioi a).indicator f x‖ ≤ (Ioi a₀).indicator (norm ∘ f) x
have h : (Ioi a).indicator (fun (a : ℝ) ↦ ‖f a‖) x ≤ (Ioi a₀).indicator (norm ∘ f) x
Tactic: rw [norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
⊢ ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f a) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f a))
have h_lim : ∀ (x : ℝ), Tendsto (fun (n : ℝ) ↦ (Ioi n).indicator f x) (𝓝[≥] a₀) (𝓝 ((Ioi a₀).indicator f x))
Tactic: refine ae_of_all _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
have pos : ∀ (hx : a₀ < x), Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
Tactic: by_cases hx : a₀ < x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
pos : ∀ (hx : a₀ < x), Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
have neg : ∀ (hx : ¬a₀ < x), Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
Tactic: by_cases hx : a₀ < x
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
have pos : EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
  if n < x then f x else 0
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
⊢ Tendsto (fun (n : ℝ) ↦ if n < x then f x else 0) (𝓝[≥] a₀) (𝓝 (if a₀ < x then f x else 0))
have neg : EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
  if n < x then f x else 0
Tactic: apply tendsto_const_nhds.congr'
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      x_1 ∈ Iio x →
        Membership.mem (γ := Set ℝ)
          {x_2 : ℝ |
            (fun (x_3 : ℝ) ↦
                Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                  ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : a₀ < x
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Iio x →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
                x_2}
            x_1}
      a
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
have h₁ : ∀ a ∈ Iio x, (if a₀ < x then f x else 0) = if a < x then f x else 0
Tactic: filter_upwards [mem_nhdsWithin_of_mem_nhds (Iio_mem_nhds hx)] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ |
      x_1 ∈ Ici a₀ →
        Membership.mem (γ := Set ℝ)
          {x_2 : ℝ |
            (fun (x_3 : ℝ) ↦
                Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                  ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
              x_2}
          x_1}
    a
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
x : ℝ
hx : ¬a₀ < x
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ |
        x_1 ∈ Ici a₀ →
          Membership.mem (γ := Set ℝ)
            {x_2 : ℝ |
              (fun (x_3 : ℝ) ↦
                  Eq.{u_1 + 1} (α := E) ((fun (x_4 : ℝ) ↦ if a₀ < x then f x else 0) x_3)
                    ((fun (n : ℝ) ↦ if n < x then f x else 0) x_3))
                x_2}
            x_1}
      a
⊢ EventuallyEq.{0, u_1} (β := E) (𝓝[≥] a₀) (fun (x_1 : ℝ) ↦ if a₀ < x then f x else 0) fun (n : ℝ) ↦
    if n < x then f x else 0
have h₁ : ∀ a ∈ Ici a₀, (if a₀ < x then f x else 0) = if a < x then f x else 0
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha using by grind
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
⊢ a ∈ Ici a₀ → ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a
have a₁ : ∀ (ha : a₀ ≤ a), ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a
Tactic: (ha : a₀ ≤ a)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀) a
have rw : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a ∧
  ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
Tactic: rw [continuousWithinAt_iff_continuous_left_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
have left : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
left : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Iic a) a ∧
    ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
have right : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Ici a₀ ∩ Ici a) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a
have h_int : IntervalIntegrable f μ a₀ a
Tactic: have h_int : IntervalIntegrable f μ a₀ a :=
      (intervalIntegrable_iff_integrableOn_Ioc_of_le ha).2 <| hf.mono_set Ioc_subset_Ioi_self
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a
have h_split : ∀ b ∈ Icc a₀ a,
  ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
Tactic: have h_split : ∀ b ∈ Icc a₀ a, ∫ x in Ioi b, f x ∂μ =
        (∫ x in Ioi a₀, f x ∂μ) - ∫ x in a₀..b, f x ∂μ := by
      intro b hb
      simp [← integral_Ioi_sub_Ioi hf hb.1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
inst_2 : NoAtoms μ
a₀ : ℝ
hf : IntegrableOn f (Ioi a₀) μ
a : ℝ
ha : a₀ ≤ a
h_int : IntervalIntegrable f μ a₀ a
h_split :
  ∀ b ∈ Icc a₀ a,
    ∫ (x : ℝ) in Ioi b, f x ∂μ = HSub.hSub (α := E) (∫ (x : ℝ) in Ioi a₀, f x ∂μ) (∫ (x : ℝ) in a₀..b, f x ∂μ)
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Ioi b, f x ∂μ) (Icc a₀ a) a
have h_cwa : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in a₀..b, f x ∂μ) (Icc a₀ a) a
Tactic: have h_cwa : ContinuousWithinAt (fun b ↦ ∫ x in a₀..b, f x ∂μ) (Icc a₀ a) a :=
      continuousWithinAt_primitive (measure_singleton a) (by simpa [ha])
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ) in Iio b, f x ∂μ) (Iic a₀) a₀
have simp_rw : ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
Tactic: simp_rw [← integral_indicator measurableSet_Iio]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
have hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
have h_bound : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
have bound_integrable : Integrable ((Iio a₀).indicator (norm ∘ f)) μ
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
hF_meas : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
h_bound : ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, ∀ᵐ (a : ℝ) ∂μ, ‖(Iio n).indicator f a‖ ≤ (Iio a₀).indicator (norm ∘ f) a
bound_integrable : Integrable ((Iio a₀).indicator (norm ∘ f)) μ
⊢ ContinuousWithinAt.{0, u_1} (Y := E) (fun (b : ℝ) ↦ ∫ (x : ℝ), (Iio b).indicator f x ∂μ) (Iic a₀) a₀
have h_lim : ∀ᵐ (a : ℝ) ∂μ, Tendsto (fun (n : ℝ) ↦ (Iio n).indicator f a) (𝓝[≤] a₀) (𝓝 ((Iio a₀).indicator f a))
Tactic: apply tendsto_integral_filter_of_dominated_convergence ((Iio a₀).indicator (norm ∘ f))
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.DominatedConvergence (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
a₀ : ℝ
hf : IntegrableOn f (Iio a₀) μ
⊢ ∀ᶠ (n : ℝ) in 𝓝[≤] a₀, AEStronglyMeasurable ((Iio n).indicator f) μ
have h : ∀ (a : ℝ) (ha : a ∈ Iic a₀), AEStronglyMeasurable ((Iio a).indicator f) μ
Tactic: filter_upwards [self_mem_nhdsWithin] with a ha