awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ).toReal =
    (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal
have h : ∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) sorry - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ =
  ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ ∫⁻ (a : α), ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ ∂μ =
    ∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ
have h : (ae μ).EventuallyEq (β := ℝ≥0∞)
  (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n) sorry - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ) fun (a : α) ↦
  ENNReal.ofReal ‖fs n a - f a‖
Tactic: refine lintegral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞)
    (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n) ⋯ - Integrable.toL1 f f_int) : α →ₘ[μ] E) : α → E) a‖ₑ) fun (a : α) ↦
    ENNReal.ofReal ‖fs n a - f a‖
have h : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) sorry) : α →ₘ[μ] E) : α → E) a‖ₑ)
  fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖
Tactic: rw [← Integrable.toL1_sub]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) a‖ₑ)
    fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖
have h : ∀ (x : α) (hx : (↑(↑(Integrable.toL1 (fs n - f) sorry) : α →ₘ[μ] E) : α → E) x = (fs n - f) x),
  Eq (α := ℝ≥0∞) ((fun (a : α) ↦ ‖(↑(↑(Integrable.toL1 (fs n - f) sorry) : α →ₘ[μ] E) : α → E) a‖ₑ) x)
    ((fun (a : α) ↦ ENNReal.ofReal ‖fs n a - f a‖) x)
Tactic: refine ((fs_int n).sub f_int).coeFn_toL1.mono fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : (↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x = (fs n - f) x
⊢ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
have h : ‖(fs n - f) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
Tactic: rw [hx, ofReal_norm, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : (↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x = (fs n - f) x
h : ‖(fs n - f) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
⊢ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
have h₁ : ‖(fs n - f) x‖ₑ = ‖fs n x - f x‖ₑ
Tactic: rw [hx, ofReal_norm, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
fs : ℕ → α → E
f : α → E
bound : α → ℝ
fs_measurable : ∀ (n : ℕ), AEStronglyMeasurable (fs n) μ
bound_integrable : Integrable bound μ
h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs n a) atTop (𝓝 (f a))
hF : CompleteSpace F
f_measurable : AEStronglyMeasurable f μ
fs_int : ∀ (n : ℕ), Integrable (fs n) μ
f_int : Integrable f μ
lintegral_norm_tendsto_zero :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ (∫⁻ (a : α), ENNReal.ofReal ‖fs n a - f a‖ ∂μ).toReal) atTop (𝓝 0)
n : ℕ
x : α
hx : (↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x = (fs n - f) x
h : ‖(fs n - f) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
h₁ : ‖(fs n - f) x‖ₑ = ‖fs n x - f x‖ₑ
⊢ ‖(↑(↑(Integrable.toL1 (fs n - f) ⋯) : α →ₘ[μ] E) : α → E) x‖ₑ = ENNReal.ofReal ‖fs n x - f x‖
have h₂ : ‖fs n x - f x‖ₑ = ‖fs n x - f x‖ₑ
Tactic: rw [hx, ofReal_norm, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
⊢ Tendsto (fun (n : ι) ↦ setToFun μ T hT (fs n)) l (𝓝 (setToFun μ T hT f))
have rw : ∀ (x : ℕ → ι), Tendsto x atTop l → Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
Tactic: rw [tendsto_iff_seq_tendsto]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
have rwa : ∀ (xl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s), ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
Tactic: rwa [tendsto_atTop'] at xl
Cleared hypotheses: xl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
have hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
Tactic: have hxl : ∀ s ∈ l, ∃ a, ∀ b ≥ a, x b ∈ s := by rwa [tendsto_atTop'] at xl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (hypothesis)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
have h : {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
    {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
  l
Tactic: have h :
    { x : ι | (fun n => AEStronglyMeasurable (fs n) μ) x } ∩
        { x : ι | (fun n => ∀ᵐ a ∂μ, ‖fs n a‖ ≤ bound a) x } ∈ l :=
    inter_mem hfs_meas h_bound
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
have obtain : ∀ (k : ℕ)
  (h :
    ∀ b ≥ k,
      Membership.mem (γ := Set ι)
        ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
          {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
        (x b)),
  Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
Tactic: obtain ⟨k, h⟩ := hxl _ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ Tendsto ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) atTop (𝓝 (setToFun μ T hT f))
have rw : Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
Tactic: rw [← tendsto_add_atTop_iff_nat k]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
have refine_1 : ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ
Tactic: refine tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
have refine_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a
Tactic: refine tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
refine_1 : ∀ (n : ℕ), AEStronglyMeasurable (fs (x (n + k))) μ
refine_2 : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs (x (n + k)) a‖ ≤ bound a
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ι) ↦ setToFun μ T hT (fs n)) ∘ x) (n + k)) atTop (𝓝 (setToFun μ T hT f))
have refine_3 : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
Tactic: refine tendsto_setToFun_of_dominated_convergence hT bound ?_ bound_integrable ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
have h₁ : ∀ (a : α), Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
Tactic: filter_upwards [h_lim]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
ι : Type u_7
l : Filter ι
inst_4 : l.IsCountablyGenerated
fs : ι → α → E
f : α → E
bound : α → ℝ
hfs_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (fs n) μ
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_lim : ∀ᵐ (a : α) ∂μ, Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))
x : ℕ → ι
xl : Tendsto x atTop l
hxl : ∀ s ∈ l, ∃ (a : ℕ), ∀ b ≥ a, x b ∈ s
h_1 :
  {x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
      {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x} ∈
    l
k : ℕ
h :
  ∀ b ≥ k,
    Membership.mem (γ := Set ι)
      ({x : ι | (fun (n : ι) ↦ AEStronglyMeasurable (fs n) μ) x} ∩
        {x : ι | (fun (n : ι) ↦ ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a) x})
      (x b)
⊢ ∀ (a : α), Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a)) → Tendsto (fun (n : ℕ) ↦ fs (x (n + k)) a) atTop (𝓝 (f a))
have h₁ : ∀ (a : α) (h_lin : Tendsto (fun (n : ι) ↦ fs n a) l (𝓝 (f a))), Tendsto (fun (n : ℕ) ↦ x (n + k)) atTop l
Tactic: refine fun a h_lin => @Tendsto.comp _ _ _ (fun n => x (n + k)) (fun n => fs n a) _ _ _ h_lin ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x
have refine_1 : ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
Tactic: refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.SetToL1 (goal)
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
C : ℝ
X : Type u_7
inst_4 : TopologicalSpace X
inst_5 : FirstCountableTopology X
hT : DominatedFinMeasAdditive μ T C
fs : X → α → E
bound : α → ℝ
s : Set X
hfs_meas : ∀ x ∈ s, AEStronglyMeasurable (fs x) μ
h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
bound_integrable : Integrable bound μ
h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn.{u_7, u_2} (Y := E) (fun (x : X) ↦ fs x a) s
x : X
hx : x ∈ s
refine_1 : ∀ᶠ (x : X) in 𝓝[s] x, AEStronglyMeasurable (fs x) μ
⊢ ContinuousWithinAt.{u_7, u_3} (Y := F) (fun (x : X) ↦ setToFun μ T hT (fs x)) s x
have refine_2 : ∀ᶠ (x : X) in 𝓝[s] x, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a
Tactic: refine continuousWithinAt_setToFun_of_dominated hT ?_ ?_ bound_integrable ?_