awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hε' : 0 < ε / 3
Tactic: have hε' : 0 < ε / 3 := ENNReal.div_pos hε.ne' (ofNat_ne_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos : ∀ (Eg : Set α) (hmEg : MeasurableSet Eg) (hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: obtain ⟨Eg, hmEg, hμEg, hgε⟩ := MemLp.exists_eLpNorm_indicator_compl_lt hp' hg' hε'.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos : ∀ (Ef : Set α) (hmEf : MeasurableSet Ef) (hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞))
  (hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: obtain ⟨Ef, hmEf, hμEf, hfε⟩ := hut.exists_measurableSet_indicator hε'.ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hmE : MeasurableSet (Ef ∪ Eg)
Tactic: have hmE := hmEf.union hmEg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
hmE : MeasurableSet (Ef ∪ Eg)
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Ef ∪ Eg) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have hfmE := (measure_union_le Ef Eg).trans_lt (add_lt_top.mpr ⟨hμEf, hμEg⟩)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hgE' : MemLp g p (μ.restrict E)
Tactic: have hgE' := MemLp.restrict E hg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have huiE : UnifIntegrable f p (μ.restrict E)
Tactic: have huiE := hui.restrict E
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Tactic: have hfgE : (∀ᵐ x ∂(μ.restrict E), Tendsto (fun n => f n x) atTop (𝓝 (g x))) :=
    ae_restrict_of_ae hfg
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have ffmE := Fact.mk hfmE
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hInner : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)
Tactic: have hInner := tendsto_Lp_finite_of_tendsto_ae_of_meas hp hp' hf hg hgE' huiE hfgE
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p (μ.restrict E)) atTop (𝓝 0)
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have hInner₁ : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
Tactic: rw [ENNReal.tendsto_atTop_zero] at hInner
Cleared hypotheses: hInner
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have pos : ∀ (N : ℕ) (hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3), ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: obtain ⟨N, hfngε⟩ := hInner (ε / 3) hε'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
⊢ ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
have h : ∀ n ≥ N, eLpNorm (f n - g) p μ ≤ ε
Tactic: use N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
⊢ eLpNorm (f n - g) p μ ≤ ε
have hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
Tactic: have hmfngE : AEStronglyMeasurable _ μ := (((hf n).sub hg).indicator hmE).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
⊢ eLpNorm (f n - g) p μ ≤ ε
have hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
Tactic: have hfngEε := calc
    eLpNorm (E.indicator (f n - g)) p μ
      = eLpNorm (f n - g) p (μ.restrict E) := eLpNorm_indicator_eq_eLpNorm_restrict hmE
    _ ≤ ε / 3                              := hfngε n hn
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
⊢ eLpNorm (f n - g) p μ ≤ ε
have hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
Tactic: have hmgEc : AEStronglyMeasurable _ μ := (hg.indicator hmE.compl).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
have rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
Tactic: rw [compl_union, ← indicator_indicator]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), StronglyMeasurable (f n)
hg : StronglyMeasurable g
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ε : ℝ≥0∞
hε : ε > 0
hfinε : ε ≠ ∞
hμ : μ ≠ 0
hε' : 0 < ε / 3
Eg : Set α
hmEg : MeasurableSet Eg
hμEg : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Eg : ℝ≥0∞) (∞ : ℝ≥0∞)
hgε : eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), eLpNorm (Efᶜ.indicator (f i)) p μ ≤ ε / 3
E : Set α := Ef ∪ Eg
hmE : MeasurableSet E
hfmE : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hgE' : MemLp g p (μ.restrict E)
huiE : UnifIntegrable f p (μ.restrict E)
hfgE : ∀ᵐ (x : α) ∂μ.restrict E, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
ffmE : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞))
hInner : ∀ ε > 0, ∃ (N : ℕ), ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator g) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
have rw₁ : eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ
Tactic: rw [compl_union, ← indicator_indicator]