awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
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 μ
⊢ MeasureTheory.eLpNorm (f n - g) p μ ≤ ε
have eLpNorm₂ : ε / 3 + ε / 3 + ε / 3 = ε
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 (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n
hgg' : g =ᶠ[ae μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (g' x))
have hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x
Tactic: have hff'' := eventually_countable_forall.mpr hff'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n
hgg' : g =ᶠ[ae μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (g' x))
have h : ∀ (x : α) (hff'x : ∀ (i : ℕ), f i x = f' i x) (hgg'x : g x = g' x)
  (hfgx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))), Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (g' x))
Tactic: filter_upwards [hff'', hgg', hfg] with x hff'x hgg'x hfgx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
f f' : ℕ → α → β
g g' : α → β
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] f' n
hgg' : g =ᶠ[ae μ] g'
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hff'' : ∀ᵐ (x : α) ∂μ, ∀ (i : ℕ), f i x = f' i x
x : α
hff'x : ∀ (i : ℕ), f i x = f' i x
hgg'x : g x = g' x
hfgx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun (n : ℕ) ↦ f' n x) atTop (𝓝 (g' x))
have h : Tendsto (fun (x_1 : ℕ) ↦ f x_1 x) atTop (𝓝 (g' x))
Tactic: apply Tendsto.congr hff'x
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) sorry)
Tactic: have hf := fun n => (haef n).stronglyMeasurable_mk
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) sorry
Tactic: have hff' := fun n => (haef n).ae_eq_mk (μ := μ)
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) sorry) p μ
Tactic: have hui' := hui.ae_eq hff'
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) sorry) p μ
Tactic: have hut' := hut.aeeq hff'
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hg : StronglyMeasurable (AEStronglyMeasurable.mk g sorry)
Tactic: have hg := hg'.aestronglyMeasurable.stronglyMeasurable_mk
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g sorry
Tactic: have hgg' := hg'.aestronglyMeasurable.ae_eq_mk (μ := μ)
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hg'' : MemLp (AEStronglyMeasurable.mk g sorry) p μ
Tactic: have hg'' := hg'.ae_eq hgg'
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hut' : UnifTight.{u_1, u_2, 0} (β := β) (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯) p μ
hg : StronglyMeasurable (AEStronglyMeasurable.mk g ⋯)
hgg' : g =ᶠ[ae μ] AEStronglyMeasurable.mk g ⋯
hg'' : MemLp (AEStronglyMeasurable.mk g ⋯) p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) sorry x) atTop (𝓝 (AEStronglyMeasurable.mk g sorry x))
Tactic: have haefg' := ae_tendsto_ae_congr hff' hgg' 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
Tactic: have haefg (n : ℕ) : f n - g =ᵐ[μ] f' n - g' := (hff' n).sub hgg'
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
Tactic: have hsnfg (n : ℕ) := eLpNorm_congr_ae (p := p) (haefg n)
-- 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 : α → β
haef : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg' : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
hf : ∀ (n : ℕ), StronglyMeasurable (AEStronglyMeasurable.mk (f n) ⋯)
hff' : ∀ (n : ℕ), f n =ᶠ[ae μ] AEStronglyMeasurable.mk (f n) ⋯
f' : (n : ℕ) → α → β := fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯
hui' : UnifIntegrable f' p μ
hut' : UnifTight f' p μ
g' : α → β := AEStronglyMeasurable.mk g ⋯
hg : StronglyMeasurable g'
hgg' : g =ᶠ[ae μ] g'
hg'' : MemLp g' p μ
haefg' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ AEStronglyMeasurable.mk (f n) ⋯ x) atTop (𝓝 (g' x))
haefg : ∀ (n : ℕ), f n - g =ᶠ[ae μ] f' n - g'
hsnfg : ∀ (n : ℕ), eLpNorm (f n - g) p μ = eLpNorm (f' n - g') p μ
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have apply : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f' n - g') p μ) atTop (𝓝 0)
Tactic: apply Filter.Tendsto.congr (fun n => (hsnfg n).symm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f n - g) p μ) atTop (𝓝 0)
have refine : ∀ (ns : ℕ → ℕ) (hns : Tendsto ns atTop atTop),
  ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
Tactic: refine tendsto_of_subseq_tendsto fun ns hns => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UnifTight (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst : NormedAddCommGroup β
μ : Measure α
p : ℝ≥0∞
f : ℕ → α → β
g : α → β
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hg : MemLp g p μ
hui : UnifIntegrable f p μ
hut : UnifTight f p μ
hfg : TendstoInMeasure μ f atTop g
ns : ℕ → ℕ
hns : Tendsto ns atTop atTop
⊢ ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
have obtain : ∀ (ms : ℕ → ℕ),
  StrictMono ms →
    ∀ (hms' : ∀ᵐ (x : α) ∂μ, Tendsto (fun (i : ℕ) ↦ f (ns (ms i)) x) atTop (𝓝 (g x))),
      ∃ (ms : ℕ → ℕ), Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ eLpNorm (f (ns (ms n)) - g) p μ) atTop (𝓝 0)
Tactic: obtain ⟨ms, _, hms'⟩ := TendstoInMeasure.exists_seq_tendsto_ae fun ε hε => (hfg ε hε).comp hns
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
have hε2 : 0 < ε / 2
Tactic: have hε2 : 0 < ε / 2 := half_pos hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ₁ : ℝ) (hδ₁_pos : 0 < δ₁)
  (hfδ₁ :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ₁, hδ₁_pos, hfδ₁⟩ := hf hε2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ₂ : ℝ) (hδ₂_pos : 0 < δ₂)
  (hgδ₂ :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ₂, hδ₂_pos, hgδ₂⟩ := hg hε2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (i : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)),
  eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨min δ₁ δ₂, lt_min hδ₁_pos hδ₂_pos, fun i s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ eLpNorm (s.indicator ((f + g) i)) p μ ≤ ENNReal.ofReal ε
have simp_rw : eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: simp_rw [Pi.add_apply, Set.indicator_add']
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ eLpNorm (s.indicator (f i) + s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
have refine : eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine (eLpNorm_add_le ((hf_meas i).indicator hs) ((hg_meas i).indicator hs) hp).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f g : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
hg : UnifIntegrable g p μ
hp : 1 ≤ p
hf_meas : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hg_meas : ∀ (i : ι), AEStronglyMeasurable (g i) μ
ε : ℝ
hε : 0 < ε
hε2 : 0 < ε / 2
δ₁ : ℝ
hδ₁_pos : 0 < δ₁
hfδ₁ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
δ₂ : ℝ
hδ₂_pos : 0 < δ₂
hgδ₂ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
have rw : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2 + ε / 2)
Tactic: rw [← ENNReal.ofReal_add hε2.le hε2.le, add_halves]