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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hμs' : μ s = 0
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
pos :
  ∀ (hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hμs' : μ s = 0
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : 0 ≤ ENNReal.ofReal ε
Tactic: rw [(eLpNorm_eq_zero_iff ((hf i).indicator hs).aestronglyMeasurable hpzero).2
        (indicator_meas_zero 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 β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm (s.indicator (f i)) p μ ≤
    eLpNorm ((s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i)) p μ +
      eLpNorm ((s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ
have refine : eLpNorm (s.indicator (f i)) p μ =
  eLpNorm ((s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ
Tactic: refine le_trans (Eq.le ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (hs.inter ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const))))
        hp)
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm (s.indicator (f i)) p μ =
    eLpNorm ((s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ
have e_f : s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
Tactic: congr
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
have e_f : s.indicator (f i) = fun (x : α) ↦
  (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) x + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i) x
Tactic: change _ = fun x => (s ∩ { x : α | C ≤ ‖f i x‖₊ }).indicator (f i) x +
        (s ∩ { x : α | ‖f i x‖₊ < C }).indicator (f i) x
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.indicator (f i) = fun (x : α) ↦
    (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) x + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i) x
have e_f : s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊} ∪ s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
Tactic: rw [← Set.indicator_union_of_disjoint]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
e_f : s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊} ∪ s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
⊢ s.indicator (f i) = fun (x : α) ↦
    (s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i) x + (s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i) x
have e_f₁ : Disjoint (s ∩ {x : α | C ≤ ‖f i x‖₊}) (s ∩ {x : α | ‖f i x‖₊ < C})
Tactic: rw [← Set.indicator_union_of_disjoint]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set α) ({x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C}) univ
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) ({x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C}) x ↔ Membership.mem (γ := Set α) univ x
Tactic: ext
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊} ∪ s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
have e_f : s.indicator (f i) = (s ∩ ({x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C})).indicator (f i)
Tactic: rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_gt] :
            { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
          Set.inter_univ]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
e_f : s.indicator (f i) = (s ∩ ({x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C})).indicator (f i)
⊢ s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊} ∪ s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
have e_f₁ : s.indicator (f i) = (s ∩ univ).indicator (f i)
Tactic: rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_gt] :
            { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
          Set.inter_univ]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
e_f : s.indicator (f i) = (s ∩ ({x : α | C ≤ ‖f i x‖₊} ∪ {x : α | ‖f i x‖₊ < C})).indicator (f i)
e_f₁ : s.indicator (f i) = (s ∩ univ).indicator (f i)
⊢ s.indicator (f i) = (s ∩ {x : α | C ≤ ‖f i x‖₊} ∪ s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)
have e_f₂ : s.indicator (f i) = s.indicator (f i)
Tactic: rw [← Set.inter_union_distrib_left, (by ext; simp [le_or_gt] :
            { x : α | C ≤ ‖f i x‖₊ } ∪ { x : α | ‖f i x‖₊ < C } = Set.univ),
          Set.inter_univ]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Disjoint (s ∩ {x : α | C ≤ ‖f i x‖₊}) (s ∩ {x : α | ‖f i x‖₊ < C})
have e_f : Disjoint.{u_1} (α := Set α) {x : α | C ≤ ‖f i x‖₊} {x : α | ‖f i x‖₊ < C}
Tactic: refine (Disjoint.inf_right' _ ?_).inf_left' _
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Disjoint.{u_1} (α := Set α) {x : α | C ≤ ‖f i x‖₊} {x : α | ‖f i x‖₊ < C}
have e_f : LE.le.{u_1} (α := Set α) ({x : α | C ≤ ‖f i x‖₊} ⊓ {x : α | ‖f i x‖₊ < C}) ⊥
Tactic: rw [disjoint_iff_inf_le]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx₁ : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
hx₂ : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x
⊢ Membership.mem (γ := Set α) ⊥ x
have hx₃ : C ≤ ‖f i x‖₊
Tactic: rw [Set.mem_setOf_eq] at hx₁ hx₂
Cleared hypotheses: hx₁, hx₂
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx₁ : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
hx₂ : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x
hx₃ : C ≤ ‖f i x‖₊
⊢ Membership.mem (γ := Set α) ⊥ x
have hx₄ : ‖f i x‖₊ < C
Tactic: rw [Set.mem_setOf_eq] at hx₁ hx₂
Cleared hypotheses: hx₁, 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 β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm ((s ∩ {x : α | C ≤ ‖f i x‖₊}).indicator (f i)) p μ +
      eLpNorm ((s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤
    eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ +
      (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have refine : eLpNorm ((s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: refine add_le_add
        (eLpNorm_mono fun x => norm_indicator_le_of_subset Set.inter_subset_right _ _) ?_
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm ((s ∩ {x : α | ‖f i x‖₊ < C}).indicator (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have rw : eLpNorm (s.indicator (indicator {x : α | ‖f i x‖₊ < C} (f i))) p μ ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: rw [← Set.indicator_indicator]
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ eLpNorm (s.indicator (indicator {x : α | ‖f i x‖₊ < C} (f i))) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
have rw : eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p (μ.restrict s) ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 / p.toReal)
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_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 β
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖ ≤ (↑C : ℝ)
have h₁ : ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖ ≤ (↑C : ℝ)
Tactic: filter_upwards
-- 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∞
hp : 1 ≤ p
hp' : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε → ∃ (C : ℝ≥0), 0 < C ∧ ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
hpzero : p ≠ 0
hμ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hCpos : 0 < C
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal (ε / 2)
i : ι
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / (2 * (↑C : ℝ))) ^ p.toReal)
hμs' : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖ ≤ (↑C : ℝ)
have h₁ : ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖) a ≤ (↑C : ℝ)
Tactic: simp_rw [norm_indicator_eq_indicator_norm]