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
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 (f n - g) p μ ≤ ε
have hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
Tactic: have hgEcε := calc
    eLpNorm (Eᶜ.indicator g) p μ
      ≤ eLpNorm (Efᶜ.indicator (Egᶜ.indicator g)) p μ := by
        unfold E; rw [compl_union, ← indicator_indicator]
    _ ≤ eLpNorm (Egᶜ.indicator g) p μ := eLpNorm_indicator_le _
    _ ≤ ε / 3 := hgε.le
-- 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
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
⊢ eLpNorm (f n - g) p μ ≤ ε
have hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
Tactic: have hmfnEc : AEStronglyMeasurable _ μ := ((hf n).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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
have rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
Tactic: rw [compl_union, inter_comm, ← 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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
have rw₁ : eLpNorm ((Egᶜ ∩ Efᶜ).indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
Tactic: rw [compl_union, inter_comm, ← 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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
rw : eLpNorm ((Efᶜ ∩ Egᶜ).indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
rw₁ : eLpNorm ((Egᶜ ∩ Efᶜ).indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
⊢ eLpNorm ((Ef ∪ Eg)ᶜ.indicator (f n)) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
have rw₂ : eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ
Tactic: rw [compl_union, inter_comm, ← indicator_indicator]
-- 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
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
⊢ eLpNorm (f n - g) p μ ≤ ε
have hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
Tactic: have hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3 := calc
    eLpNorm (Eᶜ.indicator (f n)) p μ
      ≤ eLpNorm (Egᶜ.indicator (Efᶜ.indicator (f n))) p μ := by
        unfold E; rw [compl_union, inter_comm, ← indicator_indicator]
    _ ≤ eLpNorm (Efᶜ.indicator (f n)) p μ := eLpNorm_indicator_le _
    _ ≤ ε / 3 := hfε 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
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
⊢ eLpNorm (f n - g) p μ ≤ ε
have hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
Tactic: have hmfngEc : AEStronglyMeasurable _ μ :=
    (((hf n).sub 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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ eLpNorm (Eᶜ.indicator (f n - g)) p μ = eLpNorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ
have rw : eLpNorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ = eLpNorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ
Tactic: rw [(Eᶜ.indicator_sub' _ _)]
-- 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
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
⊢ eLpNorm (f n - g) p μ ≤ ε
have hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
Tactic: have hfngEcε := calc
    eLpNorm (Eᶜ.indicator (f n - g)) p μ
      = eLpNorm (Eᶜ.indicator (f n) - Eᶜ.indicator g) p μ := by
        rw [(Eᶜ.indicator_sub' _ _)]
    _ ≤ eLpNorm (Eᶜ.indicator (f n)) p μ + eLpNorm (Eᶜ.indicator g) p μ := by
        apply eLpNorm_sub_le (by assumption) (by assumption) hp
    _ ≤ ε / 3 + ε / 3 := add_le_add hfnEcε hgEcε
-- 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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ eLpNorm (f n - g) p μ = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ
have e_f : f n - g = Eᶜ.indicator (f n - g) + E.indicator (f n - g)
Tactic: congr
-- 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) μ
hgEcε : eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
⊢ eLpNorm (f n - g) p μ ≤ ε
have eLpNorm : eLpNorm (f n - g) p μ = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ
Tactic: calc
    eLpNorm (f n - g) p μ
      = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ := by
        congr; exact (E.indicator_compl_add_self _).symm
    _ ≤ eLpNorm (indicator Eᶜ (f n - g)) p μ + eLpNorm (indicator E (f n - g)) p μ := by
        apply eLpNorm_add_le (by assumption) (by assumption) hp
    _ ≤ (ε / 3 + ε / 3) + ε / 3 := add_le_add hfngEcε hfngEε
    _ = ε := by simp only [ENNReal.add_thirds]
-- 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ε : MeasureTheory.eLpNorm (Egᶜ.indicator g) p μ < ε / 3
Ef : Set α
hmEf : MeasurableSet Ef
hμEf : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) Ef : ℝ≥0∞) (∞ : ℝ≥0∞)
hfε : ∀ (i : ℕ), MeasureTheory.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, MeasureTheory.eLpNorm (f n - g) p (μ.restrict E) ≤ ε
N : ℕ
hfngε : ∀ n ≥ N, MeasureTheory.eLpNorm (f n - g) p (μ.restrict E) ≤ ε / 3
n : ℕ
hn : n ≥ N
hmfngE : AEStronglyMeasurable (E.indicator (f n - g)) μ
hfngEε : MeasureTheory.eLpNorm (E.indicator (f n - g)) p μ ≤ ε / 3
hmgEc : AEStronglyMeasurable (Eᶜ.indicator g) μ
hgEcε : MeasureTheory.eLpNorm (Eᶜ.indicator g) p μ ≤ ε / 3
hmfnEc : AEStronglyMeasurable (Eᶜ.indicator (f n)) μ
hfnEcε : MeasureTheory.eLpNorm (Eᶜ.indicator (f n)) p μ ≤ ε / 3
hmfngEc : AEStronglyMeasurable (Eᶜ.indicator (f n - g)) μ
hfngEcε : MeasureTheory.eLpNorm (Eᶜ.indicator (f n - g)) p μ ≤ ε / 3 + ε / 3
eLpNorm :
  MeasureTheory.eLpNorm (f n - g) p μ = MeasureTheory.eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ
⊢ MeasureTheory.eLpNorm (f n - g) p μ ≤ ε
have eLpNorm₁ : MeasureTheory.eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ ≤
  MeasureTheory.eLpNorm (Eᶜ.indicator (f n - g)) p μ + MeasureTheory.eLpNorm (E.indicator (f n - g)) p μ
Tactic: calc
    eLpNorm (f n - g) p μ
      = eLpNorm (Eᶜ.indicator (f n - g) + E.indicator (f n - g)) p μ := by
        congr; exact (E.indicator_compl_add_self _).symm
    _ ≤ eLpNorm (indicator Eᶜ (f n - g)) p μ + eLpNorm (indicator E (f n - g)) p μ := by
        apply eLpNorm_add_le (by assumption) (by assumption) hp
    _ ≤ (ε / 3 + ε / 3) + ε / 3 := add_le_add hfngEcε hfngEε
    _ = ε := by simp only [ENNReal.add_thirds]