awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 δ₁ δ₂)
rw : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2 + ε / 2)
⊢ ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
have rw₁ : ENNReal.ofReal ε = ENNReal.ofReal ε
Tactic: rw [← ENNReal.ofReal_add hε2.le hε2.le, add_halves]
-- 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 < ε
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)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
have hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
Tactic: have hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2) := by
    rw [← ENNReal.ofReal_add hε2.le hε2.le, add_halves]
-- 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 δ₁ δ₂)
hε_halves : ENNReal.ofReal ε = ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
⊢ eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
have rw : eLpNorm (s.indicator (f i)) p μ + eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal (ε / 2) + ENNReal.ofReal (ε / 2)
Tactic: rw [hε_halves]
-- 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
⊢ UnifIntegrable (-f) p μ
have simp_rw : ∀ ⦃ε : ℝ⦄,
  0 < ε →
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: simp_rw [UnifIntegrable, Pi.neg_apply, Set.indicator_neg', eLpNorm_neg]
-- 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) μ
⊢ UnifIntegrable (f - g) p μ
have rw : UnifIntegrable (f + -g) p μ
Tactic: rw [sub_eq_add_neg]
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (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 ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ_pos, hfδ⟩ := hf 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (n : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  s.indicator (g n) =ᶠ[ae μ] s.indicator (f n)
Tactic: refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hfδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ s.indicator (g n) =ᶠ[ae μ] s.indicator (f n)
have h : ∀ (x : α) (hx : f n x = g n x), s.indicator (g n) x = s.indicator (f n) x
Tactic: filter_upwards [hfg n] with x hx
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
⊢ UnifIntegrable g p μ
have intro : ∀ ⦃ε : ℝ⦄,
  0 < ε →
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: classical
  intro ε hε
  obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
  refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n s hs hμs)⟩
  filter_upwards [hfg n] with x hx
  simp_rw [Set.indicator_apply, hx]
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
intro intro₁ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
⊢ UnifIntegrable g p μ
have intro₂ : ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
  (hfδ :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: classical
  intro ε hε
  obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
  refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n s hs hμs)⟩
  filter_upwards [hfg n] with x hx
  simp_rw [Set.indicator_apply, hx]
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
intro intro₁ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
intro₂ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
    (hfδ :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
⊢ UnifIntegrable g p μ
have intro₃ : ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
  (hfδ :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
  (n : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  s.indicator (g n) =ᶠ[ae μ] s.indicator (f n)
Tactic: classical
  intro ε hε
  obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
  refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n s hs hμs)⟩
  filter_upwards [hfg n] with x hx
  simp_rw [Set.indicator_apply, hx]
-- 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 μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
intro intro₁ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
intro₂ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
    (hfδ :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
intro₃ :
  ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
    (hfδ :
      ∀ (i : ι) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
    (n : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
    s.indicator (g n) =ᶠ[ae μ] s.indicator (f n)
⊢ UnifIntegrable g p μ
have h : ∀ ⦃ε : ℝ⦄ (hε : 0 < ε) (δ : ℝ) (hδ_pos : 0 < δ)
  (hfδ :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε)
  (n : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ) (x : α)
  (hx : f n x = g n x), s.indicator (g n) x = s.indicator (f n) x
Tactic: classical
  intro ε hε
  obtain ⟨δ, hδ_pos, hfδ⟩ := hf hε
  refine ⟨δ, hδ_pos, fun n s hs hμs => (le_of_eq <| eLpNorm_congr_ae ?_).trans (hfδ n s hs hμs)⟩
  filter_upwards [hfg n] with x hx
  simp_rw [Set.indicator_apply, hx]
-- 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (i : ι) ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδ_pos : 0 < δ)
  (hε :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (i : ι) ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ_pos, hε⟩ := hf 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε_1 : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (i : ι) ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (i : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (i : ι) ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨δ, 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε_1 : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (i : ι) ↦ E.indicator (f i)) i)) p μ ≤ ENNReal.ofReal ε
have eLpNorm : eLpNorm (s.indicator (E.indicator (f i))) p μ = eLpNorm (E.indicator (s.indicator (f i))) p μ
Tactic: calc
    eLpNorm (s.indicator (E.indicator (f i))) p μ
      = eLpNorm (E.indicator (s.indicator (f i))) p μ := by
      simp only [indicator_indicator, inter_comm]
    _ ≤ eLpNorm (s.indicator (f i)) p μ := eLpNorm_indicator_le _
    _ ≤ ENNReal.ofReal ε := hε _ _ 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδ_pos : 0 < δ)
  (hδε :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ_pos, hδε⟩ := hf 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
have refine : ∀ (i : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
Tactic: refine ⟨δ, hδ_pos, fun i s hs hμs ↦ ?_⟩
-- 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ.restrict E : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
have hμs₁ : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
Tactic: rw [μ.restrict_apply hs, ← measure_toMeasurable] at hμs
Cleared hypotheses: 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E))
have rw : eLpNorm (f i) p ((μ.restrict E).restrict s) = eLpNorm (f i) p (μ.restrict (s ∩ E))
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
-- 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
rw : eLpNorm (f i) p ((μ.restrict E).restrict s) = eLpNorm (f i) p (μ.restrict (s ∩ E))
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E))
have rw₁ : eLpNorm (f i) p (μ.restrict (s ∩ E)) = eLpNorm (f i) p (μ.restrict (s ∩ E))
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
-- 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 : ι → α → β
p : ℝ≥0∞
hf : UnifIntegrable f p μ
E : Set α
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ_pos : 0 < δ
hδε :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ (s ∩ E)) ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator (f i)) p (μ.restrict E) ≤ ENNReal.ofReal ε
have eLpNorm : eLpNorm (s.indicator (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E))
Tactic: calc
    eLpNorm (indicator s (f i)) p (μ.restrict E) = eLpNorm (f i) p (μ.restrict (s ∩ E)) := by
      rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, μ.restrict_restrict hs]
    _ ≤ eLpNorm (f i) p (μ.restrict (toMeasurable μ (s ∩ E))) :=
      eLpNorm_mono_measure _ <| Measure.restrict_mono (subset_toMeasurable _ _) le_rfl
    _ = eLpNorm (indicator (toMeasurable μ (s ∩ E)) (f i)) p μ :=
      (eLpNorm_indicator_eq_eLpNorm_restrict (measurableSet_toMeasurable _ _)).symm
    _ ≤ ENNReal.ofReal ε := hδε i _ (measurableSet_toMeasurable _ _) hμs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
⊢ Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
have refine : ∀ (n : ℕ) (hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1), indicator {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x = 0
Tactic: refine tendsto_atTop_of_eventually_const (i₀ := Nat.ceil (‖f x‖₊ : ℝ) + 1) fun n hn => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ indicator {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x = 0
have h : x ∉ {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)}
Tactic: rw [Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ x ∉ {x : α | (↑n : ℝ) ≤ (↑‖f x‖₊ : ℝ)}
have h : (↑‖f x‖₊ : ℝ) < (↑n : ℝ)
Tactic: simp only [not_le, Set.mem_setOf_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ (↑‖f x‖₊ : ℝ) < (↑n : ℝ)
have h : LT.lt (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) (↑n : ℝ)
Tactic: refine lt_of_le_of_lt (Nat.le_ceil _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ LT.lt (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) (↑n : ℝ)
have h : HAdd.hAdd (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) 1 ≤ (↑n : ℝ)
Tactic: refine lt_of_lt_of_le (lt_add_one _) ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
inst : NormedAddCommGroup β
f : α → β
x : α
n : ℕ
hn : n ≥ ⌈(↑‖f x‖₊ : ℝ)⌉₊ + 1
⊢ HAdd.hAdd (α := ℝ) (↑⌈(↑‖f x‖₊ : ℝ)⌉₊ : ℝ) 1 ≤ (↑n : ℝ)
have h : ⌈‖f x‖⌉₊ + 1 ≤ n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f 1 μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ (M : ℝ), ∫⁻ (x : α), (↑‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖₊ : ℝ≥0∞) ∂μ ≤ ENNReal.ofReal ε
have htendsto : ∀ᵐ (x : α) ∂μ,
  Tendsto.{0, u_2} (β := β) (fun (M : ℕ) ↦ Set.indicator {x : α | (↑M : ℝ) ≤ (↑‖f x‖₊ : ℝ)} f x) atTop (𝓝 0)
Tactic: have htendsto :
      ∀ᵐ x ∂μ, Tendsto (fun M : ℕ => { x | (M : ℝ) ≤ ‖f x‖₊ }.indicator f x) atTop (𝓝 0) :=
    univ_mem' (id fun x => tendsto_indicator_ge f x)