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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : TendstoInMeasure μ (fn ∘ s) u f
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((fun (f : (↑{g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} : Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β)) {g : α → β | ∃ (ni : κ → ι), TendstoInMeasure μ (fn ∘ ni) u g} x) f ⋯)))
      p μ ≤
    ENNReal.ofReal ε
have refine : ∀ (i : κ), AEStronglyMeasurable (t.indicator (fn (s i))) μ
Tactic: refine eLpNorm_le_of_tendstoInMeasure
    (Eventually.of_forall fun n => hδ' (s n) t ht ht') (hs.indicator t) ?_
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2)))
      (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun
                      (f :
                        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                          Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδ : 0 < δ)
  (hδ' :
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2)))
      (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun
                      (f :
                        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                          Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ, hδ'⟩ := hUI 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀
      (i :
        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
          Type (max u_1 u_2)))
      (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β)
              (s.indicator
                ((fun
                      (f :
                        (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                          Type (max u_1 u_2))) ↦
                    (↑f : α → β))
                  i))
              p μ ≤
            ENNReal.ofReal ε
have refine : ∀
  (x :
    (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
      Type (max u_1 u_2)))
  (t : Set α) (ht : MeasurableSet t) (ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ) (f : α → β) (s : κ → ι)
  (hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))),
  eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((fun
              (f :
                (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                  Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β))
              {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
            f sorry)))
      p μ ≤
    ENNReal.ofReal ε
Tactic: refine ⟨δ, hδ, fun ⟨f, s, hs⟩ t ht ht' => ?_⟩
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((fun
              (f :
                (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                  Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β))
              {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
            f ⋯)))
      p μ ≤
    ENNReal.ofReal ε
have refine_1 : ∀ (n : κ), AEStronglyMeasurable (t.indicator (fn (s n))) μ
Tactic: refine Lp.eLpNorm_le_of_ae_tendsto
    (Eventually.of_forall (f := u) fun n => hδ' (s n) t ht ht') ?_ ?_
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
refine_1 : ∀ (n : κ), AEStronglyMeasurable (t.indicator (fn (s n))) μ
⊢ eLpNorm.{u_1, u_2} (ε := β)
      (t.indicator
        ((fun
              (f :
                (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                  Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β))
              {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
            f ⋯)))
      p μ ≤
    ENNReal.ofReal ε
have refine_2 : ∀ᵐ (x : α) ∂μ,
  Tendsto.{u_4, u_2} (β := β) (fun (x_1 : κ) ↦ t.indicator (fn (s x_1)) x) u
    (𝓝
      (t.indicator
        ((fun
              (f :
                (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                  Type (max u_1 u_2))) ↦
            (↑f : α → β))
          (Subtype.mk (p := fun (x : α → β) ↦
            Membership.mem (γ := Set (α → β))
              {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
            f sorry))
        x))
Tactic: refine Lp.eLpNorm_le_of_ae_tendsto
    (Eventually.of_forall (f := u) fun n => hδ' (s n) t ht ht') ?_ ?_
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto.{u_4, u_2} (β := β) (fun (x_1 : κ) ↦ t.indicator (fn (s x_1)) x) u
      (𝓝
        (t.indicator
          ((fun
                (f :
                  (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} :
                    Type (max u_1 u_2))) ↦
              (↑f : α → β))
            (Subtype.mk (p := fun (x : α → β) ↦
              Membership.mem (γ := Set (α → β))
                {g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} x)
              f ⋯))
          x))
have h : ∀ (a : α) (ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))),
  Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Tactic: filter_upwards [hs] with a ha
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))
⊢ Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
have pos : ∀ (memt : a ∈ t), Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Tactic: by_cases memt : a ∈ t
-- 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 β
p : ℝ≥0∞
κ : Type u_4
u : Filter κ
inst_1 : u.NeBot
inst_2 : u.IsCountablyGenerated
fn : ι → α → β
hUI : UnifIntegrable fn p μ
hfn : ∀ (i : ι), AEStronglyMeasurable (fn i) μ
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδ' :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (fn i)) p μ ≤ ENNReal.ofReal ε
x : (↑{g : α → β | ∃ (ni : κ → ι), ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (ni n) x) u (𝓝 (g x))} : Type (max u_1 u_2))
t : Set α
ht : MeasurableSet t
ht' : (μ : (a : Set α) → ℝ≥0∞) t ≤ ENNReal.ofReal δ
f : α → β
s : κ → ι
hs : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : κ) ↦ fn (s n) x) u (𝓝 (f x))
a : α
ha : Tendsto (fun (n : κ) ↦ fn (s n) a) u (𝓝 (f a))
pos : ∀ (memt : a ∈ t), Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
⊢ Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
have neg : ∀ (memt : a ∉ t), Tendsto (fun (x : κ) ↦ t.indicator (fn (s x)) a) u (𝓝 (t.indicator f a))
Tactic: by_cases memt : a ∈ t
-- 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 β
p : ℝ≥0∞
f g : ι → α → β
hf : UniformIntegrable f p μ
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
⊢ UniformIntegrable g p μ
have obtain : ∀ (hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ) (hunif : UnifIntegrable f p μ) (C : ℝ≥0)
  (hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)), UniformIntegrable g p μ
Tactic: obtain ⟨hfm, hunif, C, hC⟩ := hf
Cleared hypotheses: hf
-- 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 β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable g p μ
have refine : ∀ (i : ι), eLpNorm (g i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: refine ⟨fun i => (hfm i).congr (hfg i), (unifIntegrable_congr_ae hfg).1 hunif, C, fun i => ?_⟩
-- 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 β
p : ℝ≥0∞
f g : ι → α → β
hfg : ∀ (n : ι), f n =ᶠ[ae μ] g n
hfm : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hunif : UnifIntegrable f p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
i : ι
⊢ eLpNorm (g i) p μ ≤ (↑C : ℝ≥0∞)
have rw : eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: rw [← eLpNorm_congr_ae (hfg i)]
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
⊢ UniformIntegrable f p μ
have intro : ∀ (val : Fintype ι), UniformIntegrable f p μ
Tactic: cases nonempty_fintype ι
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
⊢ UniformIntegrable f p μ
have intro : ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: refine ⟨fun n => (hf n).1, unifIntegrable_finite hp_one hp_top hf, ?_⟩
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have pos : ∀ (hι : Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: by_cases hι : Nonempty ι
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
pos : ∀ (hι : Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have neg : ∀ (hι : ¬Nonempty ι), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: by_cases hι : Nonempty ι
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
hι : Nonempty ι
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
Tactic: choose _ hf using hf
Cleared hypotheses: hf
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : ∀ (i : ι), MemLp (f i) p μ
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have hf₁ : ∀ (i : ι), eLpNorm (f i) p μ < ∞
Tactic: choose _ hf using hf
Cleared hypotheses: hf
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have pos : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C.toNNReal : ℝ≥0∞)
Tactic: refine ⟨C.toNNReal, fun i => ?_⟩
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
⊢ eLpNorm (f i) p μ ≤ (↑C.toNNReal : ℝ≥0∞)
have pos : eLpNorm (f i) p μ ≤ C
Tactic: rw [ENNReal.coe_toNNReal]
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
pos : eLpNorm (f i) p μ ≤ C
⊢ eLpNorm (f i) p μ ≤ (↑C.toNNReal : ℝ≥0∞)
have pos₁ : C ≠ ∞
Tactic: rw [ENNReal.coe_toNNReal]
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
⊢ C ≠ ∞
have pos : ∀ (y : ℝ≥0∞) (hy : Membership.mem (γ := Finset ℝ≥0∞) (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) y),
  y < ∞
Tactic: refine ne_of_lt ((Finset.max'_lt_iff _ _).2 fun y hy => ?_)
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : Finite ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
val : Fintype ι
hι : Nonempty ι
h : ∀ (i : ι), AEStronglyMeasurable (f i) μ
hf : ∀ (i : ι), eLpNorm (f i) p μ < ∞
C : ℝ≥0∞ := Finset.max' (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) ⋯
i : ι
y : ℝ≥0∞
hy : Membership.mem (γ := Finset ℝ≥0∞) (Finset.image (fun (i : ι) ↦ eLpNorm (f i) p μ) Finset.univ) y
⊢ y < ∞
have hy₁ : ∃ (a : ι), Membership.mem (γ := Finset ι) Finset.univ a ∧ eLpNorm (f a) p μ = y
Tactic: rw [Finset.mem_image] at hy
Cleared hypotheses: hy
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ UniformIntegrable f p μ
have refine : ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: refine ⟨fun i => (hf i).aestronglyMeasurable,
    unifIntegrable_of hp hp' (fun i => (hf i).aestronglyMeasurable) 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have obtain : ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: obtain ⟨C, hC⟩ := h 1 one_pos
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
have refine : ∀ (i : ι),
  eLpNorm (f i) p μ ≤
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
Tactic: refine ⟨((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1).toNNReal, fun i => ?_⟩
-- 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 β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤
    eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ
have refine : ∀ (x : α), ‖f i x‖ₑ ≤ ‖(indicator {x : α | ‖f i x‖₊ < C} (f i) + indicator {x : α | C ≤ ‖f i x‖₊} (f i)) x‖ₑ
Tactic: refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)